awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
M₃ : Type u_7
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
v₃ : Basis l R M₃
inst_10 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
rw : (((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) (M * M') : M₂ →ₗ[R] M₂) : (a : M₂) → M₂) x = x
rw₁ : ((toLin v₂ v₂ : (a : Matrix m m R) → M₂ →ₗ[R] M₂) 1 : (a : M₂) → M₂) x = x
rw₂ : (LinearMap.id : (a : M₂) → M₂) x = x
rw₃ rw₄ : x = x
⊢ (((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
      ((((toLin v₂ v₁ : (a : Matrix n m R) → M₂ →ₗ[R] M₁) M' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁) x : M₁) =
    x

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

Premises used: Matrix.toLin_mul_apply, LinearMap.id_apply, Matrix.toLin_one
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
⊢ Eq (α := Matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁) (AlgEquiv.symm (toMatrixAlgEquiv v₁)) (toLinAlgEquiv v₁)

Tactic:
rfl

Premises used: Matrix.toLinAlgEquiv, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
⊢ Eq (α := (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R) (AlgEquiv.symm (toLinAlgEquiv v₁)) (toMatrixAlgEquiv v₁)

Tactic:
rfl

Premises used: AlgEquiv.symm, LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
rw :
  (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
      ((AlgEquiv.symm (toLinAlgEquiv v₁) : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f) =
    f
rw₁ rw₂ : f = f
⊢ (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f) = f

Tactic:
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply, Matrix.toLinAlgEquiv_symm
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
rw :
  (AlgEquiv.symm (toLinAlgEquiv v₁) : (a : M₁ →ₗ[R] M₁) → Matrix n n R)
      ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M) =
    M
rw₁ rw₂ : M = M
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M) = M

Tactic:
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]

Premises used: AlgEquiv.symm_apply_apply, Matrix.toLinAlgEquiv_symm
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
i j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f i j : R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i : R)

Tactic:
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_apply]

Premises used: LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
j : n
⊢ Eq (α := n → R) (((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f)ᵀ j)
    (⇑((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R)

Tactic:
funext fun i ↦ f.toMatrix_apply _ _ i j

Premises used: funext, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
i j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f i j : R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i : R)

Tactic:
LinearMap.toMatrixAlgEquiv_apply v₁ f i j

Premises used: LinearMap.toMatrixAlgEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
j : n
⊢ Eq (α := n → R) (((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f)ᵀ j)
    (⇑((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R)

Tactic:
LinearMap.toMatrixAlgEquiv_transpose_apply v₁ f j

Premises used: LinearMap.toMatrixAlgEquiv_transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
rw :
  Eq.{u_5 + 1} (α := M₁)
    ((v₁.equivFun.symm : (a : n → R) → M₁) (M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) : M₁)
    (∑ j : n,
        HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₁ : (a : n) → M₁) j : M₁) :
      M₁)
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := M₁)
    (∑ i : n,
      HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) i)
        ((v₁ : (a : n) → M₁) i : M₁))
    (∑ j : n,
      HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
        ((v₁ : (a : n) → M₁) j : M₁))
⊢ Eq.{u_5 + 1} (α := M₁)
    ((v₁.equivFun.symm : (a : n → R) → M₁)
        ((((toLinAlgEquiv' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R)
            (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R) :
          n → R) :
      M₁)
    (∑ j : n,
        HSMul.hSMul (β := M₁) ((M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) v : n →₀ R) : (a : n) → R)) j)
          ((v₁ : (a : n) → M₁) j : M₁) :
      M₁)

Tactic:
rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, Matrix.toLinAlgEquiv'_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
i : n
⊢ Eq.{u_5 + 1} (α := M₁)
    ((((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M : M₁ →ₗ[R] M₁) : (a : M₁) → M₁)
        ((v₁ : (a : n) → M₁) i : M₁) :
      M₁)
    (∑ j : n, HSMul.hSMul (β := M₁) (M j i) ((v₁ : (a : n) → M₁) j : M₁) : M₁)

Tactic:
Matrix.toLin_self _ _ _ _

Premises used: Matrix.toLin_self
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
simp_rw :
  Eq (α := Matrix n n R)
    ((AlgEquiv.ofLinearEquiv (toMatrix v₁ v₁) ⋯ ⋯ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R)
    (1 : Matrix n n R)
simp_rw₁ :
  Eq (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)
⊢ Eq (α := Matrix n n R) ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)

Tactic:
simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]

Premises used: LinearMap.toMatrix_id, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
rw :
  Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁)
    ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
        ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) LinearMap.id) :
      M₁ →ₗ[R] M₁)
    (LinearMap.id : M₁ →ₗ[R] M₁)
rw₁ rw₂ : Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) LinearMap.id LinearMap.id
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1) LinearMap.id

Tactic:
rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]

Premises used: LinearMap.toMatrixAlgEquiv_id, Matrix.toLinAlgEquiv_toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)

Tactic:
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Premises used: LinearMap.toMatrix_comp, LinearMap.toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
rw :
  (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
rw₁ rw₂ :
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f * g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)

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

Premises used: LinearMap.toMatrixAlgEquiv_comp, Module.End.mul_eq_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
A B : Matrix n n R
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (A * B) : M₁ →ₗ[R] M₁)
    ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A ∘ₗ (toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) B :
      M₁ →ₗ[R] M₁)

