Theorem: Nat.fold'_congr (Fifteen/Data/Nat/Basic.lean)

State before:
α : Type u
m n : Nat
h : m = n
f : Fin m → α → α
g : Fin n → α → α
hf : ∀ (i : Fin m) (j : Fin n) (a : α), i.val = j.val → f i a = g j a
init : α
⊢ fold' m f init = fold' n g init
Tactic:
cases h
State after:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
⊢ fold' m f init = fold' m g init

State before:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
⊢ fold' m f init = fold' m g init
Tactic:
have : f = g := funext fun i => funext fun a =>
  hf i i a rfl
State after:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
this : f = g
⊢ fold' m f init = fold' m g init

State before:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
this : f = g
⊢ fold' m f init = fold' m g init
Tactic:
cases this
State after:
case refl.refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = f j a
⊢ fold' m f init = fold' m f init

State before:
case refl.refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = f j a
⊢ fold' m f init = fold' m f init
Tactic:
rfl
State after:
no goals