awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
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₂)
⊢ 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 True 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_5
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
M : Type u_9
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), (s : (a : M) → M) ((b : (a : ι) → M) k : M) = HSMul.hSMul (β := M) (a k) ((b : (a : ι) → M) k : M)
i j : ι
⊢ ⁅s, (b.end : (a : ι × ι) → End R M) (i, j)⁆ =
    HSMul.hSMul (β := End R M) (a i - a j) ((b.end : (a : ι × ι) → End R M) (i, j) : End R M)
have refine : ∀ (k : ι),
  Eq (α := M) (((⁅s, (b.end : (a : ι × ι) → End R M) (i, j)⁆ : End R M) : (a : M) → M) ((b : (a : ι) → M) k : M) : M)
    ((HSMul.hSMul (β := End R M) (a i - a j) ((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
        ((b : (a : ι) → M) k : M) :
      M)
Tactic: refine b.ext fun k ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_5
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
M : Type u_9
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), (s : (a : M) → M) ((b : (a : ι) → M) k : M) = HSMul.hSMul (β := M) (a k) ((b : (a : ι) → M) k : M)
i j k : ι
⊢ Eq (α := M) (((⁅s, (b.end : (a : ι × ι) → End R M) (i, j)⁆ : End R M) : (a : M) → M) ((b : (a : ι) → M) k : M) : M)
    ((HSMul.hSMul (β := End R M) (a i - a j) ((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
        ((b : (a : ι) → M) k : M) :
      M)
have simp : HSub.hSub (α := M) (β := M) ((s : (a : M) → M) (if j = k then (b : (a : ι) → M) i else 0 : M) : M)
    ((((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
        ((s : (a : M) → M) ((b : (a : ι) → M) k : M) : M) :
      M) =
  (if j = k then HSMul.hSMul (β := M) (a i) ((b : (a : ι) → M) i : M) else 0) -
    if j = k then HSMul.hSMul (β := M) (a j) ((b : (a : ι) → M) i : M) else 0
Tactic: simp only [Ring.lie_def, LinearMap.sub_apply, End.mul_apply, LinearMap.smul_apply,
    Basis.end_apply_apply, smul_ite, smul_zero, sub_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_5
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
M : Type u_9
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), (s : (a : M) → M) ((b : (a : ι) → M) k : M) = HSMul.hSMul (β := M) (a k) ((b : (a : ι) → M) k : M)
i j k : ι
⊢ HSub.hSub (α := M) (β := M) ((s : (a : M) → M) (if j = k then (b : (a : ι) → M) i else 0 : M) : M)
      ((((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
          ((s : (a : M) → M) ((b : (a : ι) → M) k : M) : M) :
        M) =
    (if j = k then HSMul.hSMul (β := M) (a i) ((b : (a : ι) → M) i : M) else 0) -
      if j = k then HSMul.hSMul (β := M) (a j) ((b : (a : ι) → M) i : M) else 0
have inl : HSub.hSub (α := M) (β := M) ((s : (a : M) → M) (if j = j then (b : (a : ι) → M) i else 0 : M) : M)
    ((((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
        ((s : (a : M) → M) ((b : (a : ι) → M) j : M) : M) :
      M) =
  (if j = j then HSMul.hSMul (β := M) (a i) ((b : (a : ι) → M) i : M) else 0) -
    if j = j then HSMul.hSMul (β := M) (a j) ((b : (a : ι) → M) i : M) else 0
Tactic: rcases eq_or_ne j k with rfl | hjk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_5
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_8
M : Type u_9
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), (s : (a : M) → M) ((b : (a : ι) → M) k : M) = HSMul.hSMul (β := M) (a k) ((b : (a : ι) → M) k : M)
i j k : ι
inl :
  HSub.hSub (α := M) (β := M) ((s : (a : M) → M) (if j = j then (b : (a : ι) → M) i else 0 : M) : M)
      ((((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
          ((s : (a : M) → M) ((b : (a : ι) → M) j : M) : M) :
        M) =
    (if j = j then HSMul.hSMul (β := M) (a i) ((b : (a : ι) → M) i : M) else 0) -
      if j = j then HSMul.hSMul (β := M) (a j) ((b : (a : ι) → M) i : M) else 0
⊢ HSub.hSub (α := M) (β := M) ((s : (a : M) → M) (if j = k then (b : (a : ι) → M) i else 0 : M) : M)
      ((((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
          ((s : (a : M) → M) ((b : (a : ι) → M) k : M) : M) :
        M) =
    (if j = k then HSMul.hSMul (β := M) (a i) ((b : (a : ι) → M) i : M) else 0) -
      if j = k then HSMul.hSMul (β := M) (a j) ((b : (a : ι) → M) i : M) else 0
have inr : ∀ (hjk : j ≠ k),
  HSub.hSub (α := M) (β := M) ((s : (a : M) → M) (if j = k then (b : (a : ι) → M) i else 0 : M) : M)
      ((((b.end : (a : ι × ι) → End R M) (i, j) : End R M) : (a : M) → M)
          ((s : (a : M) → M) ((b : (a : ι) → M) k : M) : M) :
        M) =
    (if j = k then HSMul.hSMul (β := M) (a i) ((b : (a : ι) → M) i : M) else 0) -
      if j = k then HSMul.hSMul (β := M) (a j) ((b : (a : ι) → M) i : M) else 0
Tactic: rcases eq_or_ne j k with rfl | hjk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
m : Matrix.{u_1, u_1, u_4} ι ι (End A M)
x y : ι → M
⊢ (fun (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) ((x + y) j)) =
    HAdd.hAdd (α := ι → M) (fun (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j)) fun (i : ι) ↦
      ∑ j : ι, (m i j : (a : M) → M) (y j)
have h : ∀ (x_1 : ι),
  ∑ j : ι, (m x_1 j : (a : M) → M) ((x + y) j) =
    HAdd.hAdd (α := ι → M) (β := ι → M) (fun (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j))
      (fun (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (y j)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
m : Matrix.{u_1, u_1, u_4} ι ι (End A M)
m_1 : A
x : ι → M
⊢ (fun (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) ((m_1 • x) j)) =
    HSMul.hSMul (α := A) (β := ι → M) ((RingHom.id A : (a : A) → A) m_1 : A) fun (i : ι) ↦
      ∑ j : ι, (m i j : (a : M) → M) (x j)
have h : ∀ (x_1 : ι),
  ∑ j : ι, (m x_1 j : (a : M) → M) ((m_1 • x) j) =
    HSMul.hSMul (α := A) (β := ι → M) ((RingHom.id A : (a : A) → A) m_1 : A)
      (fun (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f : End A (ι → M)
⊢ (fun (m : Matrix.{u_1, u_1, u_4} ι ι (End A M)) ↦
        ({ toFun := fun (x : ι → M) (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j), map_add' := ⋯, map_smul' := ⋯ } :
          (ι → M) →ₗ[A] ι → M))
      ((fun (f : End A (ι → M)) (i j : ι) ↦
          ({ toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
              map_smul' := ⋯ } :
            M →ₗ[A] M))
        f) =
    f
have h : ∀ (i : ι) (x : M) (j : ι),
  Eq.{u_4 + 1} (α := M)
    ((((fun (m : Matrix.{u_1, u_1, u_4} ι ι (End A M)) ↦
                  ({ toFun := fun (x : ι → M) (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j), map_add' := sorry,
                      map_smul' := sorry } :
                    (ι → M) →ₗ[A] ι → M))
                ((fun (f : End A (ι → M)) (i j : ι) ↦
                    ({ toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                        map_add' := sorry, map_smul' := sorry } :
                      M →ₗ[A] M))
                  f) ∘ₗ
              LinearMap.single.{u_3, u_1, u_4} A (fun (i : ι) ↦ M) i :
            M →ₗ[A] ι → M) :
          (a : M) → ι → M)
        x j :
      M)
    ((f ∘ₗ LinearMap.single.{u_3, u_1, u_4} A (fun (i : ι) ↦ M) i : (a : M) → ι → M) x j : M)
Tactic: ext i x j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f : End A (ι → M)
i : ι
x : M
j : ι
⊢ Eq.{u_4 + 1} (α := M)
    ((((fun (m : Matrix.{u_1, u_1, u_4} ι ι (End A M)) ↦
                  ({ toFun := fun (x : ι → M) (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j), map_add' := ⋯,
                      map_smul' := ⋯ } :
                    (ι → M) →ₗ[A] ι → M))
                ((fun (f : End A (ι → M)) (i j : ι) ↦
                    ({ toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                        map_add' := ⋯, map_smul' := ⋯ } :
                      M →ₗ[A] M))
                  f) ∘ₗ
              LinearMap.single.{u_3, u_1, u_4} A (fun (i : ι) ↦ M) i :
            M →ₗ[A] ι → M) :
          (a : M) → ι → M)
        x j :
      M)
    ((f ∘ₗ LinearMap.single.{u_3, u_1, u_4} A (fun (i : ι) ↦ M) i : (a : M) → ι → M) x j : M)
have h : Eq.{u_4 + 1} (α := M)
  (∑ x_1 : ι,
      (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) x_1 (Pi.single (M := fun (i : ι) ↦ M) i x x_1)) j :
    M)
  ((f : (a : (i : ι) → M) → ι → M) (Pi.single (M := fun (i : ι) ↦ M) i x) j : M)
Tactic: simp only [LinearMap.coe_mk, AddHom.coe_mk, coe_comp, coe_single, Function.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f : End A (ι → M)
i : ι
x : M
j : ι
⊢ Eq.{u_4 + 1} (α := M)
    (∑ x_1 : ι,
        (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) x_1 (Pi.single (M := fun (i : ι) ↦ M) i x x_1)) j :
      M)
    ((f : (a : (i : ι) → M) → ι → M) (Pi.single (M := fun (i : ι) ↦ M) i x) j : M)
have h : Eq.{u_4 + 1} (α := M)
  ((f : (a : ι → M) → (a : ι) → M)
      (∑ x_1 : ι, Pi.single (M := fun (a : ι) ↦ M) x_1 (Pi.single (M := fun (i : ι) ↦ M) i x x_1)) j :
    M)
  ((f : (a : (i : ι) → M) → ι → M) (Pi.single (M := fun (i : ι) ↦ M) i x) j : M)
Tactic: rw [← Fintype.sum_apply, ← map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
m : Matrix.{u_1, u_1, u_4} ι ι (End A M)
⊢ (fun (f : End A (ι → M)) (i j : ι) ↦
        ({ toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
            map_smul' := ⋯ } :
          M →ₗ[A] M))
      ((fun (m : Matrix.{u_1, u_1, u_4} ι ι (End A M)) ↦
          ({ toFun := fun (x : ι → M) (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j), map_add' := ⋯, map_smul' := ⋯ } :
            (ι → M) →ₗ[A] ι → M))
        m) =
    m
have a : ∀ (i j : ι) (x : M),
  Eq (α := M)
    (((fun (f : End A (ι → M)) (i j : ι) ↦
              ({ toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                  map_add' := sorry, map_smul' := sorry } :
                M →ₗ[A] M))
            ((fun (m : Matrix.{u_1, u_1, u_4} ι ι (End A M)) ↦
                ({ toFun := fun (x : ι → M) (i : ι) ↦ ∑ j : ι, (m i j : (a : M) → M) (x j), map_add' := sorry,
                    map_smul' := sorry } :
                  (ι → M) →ₗ[A] ι → M))
              m)
            i j :
          (a : M) → M)
        x :
      M)
    ((m i j : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f g : End A (ι → M)
⊢ (fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (f * g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ }) =
    HMul.hMul (α := Matrix.{u_1, u_1, u_4} ι ι (End A M))
      (fun (i j : ι) ↦
        { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
          map_smul' := ⋯ : M →ₗ[A] M })
      fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ : M →ₗ[A] M }
have a : ∀ (i j : ι) (x : M),
  Eq (α := M)
    (({ toFun := fun (x : M) ↦ (f * g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := sorry,
            map_smul' := sorry } :
          (a : M) → M)
        x :
      M)
    ((HMul.hMul (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := sorry, map_smul' := sorry : M →ₗ[A] M })
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := sorry, map_smul' := sorry : M →ₗ[A] M })
            i j :
          (a : M) → M)
        x :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f g : End A (ι → M)
i j : ι
x : M
⊢ Eq (α := M)
    (({ toFun := fun (x : M) ↦ (f * g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
            map_smul' := ⋯ } :
          (a : M) → M)
        x :
      M)
    ((HMul.hMul (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
            i j :
          (a : M) → M)
        x :
      M)
have a : Eq.{u_4 + 1} (α := M)
  ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
  (∑ x_1 : ι,
      (f : (a : ι → M) → ι → M)
        (Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
        i :
    M)
Tactic: simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply,
      LinearMap.coe_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f g : End A (ι → M)
i j : ι
x : M
⊢ Eq.{u_4 + 1} (α := M)
    ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
    (∑ x_1 : ι,
        (f : (a : ι → M) → ι → M)
          (Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
          i :
      M)
have a : Eq.{u_4 + 1} (α := M)
  ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
  ((f : (a : ι → M) → (a : ι) → M)
      (∑ x_1 : ι,
        Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
      i :
    M)
Tactic: rw [← Fintype.sum_apply, ← map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
f g : End A (ι → M)
⊢ (fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (f + g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ }) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_4} ι ι (End A M))
      (fun (i j : ι) ↦
        { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
          map_smul' := ⋯ : M →ₗ[A] M })
      fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ : M →ₗ[A] M }
have a : ∀ (i j : ι) (x : M),
  Eq (α := M)
    (({ toFun := fun (x : M) ↦ (f + g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := sorry,
            map_smul' := sorry } :
          (a : M) → M)
        x :
      M)
    ((HAdd.hAdd (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := sorry, map_smul' := sorry : M →ₗ[A] M })
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := sorry, map_smul' := sorry : M →ₗ[A] M })
            i j :
          (a : M) → M)
        x :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
r : R
⊢ Eq (α := Matrix.{u_1, u_1, u_4} ι ι (End A M))
    (Equiv.toFun (RingEquiv.toEquiv (endVecRingEquivMatrixEnd ι A M))
      ((algebraMap R (End A (ι → M)) : (a : R) → End A (ι → M)) r))
    ((algebraMap R (Matrix.{u_1, u_1, u_4} ι ι (End A M)) : (a : R) → Matrix ι ι (End A M)) r)
have a : ∀ (i j : ι) (x : M),
  Eq (α := M)
    ((Equiv.toFun (RingEquiv.toEquiv (endVecRingEquivMatrixEnd ι A M))
            ((algebraMap R (End A (ι → M)) : (a : R) → End A (ι → M)) r) i j :
          (a : M) → M)
        x :
      M)
    ((((algebraMap R (Matrix.{u_1, u_1, u_4} ι ι (End A M)) : (a : R) → Matrix ι ι (End A M)) r i j : End A M) :
          (a : M) → M)
        x :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
r : R
i j : ι
x : M
⊢ Eq (α := M)
    ((Equiv.toFun (RingEquiv.toEquiv (endVecRingEquivMatrixEnd ι A M))
            ((algebraMap R (End A (ι → M)) : (a : R) → End A (ι → M)) r) i j :
          (a : M) → M)
        x :
      M)
    ((((algebraMap R (Matrix.{u_1, u_1, u_4} ι ι (End A M)) : (a : R) → Matrix ι ι (End A M)) r i j : End A M) :
          (a : M) → M)
        x :
      M)
have a : (if i = j then r • x else 0) = (if i = j then HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id else 0 : (a : M) → M) x
Tactic: simp only [endVecRingEquivMatrixEnd, RingEquiv.toEquiv_eq_coe, Module.algebraMap_end_eq_smul_id,
      Equiv.toFun_as_coe, EquivLike.coe_coe, RingEquiv.coe_mk, Equiv.coe_fn_mk,
      LinearMap.smul_apply, id_coe, id_eq, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero,
      LinearMap.coe_mk, AddHom.coe_mk, algebraMap_matrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
r : R
i j : ι
x : M
⊢ (if i = j then r • x else 0) = (if i = j then HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id else 0 : (a : M) → M) x
have pos : i = j → r • x = (HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id : (a : M) → M) x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
r : R
i j : ι
x : M
pos : i = j → r • x = (HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id : (a : M) → M) x
⊢ (if i = j then r • x else 0) = (if i = j then HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id else 0 : (a : M) → M) x
have neg : ¬i = j → Eq (α := M) (0 : M) ((0 : (a : M) → M) x : M)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
⊢ IsStablyFiniteRing A ↔ ∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))
have simp_rw : (∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (Matrix (Fin n) (Fin n) A)) ↔
  ∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))
Tactic: simp_rw [isStablyFiniteRing_iff, MulEquivClass.isDedekindFiniteMonoid_iff
    (matrixRingEquivEndVecMulOpposite (ι := Fin _) (A := A)),
    MulOpposite.isDedekindFiniteMonoid_iff]