awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih :
  HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) k =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k)
succ :
  HMul.hMul (β := Matrix n n R)
      (HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) k)
      ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ (k + 1))
succ₁ :
  HMul.hMul (β := Matrix n n R)
      (HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) k)
      ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k * f)
succ₂ :
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k) : Matrix n n R)
      ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k * f)
⊢ HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) (k + 1) =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ (k + 1))
have succ₃ : Eq (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k * f) : Matrix n n R)
  ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k * f) : Matrix n n R)
Tactic: rw [pow_succ, pow_succ, ih, ← toMatrix_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
k : ℕ
⊢ HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) k =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k)
have zero : HPow.hPow (α := Matrix n n R) (β := ℕ) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) 0 =
  (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (HPow.hPow (β := ℕ) f 0)
Tactic: induction k with
  | zero => simp
  | succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
k : ℕ
zero :
  HPow.hPow (α := Matrix n n R) (β := ℕ) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) 0 =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (HPow.hPow (β := ℕ) f 0)
⊢ HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) k =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k)
have succ : ∀ (k : ℕ)
  (ih :
    HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) k =
      (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ k)),
  HPow.hPow (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) (k + 1) =
    (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ^ (k + 1))
Tactic: induction k with
  | zero => simp
  | succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
⊢ Eq (α := M₁ →ₗ[R] M₃) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B) : M₁ →ₗ[R] M₃)
    ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B :
      M₁ →ₗ[R] M₃)
have a : Eq (α := Matrix l n R)
  ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) :
    Matrix l n R)
  ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R)
      ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
    Matrix l n R)
Tactic: apply (LinearMap.toMatrix v₁ v₃).injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
⊢ Eq (α := Matrix l n R)
    ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) :
      Matrix l n R)
    ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R)
        ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix l n R)
have a : ∀ (this : DecidableEq l),
  Eq (α := Matrix l n R)
    ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) :
      Matrix l n R)
    ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R)
        ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix l n R)
Tactic: haveI : DecidableEq l := fun _ _ ↦ Classical.propDecidable _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ Eq (α := Matrix l n R)
    ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) :
      Matrix l n R)
    ((toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R)
        ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A ∘ₗ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix l n R)
have a : (toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) =
  HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
    ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
      Matrix l m R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix m n R)
Tactic: rw [LinearMap.toMatrix_comp v₁ v₂ v₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ (toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
        Matrix l m R)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
        Matrix m n R)
have a : A * B =
  HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
    ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
      Matrix l m R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix m n R)
Tactic: rw [LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ A * B =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
        Matrix l m R)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
        Matrix m n R)
have a : A * B =
  HMul.hMul (β := Matrix m n R) A
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix m n R)
Tactic: rw [LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ A * B =
    HMul.hMul (β := Matrix m n R) A
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
        Matrix m n R)
have a : A * B = A * B
Tactic: rw [LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ (toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
        Matrix l m R)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
        Matrix m n R)
have a : A * B =
  HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
    ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
      Matrix l m R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix m n R)
Tactic: repeat' rw [LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : Finite l
inst_11 : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
a a₁ a₂ :
  A * B =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
        Matrix l m R)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
        Matrix m n R)
⊢ (toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) ((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B)) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) ((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A) :
        Matrix l m R)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
        Matrix m n R)
have a₃ : A * B =
  HMul.hMul (β := Matrix m n R) A
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B) :
      Matrix m n R)
Tactic: repeat' rw [LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_4
inst_1 : Fintype n_1
inst_2 : DecidableEq n_1
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n_1 R M₁
A : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n
⊢ (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ (n + 1)) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
have succ : (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
  HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
Tactic: rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_4
inst_1 : Fintype n_1
inst_2 : DecidableEq n_1
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n_1 R M₁
A : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n
succ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
⊢ (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ (n + 1)) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
have succ₁ : (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
  HMul.hMul (β := M₁ →ₗ[R] M₁)
    (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
    ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
Tactic: rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_4
inst_1 : Fintype n_1
inst_2 : DecidableEq n_1
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n_1 R M₁
A : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n
succ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
succ₁ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HMul.hMul (β := M₁ →ₗ[R] M₁)
      (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
      ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
⊢ (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ (n + 1)) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
have succ₂ : (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) ∘ₗ (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A =
  HMul.hMul (β := M₁ →ₗ[R] M₁)
    (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
    ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
Tactic: rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_4
inst_1 : Fintype n_1
inst_2 : DecidableEq n_1
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n_1 R M₁
A : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n
succ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
succ₁ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HMul.hMul (β := M₁ →ₗ[R] M₁)
      (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
      ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
succ₂ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) ∘ₗ
      (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A =
    HMul.hMul (β := M₁ →ₗ[R] M₁)
      (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
      ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
⊢ (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ (n + 1)) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
have succ₃ : HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n ∘ₗ
    (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A =
  HMul.hMul (β := M₁ →ₗ[R] M₁)
    (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
    ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
Tactic: rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_4
inst_1 : Fintype n_1
inst_2 : DecidableEq n_1
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n_1 R M₁
A : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n
succ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
succ₁ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n * A) =
    HMul.hMul (β := M₁ →ₗ[R] M₁)
      (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
      ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
succ₂ :
  (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ n) ∘ₗ
      (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A =
    HMul.hMul (β := M₁ →ₗ[R] M₁)
      (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
      ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
succ₃ :
  HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n ∘ₗ
      (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A =
    HMul.hMul (β := M₁ →ₗ[R] M₁)
      (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n)
      ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁)
⊢ (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) (A ^ (n + 1)) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n + 1)
have succ₄ : Eq (α := M₁ →ₗ[R] M₁)
  (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n ∘ₗ
    (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A)
  (HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n ∘ₗ
    (toLin v₁ v₁ : (a : Matrix n_1 n_1 R) → M₁ →ₗ[R] M₁) A)
Tactic: rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
A : Matrix n n R
k : ℕ
⊢ (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (A ^ k) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) k
have zero : (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (HPow.hPow (β := ℕ) A 0) =
  HPow.hPow (α := M₁ →ₗ[R] M₁) (β := ℕ) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) 0
Tactic: induction k with
  | zero => simp only [pow_zero, toLin_one, End.one_eq_id]
  | succ n ih => rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
A : Matrix n n R
k : ℕ
zero :
  (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (HPow.hPow (β := ℕ) A 0) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) (β := ℕ) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) 0
⊢ (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (A ^ k) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) k
have succ : ∀ (n_1 : ℕ)
  (ih :
    (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (A ^ n_1) =
      HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) n_1),
  (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (A ^ (n_1 + 1)) =
    HPow.hPow (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A : M₁ →ₗ[R] M₁) (n_1 + 1)
Tactic: induction k with
  | zero => simp only [pow_zero, toLin_one, End.one_eq_id]
  | succ n ih => rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
Cleared hypotheses: k