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
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₂ : Type u_6
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Finite m
v₁ : Basis n R R
v₂ : Basis m R M₂
x : M₂
⊢ Eq (α := Matrix m n R) ((toMatrix v₁ v₂ : (a : R →ₗ[R] M₂) → Matrix m n R) (toSpanSingleton R M₂ x) : Matrix m n R)
    (vecMulVec (⇑((v₂.repr : (a : M₂) → m →₀ R) x : m →₀ R) : (a : m) → R) (⇑v₁ : (a : n) → R) : Matrix m n R)
have a : ∀ (i : m) (j : n),
  Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₂ : (a : R →ₗ[R] M₂) → Matrix m n R) (toSpanSingleton R M₂ x) i j : R)
    (vecMulVec (⇑((v₂.repr : (a : M₂) → m →₀ R) x : m →₀ R) : (a : m) → R) (⇑v₁ : (a : n) → R) i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Finite m
f : M₁ →ₗ[R] R
x : M₂
⊢ Eq (α := Matrix m n R) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) (f.smulRight x) : Matrix m n R)
    (vecMulVec (⇑((v₂.repr : (a : M₂) → m →₀ R) x : m →₀ R) : (a : m) → R)
        (Function.comp.{u_4 + 1, u_5 + 1, u_1 + 1} (β := M₁) (⇑f : (a : M₁) → R) (⇑v₁ : (a : n) → M₁)) :
      Matrix m n R)
have a : ∀ (i : m) (j : n),
  Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) (f.smulRight x) i j : R)
    (vecMulVec (⇑((v₂.repr : (a : M₂) → m →₀ R) x : m →₀ R) : (a : m) → R)
        (Function.comp.{u_4 + 1, u_5 + 1, u_1 + 1} (β := M₁) (⇑f : (a : M₁) → R) (⇑v₁ : (a : n) → M₁)) i j :
      R)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
v : M₁
⊢ Eq.{u_6 + 1} (α := M₂)
    ((v₂.equivFun.symm : (a : m → R) → M₂)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
            (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R) :
          m → R) :
      M₂)
    (∑ j : m,
        HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₂ : (a : m) → M₂) j : M₂) :
      M₂)
have rw : Eq.{u_6 + 1} (α := M₂)
  ((v₂.equivFun.symm : (a : m → R) → M₂) (M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) : M₂)
  (∑ j : m,
      HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
        ((v₂ : (a : m) → M₂) j : M₂) :
    M₂)
Tactic: rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
v : M₁
rw :
  Eq.{u_6 + 1} (α := M₂)
    ((v₂.equivFun.symm : (a : m → R) → M₂) (M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) : M₂)
    (∑ j : m,
        HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₂ : (a : m) → M₂) j : M₂) :
      M₂)
⊢ Eq.{u_6 + 1} (α := M₂)
    ((v₂.equivFun.symm : (a : m → R) → M₂)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
            (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R) :
          m → R) :
      M₂)
    (∑ j : m,
        HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₂ : (a : m) → M₂) j : M₂) :
      M₂)
have rw₁ : Eq.{u_6 + 1} (α := M₂)
  (∑ i : m,
    HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) i)
      ((v₂ : (a : m) → M₂) i : M₂))
  (∑ j : m,
    HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
      ((v₂ : (a : m) → M₂) j : M₂))
Tactic: rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
i : n
⊢ Eq.{u_6 + 1} (α := M₂)
    ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁) :
      M₂)
    (∑ j : m, HSMul.hSMul (β := M₂) (M j i) ((v₂ : (a : m) → M₂) j : M₂) : M₂)
have rw : ∀ (j : m) (_hj : Membership.mem (γ := Finset m) Finset.univ j),
  HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) i) : n →₀ R) : (a : n) → R)) j)
      ((v₂ : (a : m) → M₂) j : M₂) =
    HSMul.hSMul (β := M₂) (M j i) ((v₂ : (a : m) → M₂) j : M₂)
Tactic: rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj ↦ ?_]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
i : n
j : m
_hj : Membership.mem (γ := Finset m) Finset.univ j
⊢ HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) i) : n →₀ R) : (a : n) → R)) j)
      ((v₂ : (a : m) → M₂) j : M₂) =
    HSMul.hSMul (β := M₂) (M j i) ((v₂ : (a : m) → M₂) j : M₂)
have h₀ : ∀ (b : n),
  Membership.mem (γ := Finset n) Finset.univ b →
    b ≠ i → HMul.hMul (β := R) (M j b) ((Finsupp.single i 1 : (a : n) → R) b : R) = 0
