awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) 1) 1
rw₁ rw₂ : Eq (α := Matrix m m R) 1 1
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) 1) : Matrix m m R)
    (1 : Matrix m m R)

Tactic:
rw [map_one, LinearMap.toMatrix_one]

Premises used: LinearMap.toMatrix_one, map_one
-- 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 y : S
rw :
  (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
      (HMul.hMul (α := End R S) (β := End R S) ((lmul R S : (a : S) → End R S) x : End R S)
        ((lmul R S : (a : S) → End R S) y : End R S)) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
rw₁ rw₂ :
  HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
⊢ (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) (x * y)) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)

Tactic:
rw [map_mul, LinearMap.toMatrix_mul]

Premises used: LinearMap.toMatrix_mul, map_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
rw : Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) 0) 0
rw₁ rw₂ : Eq (α := Matrix m m R) 0 0
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) 0) : Matrix m m R)
    (0 : Matrix m m R)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- 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 y : S
rw :
  (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
      (HAdd.hAdd (α := End R S) (β := End R S) ((lmul R S : (a : S) → End R S) x : End R S)
        ((lmul R S : (a : S) → End R S) y : End R S)) =
    HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
rw₁ rw₂ :
  HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R) =
    HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
⊢ (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) (x + y)) =
    HAdd.hAdd (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)

Tactic:
rw [map_add, map_add]

Premises used: map_add
-- 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
r : R
a :
  ∀ (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) ((algebraMap R S : (a : R) → S) r : S)) i j :
        R)
      ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) :
      Matrix m m R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r : Matrix m m R)

Tactic:
ext
-- 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
r : R
i j : m
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lsmul R R S : (a : R) → End R S) r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j : R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
    (Matrix.diagonal ((algebraMap R (m → R) : (a : R) → m → R) r) i j)
a₃ :
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j)
    (Matrix.diagonal (fun (i : m) ↦ (algebraMap R R : (a : R) → R) r) i j)
a₄ a₅ : Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : m) ↦ r) i j) (Matrix.diagonal (fun (i : m) ↦ r) i j)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) r : S)) i j :
      R)
    ((algebraMap R (Matrix m m R) : (a : R) → Matrix m m R) r i j : R)

Tactic:
rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]

Premises used: Algebra.algebraMap_self_apply, Algebra.lmul_algebraMap, Matrix.algebraMap_eq_diagonal, Algebra.toMatrix_lsmul, Pi.algebraMap_def
-- 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
⊢ Eq (α := Matrix m m R) ((leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)

Tactic:
rfl

Premises used: rfl
-- 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
rw :
  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)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
    ((((b.repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((b : (a : m) → S) j : S)) : m →₀ R) : (a : m) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix b : (a : S) → Matrix m m R) 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:
rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]

Premises used: Algebra.toMatrix_lmul', Algebra.leftMulMatrix_apply
-- 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 y : S
⊢ Eq (α := m → R)
    (mulVec (n := m) ((leftMulMatrix b : (a : S) → Matrix m m R) x)
      (⇑((b.repr : (a : S) → m →₀ R) y : m →₀ R) : (a : m) → R))
    (⇑((b.repr : (a : S) → m →₀ R) (x * y) : m →₀ R) : (a : m) → R)

Tactic:
(LinearMap.mulLeft R x).toMatrix_mulVec_repr b b y

Premises used: LinearMap.toMatrix_mulVec_repr, LinearMap.mulLeft
-- 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
⊢ Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) (mulLeft R x) : Matrix m m R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix m m R)

Tactic:
rfl

