Theorem: LO.FirstOrder.Arith.Model.val_npow (Arithmetization/Vorspiel/Lemmata.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c : M
k : ℕ
a : M
⊢ (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
Tactic:
induction k <;> simp [Operator.npow_zero, Operator.npow_succ, Operator.val_comp, Matrix.empty_eq, Matrix.comp_vecCons']
State after:
case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝¹ b c a : M
n✝ : ℕ
a✝ : (Operator.npow ℒₒᵣ n✝).val ![a] = a ^ n✝
⊢ (op(*).val fun i => (![Operator.npow ℒₒᵣ n✝, Operator.bvar 0] i).val ![a]) = a ^ (n✝ + 1)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ (op(*).val fun i => (![Operator.npow ℒₒᵣ k, Operator.bvar 0] i).val ![a]) = a ^ (k + 1)
Tactic:
case succ k IH =>
  rw [Matrix.fun_eq_vec₂ (v := fun i => Operator.val ((Operator.npow ℒₒᵣ k :> ![Operator.bvar 0]) i) ![a]), pow_succ]
  simp [npowRec, mul_comm a, IH]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ (op(*).val fun i => (![Operator.npow ℒₒᵣ k, Operator.bvar 0] i).val ![a]) = a ^ (k + 1)
Tactic:
rw [Matrix.fun_eq_vec₂ (v := fun i => Operator.val ((Operator.npow ℒₒᵣ k :> ![Operator.bvar 0]) i) ![a]), pow_succ]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ op(*).val
      ![(![Operator.npow ℒₒᵣ k, Operator.bvar 0] 0).val ![a], (![Operator.npow ℒₒᵣ k, Operator.bvar 0] 1).val ![a]] =
    a ^ k * a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ op(*).val
      ![(![Operator.npow ℒₒᵣ k, Operator.bvar 0] 0).val ![a], (![Operator.npow ℒₒᵣ k, Operator.bvar 0] 1).val ![a]] =
    a ^ k * a
Tactic:
simp [npowRec, mul_comm a, IH]
State after:
no goals