awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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

Tactic:
simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply,
      LinearEquiv.apply_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, Module.Basis.toMatrix_apply, Module.Basis.equivFun_apply, LinearEquiv.apply_symm_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 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
a :
  ∀ (i j : ι),
    (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
      b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
⊢ Eq (α := Matrix ι ι S)
    ((RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) :
      Matrix ι ι S)
    (b.toMatrix fun (i : ι) ↦ (↑(v i) : M₂) : Matrix ι ι S)

Tactic:
ext
-- 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 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
i j : ι
a :
  (toMatrix (restrictScalars R₂ b) v).map (⇑(algebraMap R₂ S) : (a : R₂) → S) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₁ :
  (algebraMap R₂ S : (a : R₂) → S) (toMatrix (restrictScalars R₂ b) v i j) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₂ :
  (algebraMap R₂ S : (a : R₂) → S)
      ((((repr (restrictScalars R₂ b) : (a : ↥(span R₂ (Set.range (⇑b : (a : ι) → M₂)))) → ι →₀ R₂) (v j) : ι →₀ R₂) :
            (a : ι) → R₂)
          i :
        R₂) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₃ :
  (((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i = b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₄ a₅ :
  Eq.{u_9 + 1} (α := S) ((((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i : S)
    ((((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i : S)
⊢ (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j

Tactic:
rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]

Premises used: RingHom.mapMatrix_apply, Matrix.map_apply, Module.Basis.restrictScalars_repr_apply, 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
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Finite ι'
a : ∀ (i : ι') (j : ι), (toMatrix b b' : (a : M →ₗ[R] M) → Matrix ι' ι R) id i j = b'.toMatrix (⇑b : (a : ι) → M) i j
⊢ Eq (α := Matrix ι' ι R) ((toMatrix b b' : (a : M →ₗ[R] M) → Matrix ι' ι R) id : Matrix ι' ι R)
    (b'.toMatrix (⇑b : (a : ι) → M) : Matrix ι' ι R)

Tactic:
ext i
-- 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
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Finite ι'
i : ι'
j : ι
⊢ (toMatrix b b' : (a : M →ₗ[R] M) → Matrix ι' ι R) id i j = b'.toMatrix (⇑b : (a : ι) → M) i j

Tactic:
apply LinearMap.toMatrix_apply

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι' : 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
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
haveI :
  ∀ (this : DecidableEq κ'),
    Eq (α := M →ₗ[R] N)
      ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
          (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
            ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
        M →ₗ[R] N)
      ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)

Tactic:
haveI := Classical.decEq κ'
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι' : 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
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
this : DecidableEq κ'
rw :
  (toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) =
    f
rw₁ :
  (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ
      (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) =
    f
rw₂ : (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ f = f
rw₃ : LinearMap.id ∘ₗ f = f
rw₄ rw₅ : f = f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)

Tactic:
rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

Premises used: Module.Basis.toLin_toMatrix, Matrix.toLin_mul, Matrix.toLin_toMatrix, LinearMap.id_comp
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Fintype κ
inst_7 : Finite ι
inst_8 : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
⊢ HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' κ R) (b₁.toMatrix (⇑b₂ : (a : ι') → M))
      ((toMatrix b₃ b₂ : (a : N →ₗ[R] M) → Matrix ι' κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A) :
        Matrix ι' κ R) =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)

Tactic:
have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Fintype κ
inst_7 : Finite ι
inst_8 : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this :
  HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' κ R) (b₁.toMatrix (⇑b₂ : (a : ι') → M))
      ((toMatrix b₃ b₂ : (a : N →ₗ[R] M) → Matrix ι' κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A) :
        Matrix ι' κ R) =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
        (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)),
    HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
      (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
⊢ HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)

Tactic:
rwa [LinearMap.toMatrix_toLin] at this

Premises used: LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Fintype ι
inst_7 : Finite κ'
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
rw :
  (toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) =
    f
rw₁ :
  (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) ∘ₗ
      (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) =
    f
rw₂ : f ∘ₗ (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) = f
rw₃ : f ∘ₗ LinearMap.id = f
rw₄ rw₅ : f = f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) :
      M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N) ((toMatrix b c' : (a : M →ₗ[R] N) → Matrix κ' ι R) f) : M →ₗ[R] N)

Tactic:
rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]

Premises used: Module.Basis.toLin_toMatrix, Matrix.toLin_mul, Matrix.toLin_toMatrix, LinearMap.comp_id
-- 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
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : Fintype κ'
inst_9 : DecidableEq ι
inst_10 : DecidableEq ι'
intro :
  ∀ (val : Fintype κ),
    HMul.hMul (β := Matrix ι' ι R)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
        (b'.toMatrix (⇑b : (a : ι) → M)) =
      (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
⊢ HMul.hMul (β := Matrix ι' ι R)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f

Tactic:
cases nonempty_fintype κ

Premises used: nonempty_fintype
-- 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
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : Fintype κ'
inst_9 : DecidableEq ι
inst_10 : DecidableEq ι'
val : Fintype κ
intro :
  HMul.hMul (α := Matrix κ ι' R) (β := Matrix ι' ι R)
      ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f : Matrix κ ι' R) (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
intro₁ intro₂ :
  Eq (α := Matrix κ ι R) ((toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f : Matrix κ ι R)
    ((toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f : Matrix κ ι R)
⊢ HMul.hMul (β := Matrix ι' ι R)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f

Tactic:
rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]

Premises used: linearMap_toMatrix_mul_basis_toMatrix, basis_toMatrix_mul_linearMap_toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
intro :
  ∀ (val : Fintype κ),
    HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
      (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
⊢ HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)

Tactic:
cases nonempty_fintype κ

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val : Fintype κ
⊢ HMul.hMul (α := Matrix κ ι R) (β := Matrix ι ι' R)
      ((toMatrix b₁ b₃ : (a : M →ₗ[R] N) → Matrix κ ι R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A) :
        Matrix κ ι R)
      (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)

Tactic:
have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val : Fintype κ
this :
  HMul.hMul (α := Matrix κ ι R) (β := Matrix ι ι' R)
      ((toMatrix b₁ b₃ : (a : M →ₗ[R] N) → Matrix κ ι R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A) :
        Matrix κ ι R)
      (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
intro intro₁ intro₂ intro₃ :
  ∀
    (this :
      HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
        (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)),
    HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
      (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
⊢ HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)

Tactic:
rwa [LinearMap.toMatrix_toLin] at this

Premises used: LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
simp :
  Eq (α := Matrix ι ι R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
      Matrix ι ι R)
    ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
        (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
      Matrix ι ι R)
⊢ b.toMatrix (⇑(Pi.basisFun R ι) : (a : ι) → ι → R) * A =
    (of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i

Tactic:
simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']

Premises used: Matrix.toLin_eq_toLin', Pi.basisFun, basis_toMatrix_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
a :
  ∀ (i j : ι),
    Eq.{u_5 + 1} (α := R)
      ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
          ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
        R)
      ((of : (a : ι → ι → R) → Matrix ι ι R)
          (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
        R)
⊢ Eq (α := Matrix ι ι R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
      Matrix ι ι R)
    ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
        (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
      Matrix ι ι R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
a :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R)
              ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
                ((Pi.basisFun R ι : (a : ι) → ι → R) j : ι → R)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₁ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ (Pi.basisFun R ι : (a : ι) → ι → R) j) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₂ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ Pi.single (M := fun (j : ι) ↦ R) j 1) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₃ :
  Eq.{u_5 + 1} (α := R) ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₄ a₅ :
  Eq.{u_5 + 1} (α := R) ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
⊢ Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)

Tactic:
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]

Premises used: Matrix.mulVec_single_one, Matrix.of_apply, Pi.basisFun_apply, Matrix.toLin'_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Basis
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
simp :
  Eq (α := Matrix ι ι R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
      Matrix ι ι R)
    ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
        (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
      Matrix ι ι R)
a :
  ∀ (i j : ι),
    Eq.{u_5 + 1} (α := R)
      ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
          ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
        R)
      ((of : (a : ι → ι → R) → Matrix ι ι R)
          (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
        R)
⊢ b.toMatrix (⇑(Pi.basisFun R ι) : (a : ι) → ι → R) * A =
    (of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i

Tactic:
classical
  simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
  ext i j
  rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]

Premises used: Matrix.mulVec_single_one, Matrix.of_apply, Pi.basisFun_apply, Matrix.toLin_eq_toLin', Matrix.toLin'_apply, LinearMap.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
inst_3 : Fintype ι'
inst_4 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
a :
  ∀ (i j : ι'),
    (b.reindex e).toMatrix v i j =
      (reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) i j
⊢ (b.reindex e).toMatrix v =
    (reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))

Tactic:
ext
-- 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
inst_3 : Fintype ι'
inst_4 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i j : ι'
⊢ (b.reindex e).toMatrix v i j =
    (reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) i j

Tactic:
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply,
    Matrix.reindex_apply, Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply,
    Finsupp.mapDomain_equiv_apply]

Premises used: Equiv.apply_symm_apply, Matrix.reindex_apply, Module.Basis.repr_reindex, Module.Basis.toMatrix_apply, Finsupp.mapDomain_equiv_apply, Matrix.reindexAlgEquiv_apply, Function.comp_apply, Matrix.submatrix_apply