awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
h :
  ∀ (i : m),
    Eq.{u_1 + 1} (α := R)
      (mulVec.{u_1, u_3, u_4} (n := n) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)
          (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i :
        R)
      ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)
⊢ Eq (α := m → R)
    (mulVec.{u_1, u_3, u_4} (n := n) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)
      (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
    (⇑((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
h :
  Eq.{u_1 + 1} (α := R)
    ((((v₂.repr : (a : M₂) → m →₀ R)
              ((f : (a : M₁) → M₂)
                ((v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) :
                  M₁)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R)
    (mulVec.{u_1, u_3, u_4} (n := n) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)
        (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)

Tactic:
rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
    LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]

Premises used: LinearEquiv.trans_apply, LinearEquiv.arrowCongr_apply, Module.Basis.equivFun_apply, Matrix.toLin'_apply, Matrix.toLin'_toMatrix', LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
h : (v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) = x
⊢ Eq.{u_1 + 1} (α := R)
    ((((v₂.repr : (a : M₂) → m →₀ R)
              ((f : (a : M₁) → M₂)
                ((v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) :
                  M₁)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ (v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) = x

Tactic:
exact v₁.equivFun.symm_apply_apply x

Premises used: LinearEquiv.symm_apply_apply, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
x : M₁
rw :
  mulVec.{u_1, u_3, u_4} (n := n)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M))
      (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) =
    M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
rw₁ rw₂ :
  M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) =
    M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
⊢ (⇑((v₂.repr : (a : M₂) → m →₀ R)
            ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x) :
          m →₀ R) :
      (a : m) → R) =
    M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)

Tactic:
rw [← toMatrix_mulVec_repr v₁, toMatrix_toLin]

Premises used: LinearMap.toMatrix_mulVec_repr, LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype l
inst_6 : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
a :
  ∀ (i j : l),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix b' b : (a : M₂ →ₗ[R] M₁) → Matrix l l R) (↑(b'.equiv b (Equiv.refl l)) : M₂ →ₗ[R] M₁) i j : R)
      (1 i j : R)
⊢ Eq (α := Matrix l l R)
    ((toMatrix b' b : (a : M₂ →ₗ[R] M₁) → Matrix l l R) (↑(b'.equiv b (Equiv.refl l)) : M₂ →ₗ[R] M₁) : Matrix l l R)
    (1 : Matrix l l R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype l
inst_6 : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b' b : (a : M₂ →ₗ[R] M₁) → Matrix l l R) (↑(b'.equiv b (Equiv.refl l)) : M₂ →ₗ[R] M₁) i j : R)
    (1 i j : R)

Tactic:
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst_8 : Group G
inst_9 : DistribMulAction G M₁
inst_10 : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
⊢ Eq (α := Matrix m n R) ((toMatrix (g • v₁) v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f : Matrix m n R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) (f ∘ₗ DistribSMul.toLinearMap R M₁ g) : Matrix m n R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst_8 : Group G
inst_9 : DistribMulAction G M₂
inst_10 : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
⊢ Eq (α := Matrix m n R) ((toMatrix v₁ (g • v₂) : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f : Matrix m n R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) (DistribSMul.toLinearMap R M₂ g⁻¹ ∘ₗ f) : Matrix m n R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M₃ →ₗ[R] M₂
g : M₁ ≃ₗ[R] M₃
⊢ Eq (α := Matrix m n R) ((toMatrix (v₁.map g) v₂ : (a : M₃ →ₗ[R] M₂) → Matrix m n R) f : Matrix m n R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) (f ∘ₗ (↑g : M₁ →ₗ[R] M₃)) : Matrix m n R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M₁ →ₗ[R] M₃
g : M₂ ≃ₗ[R] M₃
⊢ Eq (α := Matrix m n R) ((toMatrix v₁ (v₂.map g) : (a : M₁ →ₗ[R] M₃) → Matrix m n R) f : Matrix m n R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((↑g.symm : M₃ →ₗ[R] M₂) ∘ₗ f) : Matrix m n R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₂
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₂
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:
simp [toMatrix_apply, vecMulVec_apply, mul_comm]

Premises used: Matrix.vecMulVec_apply, mul_comm, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₂
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)
⊢ 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)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₂
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:
simpa [toMatrix_apply, vecMulVec_apply] using mul_comm _ _

Premises used: Matrix.vecMulVec_apply, mul_comm, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₂)
rw₁ 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₂))
⊢ 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₂)

Tactic:
rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, Matrix.toLin'_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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₂)
⊢ 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₂)

Tactic:
rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj ↦ ?_]

Premises used: Matrix.toLin_apply, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
h₁ : i ∉ Finset.univ → HMul.hMul (β := R) (M j i) ((Finsupp.single i 1 : (a : n) → R) i : 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₂)

Tactic:
rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same,
    mul_one]

Premises used: Finsupp.single_eq_same, dotProduct, Finset.sum_eq_single, mul_one, Matrix.mulVec, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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' ≠ i → HMul.hMul (β := R) (M j i') ((Finsupp.single i 1 : (a : n) → R) i' : R) = 0
⊢ Membership.mem (γ := Finset n) Finset.univ i' →
    i' ≠ i → HMul.hMul (β := R) (M j i') ((Finsupp.single i 1 : (a : n) → R) i' : R) = 0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
h₁ h₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (β := R) (M j i') ((Finsupp.single i 1 : (a : n) → R) i' : R) = 0

Tactic:
rw [Finsupp.single_eq_of_ne i'_ne, mul_zero]

Premises used: Finsupp.single_eq_of_ne, MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
⊢ Membership.mem (γ := Finset n) Finset.univ i

Tactic:
have := Finset.mem_univ i
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
this : Membership.mem (γ := Finset n) Finset.univ i
⊢ HMul.hMul (β := R) (M j i) ((Finsupp.single i 1 : (a : n) → R) i : R) = 0

Tactic:
contradiction
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₁
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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
⊢ 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:
rw [toLin_apply]

Premises used: Matrix.toLin_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
h : ∀ (j : m), (A *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)) j = 0
⊢ 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

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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₂)
      (∑ 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:
exact ⟨Fintype.linearIndependent_iff.mp v₂.linearIndependent _, fun h ↦ by simp [h]⟩
-- 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₂
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)
⊢ (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)

Tactic:
simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply]

Premises used: LinearEquiv.trans_apply, LinearMap.toMatrix