awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
i j : m
a :
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (g • b) (g • b) : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((lmul R S : (a : S) → End R S) x : End R S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R)
              ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S)
                ((g • b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((b.repr : (a : S) → m →₀ R)
              ((((LinearMap.mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) : (a : S) → S) ((b : (a : m) → S) j : S)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
a₃ :
  Eq.{u_1 + 1} (α := R)
    (((((g • b).repr : (a : S) → m →₀ R) (HMul.hMul (β := S) x ((g • 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)
a₄ :
  Eq.{u_1 + 1} (α := R)
    ((((LinearEquiv.symm (DistribMulAction.toLinearEquiv R S g) ≪≫ₗ b.repr : (a : S) → m →₀ R)
              (HMul.hMul (β := S) x ((g • 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 (g • b) : (a : S) → Matrix m m R) x i j : R)
    ((leftMulMatrix b : (a : S) → Matrix m m R) x i j : R)
have a₅ : Eq.{u_1 + 1} (α := R)
  ((((LinearEquiv.symm (DistribMulAction.toLinearEquiv R S g) ≪≫ₗ b.repr : (a : S) → m →₀ R)
            (x * HSMul.hSMul (β := S) g ((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)
Tactic: simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
⊢ 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)
have 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)
Tactic: ext ⟨i, k⟩ ⟨j, k'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
⊢ 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)
have 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)
Tactic: rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
⊢ 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)
have 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)
Tactic: rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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)
⊢ 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)
have 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)
Tactic: rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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'
⊢ 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)
have 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
Tactic: rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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
⊢ 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)
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
⊢ 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₂)
have 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₂)
Tactic: have := Classical.decEq ι₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
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₂)
have rw : Eq.{u_4 + 1} (α := M₂)
  (∑ j : ι₂,
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (Matrix.single ij.1 ij.2 1 j k) ((b₂ : (a : ι₂) → M₂) j : M₂) :
    M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: rw [linearMap_apply, Matrix.stdBasis_eq_single, Matrix.toLin_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
this : DecidableEq ι₂
⊢ Eq.{u_4 + 1} (α := M₂)
    (∑ j : ι₂,
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (Matrix.single ij.1 ij.2 1 j k) ((b₂ : (a : ι₂) → M₂) j : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
have dsimp : Eq.{u_4 + 1} (α := M₂)
  (∑ j : ι₂,
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (if ij.1 = j ∧ ij.2 = k then 1 else 0)
        ((b₂ : (a : ι₂) → M₂) j : M₂) :
    M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: dsimp only [Matrix.single, of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
this : DecidableEq ι₂
⊢ Eq.{u_4 + 1} (α := M₂)
    (∑ j : ι₂,
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (if ij.1 = j ∧ ij.2 = k then 1 else 0)
          ((b₂ : (a : ι₂) → M₂) j : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
have simp_rw : Eq.{u_4 + 1} (α := M₂)
  (∑ x : ι₂,
      if ij.1 = x ∧ ij.2 = k then HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 1 ((b₂ : (a : ι₂) → M₂) x : M₂)
      else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
    M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
this : DecidableEq ι₂
simp_rw :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 1 ((b₂ : (a : ι₂) → M₂) x : M₂)
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
⊢ Eq.{u_4 + 1} (α := M₂)
    (∑ j : ι₂,
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (if ij.1 = j ∧ ij.2 = k then 1 else 0)
          ((b₂ : (a : ι₂) → M₂) j : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
have simp_rw₁ : Eq.{u_4 + 1} (α := M₂)
  (∑ x : ι₂,
      if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x
      else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
    M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
this : DecidableEq ι₂
simp_rw :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 1 ((b₂ : (a : ι₂) → M₂) x : M₂)
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
⊢ Eq.{u_4 + 1} (α := M₂)
    (∑ j : ι₂,
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (if ij.1 = j ∧ ij.2 = k then 1 else 0)
          ((b₂ : (a : ι₂) → M₂) j : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
have simp_rw₂ : Eq.{u_4 + 1} (α := M₂) (∑ x : ι₂, if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x else 0 : M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
this : DecidableEq ι₂
simp_rw :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 1 ((b₂ : (a : ι₂) → M₂) x : M₂)
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M₂) (∑ x : ι₂, if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x else 0 : M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
⊢ Eq.{u_4 + 1} (α := M₂)
    (∑ j : ι₂,
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (if ij.1 = j ∧ ij.2 = k then 1 else 0)
          ((b₂ : (a : ι₂) → M₂) j : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
have simp_rw₃ : Eq.{u_4 + 1} (α := M₂) (∑ x : ι₂, if ij.1 = x then if ij.2 = k then (b₂ : (a : ι₂) → M₂) x else 0 else 0 : M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
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 : ι₁
this : DecidableEq ι₂
simp_rw :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 1 ((b₂ : (a : ι₂) → M₂) x : M₂)
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M₂)
    (∑ x : ι₂,
        if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x
        else HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) 0 ((b₂ : (a : ι₂) → M₂) x : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M₂) (∑ x : ι₂, if ij.1 = x ∧ ij.2 = k then (b₂ : (a : ι₂) → M₂) x else 0 : M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
simp_rw₃ :
  Eq.{u_4 + 1} (α := M₂) (∑ x : ι₂, if ij.1 = x then if ij.2 = k then (b₂ : (a : ι₂) → M₂) x else 0 else 0 : M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
⊢ Eq.{u_4 + 1} (α := M₂)
    (∑ j : ι₂,
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := M₂) (if ij.1 = j ∧ ij.2 = k then 1 else 0)
          ((b₂ : (a : ι₂) → M₂) j : M₂) :
      M₂)
    (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
have simp_rw₄ : Eq.{u_4 + 1} (α := M₂)
  (if Membership.mem (γ := Finset ι₂) Finset.univ ij.1 then if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 else 0 :
    M₂)
  (if ij.2 = k then (b₂ : (a : ι₂) → M₂) ij.1 else 0 : M₂)
Tactic: simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]