Tactic: rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same,
    mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
i : n
j : m
_hj : Membership.mem (γ := Finset m) Finset.univ j
h₀ :
  ∀ (b : n),
    Membership.mem (γ := Finset n) Finset.univ b →
      b ≠ i → HMul.hMul (β := R) (M j b) ((Finsupp.single i 1 : (a : n) → R) b : R) = 0
⊢ HSMul.hSMul (β := M₂) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) i) : n →₀ R) : (a : n) → R)) j)
      ((v₂ : (a : m) → M₂) j : M₂) =
    HSMul.hSMul (β := M₂) (M j i) ((v₂ : (a : m) → M₂) j : M₂)
have h₁ : i ∉ Finset.univ → HMul.hMul (β := R) (M j i) ((Finsupp.single i 1 : (a : n) → R) i : R) = 0
Tactic: rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same,
    mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
i : n
j : m
_hj : Membership.mem (γ := Finset m) Finset.univ j
i' : n
h : Membership.mem (γ := Finset n) Finset.univ i'
i'_ne : i' ≠ i
⊢ HMul.hMul (β := R) (M j i') ((Finsupp.single i 1 : (a : n) → R) i' : R) = 0
have h₀ : M j i' * 0 = 0
Tactic: rw [Finsupp.single_eq_of_ne i'_ne, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
i : n
j : m
_hj : Membership.mem (γ := Finset m) Finset.univ j
i' : n
h : Membership.mem (γ := Finset n) Finset.univ i'
i'_ne : i' ≠ i
h₀ : M j i' * 0 = 0
⊢ HMul.hMul (β := R) (M j i') ((Finsupp.single i 1 : (a : n) → R) i' : R) = 0
have h₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Finsupp.single_eq_of_ne i'_ne, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
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 : Matrix m n R
i : n
j : m
_hj : Membership.mem (γ := Finset m) Finset.univ j
h : i ∉ Finset.univ
⊢ HMul.hMul (β := R) (M j i) ((Finsupp.single i 1 : (a : n) → R) i : R) = 0
have this : Membership.mem (γ := Finset n) Finset.univ i
Tactic: have := Finset.mem_univ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
m : Type u_3
n : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst_2 : Finite m
inst_3 : CommRing R
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
⊢ Eq.{u_9 + 1} (α := M₂) ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) A : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂)
      (0 : M₂) ↔
    ∀ (j : m), (A *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)) j = 0
have have : ∀ (this : Fintype m),
  Eq.{u_9 + 1} (α := M₂) ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) A : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂)
      (0 : M₂) ↔
    ∀ (j : m), (A *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)) j = 0
Tactic: have := Fintype.ofFinite m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
m : Type u_3
n : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst_2 : Finite m
inst_3 : CommRing R
inst_4 : AddCommGroup M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
this : Fintype m
⊢ Eq.{u_9 + 1} (α := M₂) ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) A : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x : M₂)
      (0 : M₂) ↔
    ∀ (j : m), (A *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)) j = 0
have rw : Eq.{u_9 + 1} (α := M₂)
    (∑ j : m,
      HSMul.hSMul (β := M₂) ((A *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)) j)
        ((v₂ : (a : m) → M₂) j : M₂))
    0 ↔
  ∀ (j : m), (A *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)) j = 0
Tactic: rw [toLin_apply]
-- 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
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
⊢ (toMatrix v₁ v₃ : (a : M₁ →ₗ[R] M₃) → Matrix l n R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix l m R) (β := Matrix m n R)
      ((toMatrix v₂ v₃ : (a : M₂ →ₗ[R] M₃) → Matrix l m R) f : Matrix l m R)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) g : Matrix m n R)
have simp_rw : (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: simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply]
-- 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
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
⊢ (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)
have 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)
Tactic: rw [LinearEquiv.arrowCongr_comp _ v₂.equivFun, LinearMap.toMatrix'_comp]
-- 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
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)
⊢ (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)
have 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)
Tactic: rw [LinearEquiv.arrowCongr_comp _ v₂.equivFun, LinearMap.toMatrix'_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₁
f g : M₁ →ₗ[R] M₁
⊢ (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)
have 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)
Tactic: rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]
-- 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 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)
⊢ (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)
have 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)
Tactic: rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]
-- 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)
⊢ 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 : 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))
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 : ℕ
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))
⊢ 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₁ : 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)
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 : ℕ
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)
⊢ 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₂ : 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)
Tactic: rw [pow_succ, pow_succ, ih, ← toMatrix_mul]