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

State before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
have := Nat.beta_unbeta_coe (recSequence f g z v) ⟨m, by simp[recSequence, hm]⟩
State after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta ↑⟨m, ⋯⟩ = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m

State before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta ↑⟨m, ⋯⟩ = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
simp at this
State after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m

State before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
rw[this]
State after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (recSequence f g z v).get ⟨m, ⋯⟩ = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m

State before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (recSequence f g z v).get ⟨m, ⋯⟩ = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
simp[recSequence]
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
⊢ m < (recSequence f g z v).length
Tactic:
simp[recSequence, hm]
State after:
no goals