Premises used: rfl
-- 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 x' : S
h :
  Eq (α := Matrix m m R) ((leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix m m R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x' : Matrix m m R)
rw rw₁ :
  Eq (α := S) ((((lmul R S : (a : S) → End R S) x' : End R S) : (a : S) → S) 1 : S)
    ((((lmul R S : (a : S) → End R S) x' : End R S) : (a : S) → S) 1 : S)
⊢ Eq (α := S) ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) 1 : S)
    ((((lmul R S : (a : S) → End R S) x' : End R S) : (a : S) → S) 1 : S)

Tactic:
rw [(LinearMap.toMatrix b b).injective h]

Premises used: LinearEquiv.injective, 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
G : Type u_4
inst_5 : Group G
inst_6 : DistribMulAction G S
inst_7 : SMulCommClass G R S
inst_8 : SMulCommClass G S S
g : G
x : S
a :
  ∀ (i j : m),
    Eq.{u_1 + 1} (α := R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x i j : R)
      ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
⊢ Eq (α := Matrix m m R) ((leftMulMatrix (g • b) : (a : S) → Matrix m m R) x : Matrix m m R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix m m R)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
inst_1 : Fintype m
inst_2 : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : CommSemiring A
inst_6 : AddCommMonoid M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : Algebra R A
inst_10 : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
a :
  ∀ (i j : n × m),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (bA.smulTower' bM) (bA.smulTower' bM) : (a : M →ₗ[R] M) → Matrix (n × m) (n × m) R)
          ((↑R :
              {S : Type u_4} →
                {M M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f)
          i j :
        R)
      ((Matrix.comp n n m m R : (a : Matrix n n (Matrix m m R)) → Matrix (n × m) (n × m) R)
          (Matrix.map (α := A) ((toMatrix bM bM : (a : M →ₗ[A] M) → Matrix n n A) f)
            (⇑(leftMulMatrix bA) : (a : A) → Matrix m m R))
          i j :
        R)
⊢ Eq (α := Matrix (n × m) (n × m) R)
    ((toMatrix (bA.smulTower' bM) (bA.smulTower' bM) : (a : M →ₗ[R] M) → Matrix (n × m) (n × m) R)
        ((↑R :
            {S : Type u_4} →
              {M M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      Matrix (n × m) (n × m) R)
    ((Matrix.comp n n m m R : (a : Matrix n n (Matrix m m R)) → Matrix (n × m) (n × m) R)
        (Matrix.map (α := A) ((toMatrix bM bM : (a : M →ₗ[A] M) → Matrix n n A) f)
          (⇑(leftMulMatrix bA) : (a : A) → Matrix m m R)) :
      Matrix (n × m) (n × m) R)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
inst_1 : Fintype m
inst_2 : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : CommSemiring A
inst_6 : AddCommMonoid M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : Algebra R A
inst_10 : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
i j : n × m
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix (bA.smulTower' bM) (bA.smulTower' bM) : (a : M →ₗ[R] M) → Matrix (n × m) (n × m) R)
        ((↑R :
            {S : Type u_4} →
              {M M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f)
        i j :
      R)
    ((Matrix.comp n n m m R : (a : Matrix n n (Matrix m m R)) → Matrix (n × m) (n × m) R)
        (Matrix.map (α := A) ((toMatrix bM bM : (a : M →ₗ[A] M) → Matrix n n A) f)
          (⇑(leftMulMatrix bA) : (a : A) → Matrix m m R))
        i j :
      R)

Tactic:
simp [toMatrix, Algebra.leftMulMatrix_apply,
    Basis.smulTower'_repr, Basis.smulTower'_apply, mul_comm]

Premises used: Module.Basis.smulTower'_apply, Module.Basis.smulTower'_repr, mul_comm, Algebra.leftMulMatrix_apply, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : T
ik jk : m × n
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (m × n) (m × n) R) x ik jk : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) ((leftMulMatrix c : (a : T) → Matrix n n S) x ik.2 jk.2) ik.1 jk.1 : R)

Tactic:
simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smulTower_apply,
    Basis.smulTower_repr, Finsupp.smul_apply, smul_eq_mul, map_smul, mul_smul_comm,
    coe_lmul_eq_mul, LinearMap.mul_apply']

Premises used: LinearMap.mul_apply', Finsupp.smul_apply, Module.Basis.smulTower_apply, mul_comm, mul_smul_comm, smul_eq_mul, Algebra.coe_lmul_eq_mul, Module.Basis.smulTower_repr, Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply, map_smul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
a :
  ∀ (i : m) (k : n) (j : m) (k' : n),
    Eq.{u_1 + 1} (α := R)
      ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (m × n) (m × n) R) ((algebraMap S T : (a : S) → T) x) (i, k)
          (j, k') :
        R)
      (blockDiagonal (fun (x_1 : n) ↦ (leftMulMatrix b : (a : S) → Matrix m m R) x) (i, k) (j, k') : R)
⊢ Eq (α := Matrix (m × n) (m × n) R)
    ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (m × n) (m × n) R) ((algebraMap S T : (a : S) → T) x) :
      Matrix (m × n) (m × n) R)
    (blockDiagonal fun (x_1 : n) ↦ (leftMulMatrix b : (a : S) → Matrix m m R) x : Matrix (m × n) (m × n) R)

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
a :
  Eq.{u_1 + 1} (α := R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) (if (i, k).2 = (j, k').2 then (algebraMap S S : (a : S) → S) x else 0)
        (i, k).1 (j, k').1 :
      R)
    (if (i, k).2 = (j, k').2 then (leftMulMatrix b : (a : S) → Matrix m m R) x (i, k).1 (j, k').1 else 0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (m × n) (m × n) R) ((algebraMap S T : (a : S) → T) x) (i, k)
        (j, k') :
      R)
    (blockDiagonal (fun (x_1 : n) ↦ (leftMulMatrix b : (a : S) → Matrix m m R) x) (i, k) (j, k') : R)

Tactic:
rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]

Premises used: Algebra.smulTower_leftMulMatrix, AlgHom.commutes, Matrix.blockDiagonal_apply, Matrix.algebraMap_matrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
pos :
  ∀ (h : (i, k).2 = (j, k').2),
    Eq.{u_1 + 1} (α := R)
      ((leftMulMatrix b : (a : S) → Matrix m m R) ((algebraMap S S : (a : S) → S) x) (i, k).1 (j, k').1 : R)
      ((leftMulMatrix b : (a : S) → Matrix m m R) x (i, k).1 (j, k').1 : R)
neg :
  ∀ (h : ¬(i, k).2 = (j, k').2),
    Eq.{u_1 + 1} (α := R) ((leftMulMatrix b : (a : S) → Matrix m m R) 0 (i, k).1 (j, k').1 : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) (if (i, k).2 = (j, k').2 then (algebraMap S S : (a : S) → S) x else 0)
        (i, k).1 (j, k').1 :
      R)
    (if (i, k).2 = (j, k').2 then (leftMulMatrix b : (a : S) → Matrix m m R) x (i, k).1 (j, k').1 else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
h : k = k'
⊢ Eq.{u_1 + 1} (α := R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) ((algebraMap S S : (a : S) → S) x) (i, k).1 (j, k').1 : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x (i, k).1 (j, k').1 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
h : ¬k = k'
⊢ Eq.{u_1 + 1} (α := R) ((leftMulMatrix b : (a : S) → Matrix m m R) 0 (i, k).1 (j, k').1 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k : n
rw :
  Eq.{u_1 + 1} (α := R) (blockDiagonal (fun (x_1 : n) ↦ (leftMulMatrix b : (a : S) → Matrix m m R) x) (i, k) (j, k) : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (m × n) (m × n) R) ((algebraMap S T : (a : S) → T) x) (i, k)
        (j, k) :
      R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)

Tactic:
rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]

Premises used: Matrix.blockDiagonal_apply_eq, Algebra.smulTower_leftMulMatrix_algebraMap
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k k' : n
h : k ≠ k'
rw :
  Eq.{u_1 + 1} (α := R) (blockDiagonal (fun (x_1 : n) ↦ (leftMulMatrix b : (a : S) → Matrix m m R) x) (i, k) (j, k')) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R)
    ((leftMulMatrix (b.smulTower c) : (a : T) → Matrix (m × n) (m × n) R) ((algebraMap S T : (a : S) → T) x) (i, k)
        (j, k') :
      R)
    (0 : R)

Tactic:
rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]

Premises used: Matrix.blockDiagonal_apply_ne, Algebra.smulTower_leftMulMatrix_algebraMap
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
⊢ Eq (α := M₁ →ₗ[R] M₂) ((b₁.linearMap b₂ : (a : ι₂ × ι₁) → M₁ →ₗ[R] M₂) ij : M₁ →ₗ[R] M₂)
    ((toLin b₁ b₂ : (a : Matrix ι₂ ι₁ R) → M₁ →ₗ[R] M₂) ((stdBasis R ι₂ ι₁ : (a : ι₂ × ι₁) → Matrix ι₂ ι₁ R) ij) :
      M₁ →ₗ[R] M₂)

Tactic:
simp [linearMap]

Premises used: Module.Basis.linearMap
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
have :
  ∀ (this : DecidableEq ι₂),
    Eq.{u_4 + 1} (α := M₂)
      ((((b₁.linearMap b₂ : (a : ι₂ × ι₁) → M₁ →ₗ[R] M₂) ij : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
          ((b₁ : (a : ι₁) → M₁) k : M₁) :
        M₂)
      (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
⊢ Eq.{u_4 + 1} (α := M₂)
    ((((b₁.linearMap b₂ : (a : ι₂ × ι₁) → M₁ →ₗ[R] M₂) ij : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
        ((b₁ : (a : ι₁) → M₁) k : M₁) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)

Tactic:
have := Classical.decEq ι₂