awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
rw :
  (toMatrix' : (a : (n → R) →ₗ[R] l → R) → Matrix l n R)
      ((v₂.equivFun.arrowCongr v₃.equivFun : (a : M₂ →ₗ[R] M₃) → (m → R) →ₗ[R] l → R) f ∘ₗ
        (v₁.equivFun.arrowCongr v₂.equivFun : (a : M₁ →ₗ[R] M₂) → (n → R) →ₗ[R] m → R) g) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix' : (a : (m → R) →ₗ[R] l → R) → Matrix l m R)
          ((v₂.equivFun.arrowCongr v₃.equivFun : (a : M₂ →ₗ[R] M₃) → (m → R) →ₗ[R] l → R) f) :
        Matrix l m R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R)
          ((v₁.equivFun.arrowCongr v₂.equivFun : (a : M₁ →ₗ[R] M₂) → (n → R) →ₗ[R] m → R) g) :
        Matrix m n R)
rw₁ rw₂ :
  HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix' : (a : (m → R) →ₗ[R] l → R) → Matrix l m R)
          ((v₂.equivFun.arrowCongr v₃.equivFun : (a : M₂ →ₗ[R] M₃) → (m → R) →ₗ[R] l → R) f) :
        Matrix l m R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R)
          ((v₁.equivFun.arrowCongr v₂.equivFun : (a : M₁ →ₗ[R] M₂) → (n → R) →ₗ[R] m → R) g) :
        Matrix m n R) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix' : (a : (m → R) →ₗ[R] l → R) → Matrix l m R)
          ((v₂.equivFun.arrowCongr v₃.equivFun : (a : M₂ →ₗ[R] M₃) → (m → R) →ₗ[R] l → R) f) :
        Matrix l m R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R)
          ((v₁.equivFun.arrowCongr v₂.equivFun : (a : M₁ →ₗ[R] M₂) → (n → R) →ₗ[R] m → R) g) :
        Matrix m n R)
⊢ (toMatrix' : (a : (n → R) →ₗ[R] l → R) → Matrix l n R)
      ((v₁.equivFun.arrowCongr v₃.equivFun : (a : M₁ →ₗ[R] M₃) → (n → R) →ₗ[R] l → R) (f ∘ₗ g)) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix' : (a : (m → R) →ₗ[R] l → R) → Matrix l m R)
          ((v₂.equivFun.arrowCongr v₃.equivFun : (a : M₂ →ₗ[R] M₃) → (m → R) →ₗ[R] l → R) f) :
        Matrix l m R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R)
          ((v₁.equivFun.arrowCongr v₂.equivFun : (a : M₁ →ₗ[R] M₂) → (n → R) →ₗ[R] m → R) g) :
        Matrix m n R)

Tactic:
rw [LinearEquiv.arrowCongr_comp _ v₂.equivFun, LinearMap.toMatrix'_comp]

Premises used: LinearMap.toMatrix'_comp, LinearEquiv.arrowCongr_comp, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 g : M₁ →ₗ[R] M₁
rw :
  (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix n n R) (β := 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) g : Matrix n n R)
rw₁ rw₂ :
  HMul.hMul (α := Matrix n n R) (β := 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) g : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := 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) g : Matrix n n R)
⊢ (toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f * g) =
    HMul.hMul (α := Matrix n n R) (β := 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) g : Matrix n n R)

Tactic:
rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Premises used: Module.End.mul_eq_comp, LinearMap.toMatrix_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₁
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
succ₃ 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)
⊢ 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:
rw [pow_succ, pow_succ, ih, ← toMatrix_mul]

Premises used: pow_succ, LinearMap.toMatrix_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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))
⊢ 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)

Tactic:
induction k with
  | zero => simp
  | succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]

Premises used: pow_succ, LinearMap.toMatrix_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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)
⊢ 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₃)

Tactic:
apply (LinearMap.toMatrix v₁ v₃).injective

Premises used: LinearEquiv.injective, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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)
⊢ 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 _
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 :
  (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)
⊢ 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:
rw [LinearMap.toMatrix_comp v₁ v₂ v₃]

Premises used: LinearMap.toMatrix_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 * 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)

Tactic:
rw [LinearMap.toMatrix_toLin]

Premises used: LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 * 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)
⊢ 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]

Premises used: LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 * B = A * B
⊢ 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]

Premises used: LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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)
⊢ (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:
repeat' rw [LinearMap.toMatrix_toLin]

Premises used: LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
⊢ (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:
simp only [pow_zero, toLin_one, End.one_eq_id]

Premises used: Module.End.one_eq_id, pow_zero, Matrix.toLin_one
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₁)
succ₄ 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)
⊢ (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)

Tactic:
rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, pow_succ, Matrix.toLin_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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)
⊢ (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

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]

Premises used: Module.End.mul_eq_comp, Module.End.one_eq_id, pow_succ, Matrix.toLin_mul, pow_zero, Matrix.toLin_one, Matrix.zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
x : M₁
rw :
  Eq.{u_7 + 1} (α := 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 :
          (a : M₁) → M₃)
        x :
      M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)
rw₁ rw₂ :
  Eq.{u_7 + 1} (α := M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)
⊢ Eq.{u_7 + 1} (α := M₃)
    ((((toLin v₁ v₃ : (a : Matrix l n R) → M₁ →ₗ[R] M₃) (A * B) : M₁ →ₗ[R] M₃) : (a : M₁) → M₃) x : M₃)
    ((((toLin v₂ v₃ : (a : Matrix l m R) → M₂ →ₗ[R] M₃) A : M₂ →ₗ[R] M₃) : (a : M₂) → M₃)
        ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) B : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) :
      M₃)

Tactic:
rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Matrix.toLin_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
rw : (((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (M' * M) : M₁ →ₗ[R] M₁) : (a : M₁) → M₁) x = x
rw₁ : ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1 : (a : M₁) → M₁) x = x
rw₂ : (LinearMap.id : (a : M₁) → M₁) x = x
rw₃ rw₄ : x = x
⊢ (((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁)
      ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂) =
    x

Tactic:
rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]

Premises used: Matrix.toLin_mul_apply, LinearMap.id_apply, Matrix.toLin_one