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

State before:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i✝ : Fin (succ 0).succ
i : Fin 1
⊢ Arith₁ (![g, h] i.succ)
Tactic:
simpa using hh
State after:
no goals

State before:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
⊢ ∀ (i : Vector ℕ n), f ((ofFn fun i_1 => ![g, h] i_1 i).get 0) ((ofFn fun i_1 => ![g, h] i_1 i).get 1) = f (g i) (h i)
Tactic:
intro i
State after:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ f ((ofFn fun i_1 => ![g, h] i_1 i).get 0) ((ofFn fun i_1 => ![g, h] i_1 i).get 1) = f (g i) (h i)

State before:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ f ((ofFn fun i_1 => ![g, h] i_1 i).get 0) ((ofFn fun i_1 => ![g, h] i_1 i).get 1) = f (g i) (h i)
Tactic:
simp[Matrix.comp_vecCons']
State after:
no goals