awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
⊢ (a₁ * a₂) •
      HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) =
    HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
      HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A))
have a : ∀ (i j : n),
  ((a₁ * a₂) •
        HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
          (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j =
    (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
i j : n
⊢ ((a₁ * a₂) •
        HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
          (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j =
    (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a : a₁ * a₂ *
    HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
      (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
  (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
      HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
    i j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
i j : n
⊢ a₁ * a₂ *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a : a₁ * a₂ *
    ∑ j_1 : n,
      HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
        (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
  ∑ j_1 : n,
    HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
      HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
Tactic: simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁ * a₂ *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ j_1 : n,
      HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
⊢ a₁ * a₂ *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a₁ : a₁ * a₂ *
    ∑ j_1 : n,
      HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
        (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
  ∑ x : n,
    HSMul.hSMul (β := A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A) i x) *
      HSMul.hSMul (β := A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A) x j)
Tactic: simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁_1 a₂ : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁_1 * a₂ *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ j_1 : n,
      HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
a₁ :
  a₁_1 * a₂ *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A) i x) *
        HSMul.hSMul (β := A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A) x j)
⊢ a₁_1 * a₂ *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a₂ : a₁_1 * a₂ *
    ∑ x : n,
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
        ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
  ∑ x : n,
    HSMul.hSMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
      HSMul.hSMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
Tactic: simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁_1 a₂_1 : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ j_1 : n,
      HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
a₁ :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A) i x) *
        HSMul.hSMul (β := A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A) x j)
a₂ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HSMul.hSMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
⊢ a₁_1 * a₂_1 *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a₃ : a₁_1 * a₂_1 *
    ∑ x : n,
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
        ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
  ∑ x : n,
    HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
      HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
Tactic: simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁_1 a₂_1 : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ j_1 : n,
      HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
a₁ :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A) i x) *
        HSMul.hSMul (β := A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A) x j)
a₂ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HSMul.hSMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
a₃ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
⊢ a₁_1 * a₂_1 *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a₄ : Eq.{u_7 + 1} (α := A)
  (∑ i_1 : n,
    a₁_1 * a₂_1 *
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i i_1) : A)
        ((algebraMap R A : (a : R) → A) (b₂ i_1 j) : A))
  (∑ x : n,
    HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
      HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A))
Tactic: simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁_1 a₂_1 : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ j_1 : n,
      HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) i j_1 *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)) j_1 j
a₁ :
  a₁_1 * a₂_1 *
      ∑ j_1 : n,
        HMul.hMul (α := A) (b₁.map (⇑(algebraMap R A) : (a : R) → A) i j_1)
          (b₂.map (⇑(algebraMap R A) : (a : R) → A) j_1 j) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A) i x) *
        HSMul.hSMul (β := A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A) x j)
a₂ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HSMul.hSMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HSMul.hSMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
a₃ :
  a₁_1 * a₂_1 *
      ∑ x : n,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A) =
    ∑ x : n,
      HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)
a₄ :
  Eq.{u_7 + 1} (α := A)
    (∑ i_1 : n,
      a₁_1 * a₂_1 *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i i_1) : A)
          ((algebraMap R A : (a : R) → A) (b₂ i_1 j) : A))
    (∑ x : n,
      HMul.hMul (β := A) a₁_1 ((algebraMap R A : (a : R) → A) (b₁ i x) : A) *
        HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A))