Tactic:
Matrix.toLin_mul v₁ v₁ v₁ A B

Premises used: Matrix.toLin_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
A B : Matrix n n R
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) (A * B) : M₁ →ₗ[R] M₁)
    ((toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) A ∘ₗ
        (toLinAlgEquiv v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) B :
      M₁ →ₗ[R] M₁)

Tactic:
convert! Matrix.toLin_mul v₁ v₁ v₁ A B

Premises used: Matrix.toLin_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ IsUnit (M := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R) ↔ IsUnit f

Tactic:
isUnit_map_iff (LinearMap.toMatrixAlgEquiv _) f

Premises used: isUnit_map_iff, LinearMap.toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ IsUnit.{u_5} (M := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) M : M₁ →ₗ[R] M₁) ↔ IsUnit M

Tactic:
isUnit_map_iff (LinearMap.toMatrixAlgEquiv _).symm M

Premises used: AlgEquiv.symm, isUnit_map_iff, LinearMap.toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
a b c d : R
x : R × R
⊢ (((toLin (Basis.finTwoProd R) (Basis.finTwoProd R) : (a : Matrix (Fin 2) (Fin 2) R) → R × R →ₗ[R] R × R)
            !![a, b; c, d] :
          R × R →ₗ[R] R × R) :
        (a : R × R) → R × R)
      x =
    (a * x.1 + b * x.2, c * x.1 + d * x.2)

Tactic:
simp [Matrix.toLin_apply, Matrix.mulVec, dotProduct]

Premises used: dotProduct, Matrix.toLin_apply, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
a b c d : R
⊢ (toLin (Basis.finTwoProd R) (Basis.finTwoProd R) : (a : Matrix (Fin 2) (Fin 2) R) → R × R →ₗ[R] R × R)
      !![a, b; c, d] =
    (HSMul.hSMul (β := R × R →ₗ[R] R) a (LinearMap.fst R R R) +
          HSMul.hSMul (β := R × R →ₗ[R] R) b (LinearMap.snd R R R)).prod
      (HSMul.hSMul (β := R × R →ₗ[R] R) c (LinearMap.fst R R R) +
        HSMul.hSMul (β := R × R →ₗ[R] R) d (LinearMap.snd R R R))

Tactic:
LinearMap.ext <| Matrix.toLin_finTwoProd_apply _ _ _ _

Premises used: LinearMap.ext, Matrix.toLin_finTwoProd_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
a :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
      (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq (α := Matrix n n R)
    ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) : Matrix n n R)
    (Matrix.diagonal fun (x_1 : n) ↦ x : Matrix n n R)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₃ :
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := n →₀ R) x (Finsupp.single j 1) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₄ : Eq.{u_1 + 1} (α := R) ((Finsupp.single j x : (a : n) → R) i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₅ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (j : n) ↦ R) j x i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₆ : Pi.single (M := fun (j : n) ↦ R) j x i = if i = j then x else 0
a₇ a₈ : (if i = j then x else 0) = if i = j then x else 0
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)

Tactic:
rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]

Premises used: Pi.single_apply, Matrix.diagonal_apply, DistribSMul.toLinearMap_apply, Finsupp.single_eq_pi_single, Finsupp.smul_single_one, Module.Basis.repr_self, LinearMap.toMatrix_apply, map_smul
-- 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
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
a :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inl j) :
        R)
      (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (m := m) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0
          0 ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inl j) :
        R)
a₁ :
  ∀ (i : n) (j : m),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inr j) :
        R)
      (fromBlocks (l := n) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
          ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inr j) :
        R)
a₂ :
  ∀ (i : m) (j : n),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inr i) (Sum.inl j) :
        R)
      (fromBlocks (m := m) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
          ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inl j) :
        R)
a₃ :
  ∀ (i j : m),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inr i) (Sum.inr j) :
        R)
      (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (l := n) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0
          0 ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inr j) :
        R)
⊢ Eq (α := Matrix (n ⊕ m) (n ⊕ m) R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
    (fromBlocks ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)

Tactic:
ext (i | i) (j | 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 : Fintype m
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : n
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inl i) (Sum.inl j) :
      R)
    (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (m := m) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inl j) :
      R)

Tactic:
simp [toMatrix]

Premises used: 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 : 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
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : n
j : m
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inl i) (Sum.inr j) :
      R)
    (fromBlocks (l := n) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inr j) :
      R)

Tactic:
simp [toMatrix]

Premises used: 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 : 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
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i : m
j : n
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inr i) (Sum.inl j) :
      R)
    (fromBlocks (m := m) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inl j) :
      R)

Tactic:
simp [toMatrix]

Premises used: 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 : 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
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
i j : m
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inr i) (Sum.inr j) :
      R)
    (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (l := n) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inr j) :
      R)

Tactic:
simp [toMatrix]

Premises used: LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)

Tactic:
simp only [LinearMap.toMatrix_apply', coe_lmul_eq_mul, LinearMap.mul_apply']

Premises used: LinearMap.toMatrix_apply', LinearMap.mul_apply', Algebra.coe_lmul_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x : R
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) x) : Matrix m m R)
    (Matrix.diagonal fun (x_1 : m) ↦ x : Matrix m m R)

Tactic:
toMatrix_distrib_mul_action_toLinearMap b x

Premises used: toMatrix_distrib_mul_action_toLinearMap