awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
⊢ (e.toMatrix v)ᵀ j = (⇑((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R)

Tactic:
funext fun _ => rfl

Premises used: funext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
v : ι → M
a :
  ∀ (i j : ι),
    e.toMatrix v i j =
      (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j
⊢ e.toMatrix v = (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
v : ι → M
i j : ι
a :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
    ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j : R)
a₁ :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
    ((((e.repr : (a : M) → ι →₀ R)
              ((((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v : M →ₗ[R] M) : (a : M) → M) ((e : (a : ι) → M) j : M)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
a₂ a₃ :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
    ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i : R)
⊢ e.toMatrix v i j =
    (LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v) i j

Tactic:
rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]

Premises used: Module.Basis.toMatrix_apply, Module.Basis.constr_basis, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Finite ι
h : ∀ (M : ι → ι → R) (i j : ι), toMatrix (Pi.basisFun R ι) M i j = Mᵀ i j
⊢ Eq (α := (v : ι → ι → R) → Matrix ι ι R) (toMatrix (Pi.basisFun R ι)) transpose

Tactic:
ext M i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Finite ι
M : ι → ι → R
i j : ι
⊢ toMatrix (Pi.basisFun R ι) M i j = Mᵀ i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : DecidableEq ι
unfold :
  Eq (α := Matrix ι ι R)
    (fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i) 1
⊢ Eq (α := Matrix ι ι R) (e.toMatrix (⇑e : (a : ι) → M)) 1

Tactic:
unfold Basis.toMatrix

Premises used: Module.Basis.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : DecidableEq ι
a :
  ∀ (i j : ι),
    Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      (1 i j : R)
⊢ Eq (α := Matrix ι ι R)
    (fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i) 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : DecidableEq ι
i j : ι
⊢ Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) ((e : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i : R) (1 i j : R)

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

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
a :
  ∀ (i' : ι) (k : ι'),
    e.toMatrix (update (β := fun (a : ι') ↦ M) v j x) i' k =
      (e.toMatrix v).updateCol j (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' k
⊢ e.toMatrix (update (β := fun (a : ι') ↦ M) v j x) =
    (e.toMatrix v).updateCol j (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)

Tactic:
ext i' k
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
a :
  Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    (if k = j then (((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i'
      else (((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' :
      R)
⊢ e.toMatrix (update (β := fun (a : ι') ↦ M) v j x) i' k =
    (e.toMatrix v).updateCol j (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' k

Tactic:
rw [Basis.toMatrix, Matrix.updateCol_apply, e.toMatrix_apply]

Premises used: Matrix.updateCol_apply, Module.Basis.toMatrix, Module.Basis.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
pos :
  ∀ (h : k = j),
    Eq.{u_5 + 1} (α := R)
      ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
      ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
neg :
  ∀ (h : ¬k = j),
    Eq.{u_5 + 1} (α := R)
      ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
      ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    (if k = j then (((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i'
      else (((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' :
      R)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
pos :
  Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x j) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
pos₁ pos₂ :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i' : R)

Tactic:
rw [h, update_self j x v]

Premises used: Function.update_self
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
neg neg₁ :
  Eq.{u_5 + 1} (α := R) ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)
⊢ Eq.{u_5 + 1} (α := R)
    ((((e.repr : (a : M) → ι →₀ R) (update (β := fun (a : ι') ↦ M) v j x k) : ι →₀ R) : (a : ι) → R) i' : R)
    ((((e.repr : (a : M) → ι →₀ R) (v k) : ι →₀ R) : (a : ι) → R) i' : R)

Tactic:
rw [update_of_ne h]

Premises used: Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
a : ∀ (i j : ι), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) = Matrix.diagonal (Units.val ∘ w)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
pos : ∀ (h : i = j), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
neg : ∀ (h : ¬i = j), e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]

Premises used: Module.Basis.toMatrix_apply, Units.smul_def, Module.Basis.unitsSMul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ e.toMatrix (⇑(e.unitsSMul w) : (a : ι) → M₂) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]

Premises used: Module.Basis.toMatrix_apply, Units.smul_def, Module.Basis.unitsSMul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂
hw : ∀ (i : ι), IsUnit (w i)
⊢ e.toMatrix (⇑(e.isUnitSMul hw) : (a : ι) → M₂) = Matrix.diagonal w

Tactic:
e.toMatrix_unitsSMul _

Premises used: Module.Basis.toMatrix_unitsSMul
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
G : Type u_9
inst_3 : Group G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
g : G
⊢ (g • e).toMatrix v = e.toMatrix (g⁻¹ • v)

Tactic:
rfl

Premises used: Module.Basis.map, Module.Basis.toMatrix, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst_3 : Fintype ι
simp_rw :
  ∑ x : ι,
      HSMul.hSMul.{u_5, u_6, u_6} (α := R) (β := M) ((((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) x : R)
        ((e : (a : ι) → M) x : M) =
    v j
⊢ ∑ i : ι, HSMul.hSMul (β := M) (e.toMatrix v i j) ((e : (a : ι) → M) i : M) = v j

Tactic:
simp_rw [e.toMatrix_apply, e.sum_repr]

Premises used: Module.Basis.toMatrix_apply, Module.Basis.sum_repr
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst : CommSemiring R₁
inst_1 : Semiring S
inst_2 : Algebra R₁ S
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
a :
  ∀ (i j : ι),
    b.toMatrix (x • w) i j =
      HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
        (b.toMatrix w) i j
⊢ b.toMatrix (x • w) =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst : CommSemiring R₁
inst_1 : Semiring S
inst_2 : Algebra R₁ S
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i j : ι
a :
  mulVec (n := ι) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x)
      (⇑((b.repr : (a : S) → ι →₀ R₁) (w j) : ι →₀ R₁) : (a : ι) → R₁) i =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w) i j
⊢ b.toMatrix (x • w) i j =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w) i j

Tactic:
rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]

Premises used: Module.Basis.toMatrix_apply, Algebra.leftMulMatrix_mulVec_repr, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst : CommSemiring R₁
inst_1 : Semiring S
inst_2 : Algebra R₁ S
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i j : ι
⊢ mulVec (n := ι) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x)
      (⇑((b.repr : (a : S) → ι →₀ R₁) (w j) : ι →₀ R₁) : (a : ι) → R₁) i =
    HMul.hMul (α := Matrix ι ι R₁) ((Algebra.leftMulMatrix b : (a : S) → Matrix ι ι R₁) x : Matrix ι ι R₁)
      (b.toMatrix w) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
h : ∀ (i : ι'), ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i
⊢ (⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) = v

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst : CommSemiring R
S : Type u_9
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
h : ((⇑b : (a : ι) → S) ⬝ᵥ fun (i_1 : ι) ↦ (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) i_1 i) = v i
h₁ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S)
        ((b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S) x i : S) =
    v i
h₂ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) x : S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) =
    v i
h₃ :
  ∑ x : ι,
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (b.toMatrix v x i) : S) ((b : (a : ι) → S) x : S) =
    v i
h₄ : ∑ x : ι, HSMul.hSMul (β := S) (b.toMatrix v x i) ((b : (a : ι) → S) x : S) = v i
⊢ ((⇑b : (a : ι) → S) ᵥ* (b.toMatrix v).map (⇑(algebraMap R S) : (a : R) → S)) i = v i

Tactic:
simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]

Premises used: dotProduct, Matrix.vecMul, Matrix.map_apply, Module.Basis.sum_toMatrix_smul_self, Algebra.smul_def, Algebra.commutes
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Finite ι
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
v : Basis ι' R M
i : ι'
intro :
  ∀ (val : Fintype ι),
    Eq.{u_6 + 1} (α := M)
      ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
          ((v : (a : ι') → M) i : M) :
        M)
      ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
⊢ Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : Basis ι R M
inst_3 : Finite ι
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
v : Basis ι' R M
i : ι'
val : Fintype ι
intro :
  Eq.{u_6 + 1} (α := M)
    (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)
intro₁ :
  Eq.{u_6 + 1} (α := M)
    (∑ j : ι, HSMul.hSMul (β := M) (e.toMatrix (⇑v : (a : ι') → M) j i) ((e : (a : ι) → M) j : M) : M)
    ((v : (a : ι') → M) i : M)
intro₂ intro₃ : Eq.{u_6 + 1} (α := M) ((v : (a : ι') → M) i : M) ((v : (a : ι') → M) i : M)
⊢ Eq.{u_6 + 1} (α := M)
    ((((toLin v e : (a : Matrix ι ι' R) → M →ₗ[R] M) (e.toMatrix (⇑v : (a : ι') → M)) : M →ₗ[R] M) : (a : M) → M)
        ((v : (a : ι') → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((v : (a : ι') → M) i : M) : M)

Tactic:
rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

Premises used: LinearMap.id_apply, Matrix.toLin_self, Module.Basis.sum_toMatrix_smul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
v w : ι → M
a : ∀ (i j : ι), e.toMatrix (v + w) i j = (e.toMatrix v + e.toMatrix w) i j
⊢ e.toMatrix (v + w) = e.toMatrix v + e.toMatrix w

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i_1 : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
a :
  (HAdd.hAdd (α := ι →₀ R) (β := ι →₀ R) ((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R)
          ((e.repr : (a : M) → ι →₀ R) (w j) : ι →₀ R) :
        (a : ι) → R)
      i =
    e.toMatrix v i j + e.toMatrix w i j
⊢ e.toMatrix (v + w) i j = (e.toMatrix v + e.toMatrix w) i j

Tactic:
rw [Matrix.add_apply, e.toMatrix_apply, Pi.add_apply, map_add]

Premises used: Matrix.add_apply, map_add, Pi.add_apply, Module.Basis.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i_1 : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ (HAdd.hAdd (α := ι →₀ R) (β := ι →₀ R) ((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R)
          ((e.repr : (a : M) → ι →₀ R) (w j) : ι →₀ R) :
        (a : ι) → R)
      i =
    e.toMatrix v i j + e.toMatrix w i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
c : R
v : ι → M
a : ∀ (i j : ι), e.toMatrix (c • v) i j = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j
⊢ e.toMatrix (c • v) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i_1 : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
a :
  (HSMul.hSMul (β := ι →₀ R) c ((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j
⊢ e.toMatrix (c • v) i j = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j

Tactic:
rw [e.toMatrix_apply, Pi.smul_apply, map_smul]

Premises used: Module.Basis.toMatrix_apply, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i_1 : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ (HSMul.hSMul (β := ι →₀ R) c ((e.repr : (a : M) → ι →₀ R) (v j) : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (e.toMatrix v) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
h :
  ∀ (j : ι),
    (fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M))
        (e.toMatrix v) j =
      v j
⊢ (fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M))
      (e.toMatrix v) =
    v

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
j : ι
⊢ (fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M))
      (e.toMatrix v) j =
    v j

Tactic:
e.sum_toMatrix_smul_self v j

Premises used: Module.Basis.sum_toMatrix_smul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v_1 : ι' → M
i : ι
j_1 : ι'
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
j : ι
⊢ (fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M))
      (e.toMatrix v) j =
    v j

Tactic:
exact e.sum_toMatrix_smul_self v j

Premises used: Module.Basis.sum_toMatrix_smul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst_3 : CommRing R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
e_1 : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst_6 : Fintype ι
e : Basis ι R M
m : Matrix ι ι R
a :
  ∀ (k l : ι),
    e.toMatrix
        ((fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M)) m) k
        l =
      m k l
⊢ e.toMatrix
      ((fun (m : Matrix ι ι R) (j : ι) ↦ (∑ i : ι, HSMul.hSMul (β := M) (m i j) ((e : (a : ι) → M) i : M) : M)) m) =
    m

Tactic:
ext k l