⊢ a₁_1 * a₂_1 *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁_1 (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂_1 (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
have a₅ : Eq.{u_7 + 1} (α := A)
  (∑ x : n,
    a₁_1 *
      (a₂_1 *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
          ((algebraMap R A : (a : R) → A) (b₂ x j) : A)))
  (∑ x : n,
    a₁_1 *
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (b₁ i x) : A)
        (HMul.hMul (β := A) a₂_1 ((algebraMap R A : (a : R) → A) (b₂ x j) : A)))
Tactic: simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
⊢ Eq (α := Matrix n n A) ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
have simp_rw : Eq (α := Matrix n n A)
  ((TensorProduct.lift (toFunBilinear n R A) : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
  (1 : Matrix n n A)
Tactic: simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply,
        Matrix.map_one (algebraMap R A) (map_zero _) (map_one _), one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
simp_rw :
  Eq (α := Matrix n n A)
    ((TensorProduct.lift (toFunBilinear n R A) : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
⊢ Eq (α := Matrix n n A) ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
have simp_rw₁ : Eq (α := Matrix n n A)
  (((toFunBilinear n R A : (a : A) → Matrix n n R →ₗ[R] Matrix n n A) 1 : (a : Matrix n n R) → Matrix n n A) 1) 1
Tactic: simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply,
        Matrix.map_one (algebraMap R A) (map_zero _) (map_one _), one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
simp_rw :
  Eq (α := Matrix n n A)
    ((TensorProduct.lift (toFunBilinear n R A) : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
simp_rw₁ :
  Eq (α := Matrix n n A)
    (((toFunBilinear n R A : (a : A) → Matrix n n R →ₗ[R] Matrix n n A) 1 : (a : Matrix n n R) → Matrix n n A) 1) 1
⊢ Eq (α := Matrix n n A) ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
have simp_rw₂ : HSMul.hSMul (α := A) (β := Matrix n n A) 1
    (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) 1 (⇑(algebraMap R A) : (a : R) → A)) =
  1
Tactic: simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply,
        Matrix.map_one (algebraMap R A) (map_zero _) (map_one _), one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
simp_rw :
  Eq (α := Matrix n n A)
    ((TensorProduct.lift (toFunBilinear n R A) : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
simp_rw₁ :
  Eq (α := Matrix n n A)
    (((toFunBilinear n R A : (a : A) → Matrix n n R →ₗ[R] Matrix n n A) 1 : (a : Matrix n n R) → Matrix n n A) 1) 1
simp_rw₂ :
  HSMul.hSMul (α := A) (β := Matrix n n A) 1
      (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) 1 (⇑(algebraMap R A) : (a : R) → A)) =
    1
⊢ Eq (α := Matrix n n A) ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
have simp_rw₃ : HSMul.hSMul (α := A) (β := Matrix n n A) 1 1 = 1
Tactic: simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply,
        Matrix.map_one (algebraMap R A) (map_zero _) (map_one _), one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
⊢ Eq (α := A ⊗[R] Matrix n n R) (invFun n R A (M.map (⇑(algebraMap R A) : (a : R) → A))) (1 ⊗ₜ[R] M)
have dsimp : Eq (α := A ⊗[R] Matrix n n R) (∑ p : n × n, (algebraMap R A : (a : R) → A) (M p.1 p.2) ⊗ₜ[R] single p.1 p.2 1)
  (1 ⊗ₜ[R] M)
Tactic: dsimp [invFun]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
⊢ Eq (α := A ⊗[R] Matrix n n R) (∑ p : n × n, (algebraMap R A : (a : R) → A) (M p.1 p.2) ⊗ₜ[R] single p.1 p.2 1)
    (1 ⊗ₜ[R] M)
have simp : Eq (α := A ⊗[R] Matrix n n R) (1 ⊗ₜ[R] ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
  (1 ⊗ₜ[R] M)
Tactic: simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
⊢ Eq (α := A ⊗[R] Matrix n n R) (1 ⊗ₜ[R] ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
    (1 ⊗ₜ[R] M)
have e_n : ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1) = M
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
| M
have rw : ∑ i : n, ∑ j : n, single i j (M i j)
Tactic: rw [matrix_eq_sum_single M]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1) = M
have e_n : Eq (α := Matrix n n R) (∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
  (∑ i : n, ∑ j : n, single i j (M i j))
Tactic: conv_rhs => rw [matrix_eq_sum_single M]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
⊢ Eq (α := Matrix n n R) (∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
    (∑ i : n, ∑ j : n, single i j (M i j))
have h : ∀ (x : n),
  Membership.mem (γ := Finset n) Finset.univ x →
    ∀ (x_1 : n),
      Membership.mem (γ := Finset n) Finset.univ x_1 →
        single x x_1 (M x x_1) =
          HSMul.hSMul (β := Matrix n n R) (M (x, x_1).1 (x, x_1).2) (single (x, x_1).1 (x, x_1).2 1)
Tactic: convert! Finset.sum_product (β := Matrix n n R) ..
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
⊢ (toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (invFun n R A M) = M
have simp : ∑ x : n × n,
    HSMul.hSMul (β := Matrix n n A) (M x.1 x.2)
      (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single x.1 x.2 1) (⇑(algebraMap R A) : (a : R) → A)) =
  M
Tactic: simp only [invFun, map_sum, toFunAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
⊢ ∑ x : n × n,
      HSMul.hSMul (β := Matrix n n A) (M x.1 x.2)
        (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single x.1 x.2 1) (⇑(algebraMap R A) : (a : R) → A)) =
    M
have h : M =
  ∑ x : n,
    ∑ y : n,
      HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
        (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A))
Tactic: convert! Finset.sum_product (β := Matrix n n A) ..
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
| M
have rw : ∑ i : n, ∑ j : n, single i j (M i j)
Tactic: rw [matrix_eq_sum_single M]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
⊢ M =
    ∑ x : n,
      ∑ y : n,
        HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
          (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A))
have h : Eq (α := Matrix n n A) (∑ i : n, ∑ j : n, single i j (M i j))
  (∑ x : n,
    ∑ y : n,
      HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
        (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A)))
Tactic: conv_lhs => rw [matrix_eq_sum_single M]