Theorem: Nat.rec_eq (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
H : ∀ m < n, ∀ (a : α), f₁ m a = f₂ m a
⊢ rec a f₁ n = rec a f₂ n
Tactic:
induction' n with n ih <;> simp
State after:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)

State before:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)
Tactic:
have : (n.rec a f₁ : α) = n.rec a f₂ := ih (fun m hm a =>  H m (Nat.lt.step hm) a)
State after:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
this : rec a f₁ n = rec a f₂ n
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)

State before:
case succ
α✝ : ℕ → Sort u
α : Sort u_1
a : α
f₁ f₂ : ℕ → α → α
n : ℕ
ih : (∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) → rec a f₁ n = rec a f₂ n
H : ∀ m < n + 1, ∀ (a : α), f₁ m a = f₂ m a
this : rec a f₁ n = rec a f₂ n
⊢ f₁ n (rec a f₁ n) = f₂ n (rec a f₂ n)
Tactic:
simpa[this] using H n (Nat.lt.base n) (n.rec a f₂)
State after:
no goals