Theorem: Nat.Arith₁.beta_eq_rec (Logic/Vorspiel/Arith.lean)

State before:
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
h0 : z.beta 0 = f v
hs : ∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)
⊢ z.beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
induction' m with m ih <;> simp[h0]
State after:
case succ
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
h0 : z.beta 0 = f v
m : ℕ
ih : (∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) → z.beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
hs : ∀ i < m + 1, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)
⊢ z.beta (m + 1) = g (m ::ᵥ rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m ::ᵥ v)

State before:
case succ
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
h0 : z.beta 0 = f v
m : ℕ
ih : (∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) → z.beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
hs : ∀ i < m + 1, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)
⊢ z.beta (m + 1) = g (m ::ᵥ rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m ::ᵥ v)
Tactic:
rw[hs m (lt.base m), ←ih (fun i hi => hs i (lt.step hi))]
State after:
no goals