case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
⊢ ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
    f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ }
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
n : ℕ
m : Fin n → β
H : Agrees arr f m
⊢ ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
    f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }
cases H
no goals
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
⊢ ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
    f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ }
exact fun i h _ ↦ rfl