case refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ Agrees arr f g
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
n : ℕ
g : Fin n → β
e : n = Array.size arr
H :
  ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
    f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ Agrees arr f g
cases e
case refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
this : (fun i => f (Array.get arr i)) = g
⊢ Agrees arr f g
case refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ Agrees arr f g
have : (fun i ↦ f (arr.get i)) = g := by funext ⟨i, h⟩; apply H
case refl.refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
H :
  ∀ (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₂ }
⊢ Agrees arr f fun i => f (Array.get arr i)
case refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
this : (fun i => f (Array.get arr i)) = g
⊢ Agrees arr f g
cases this
no goals
case refl.refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
H :
  ∀ (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₂ }
⊢ Agrees arr f fun i => f (Array.get arr i)
constructor
case h
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
i : ℕ
h : i < Array.size arr
⊢ f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h }
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ (fun i => f (Array.get arr i)) = g
funext ⟨i, h⟩
no goals
case h
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
i : ℕ
h : i < Array.size arr
⊢ f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h }
apply H