awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι₁
this : DecidableEq ι₂
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₂)
⊢ 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:
rw [linearMap_apply, Matrix.stdBasis_eq_single, Matrix.toLin_self]

Premises used: Module.Basis.linearMap_apply, Matrix.toLin_self, Matrix.stdBasis_eq_single
-- 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 : ι₁
this : DecidableEq ι₂
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₂)
⊢ 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:
dsimp only [Matrix.single, of_apply]

Premises used: Matrix.of_apply, Matrix.single
-- 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 : ι₁
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₂)
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₂)
⊢ 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:
simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]

Premises used: Finset.mem_univ, if_true, one_smul, zero_smul, ite_smul, ite_and, Finset.sum_ite_eq
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
M : Type u_2
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R M
ij : ι × ι
⊢ Eq.{u_2 + 1} (α := End R M) ((b.end : (a : ι × ι) → End R M) ij : End R M)
    ((toLin b b : (a : Matrix ι ι R) → M →ₗ[R] M) ((stdBasis R ι ι : (a : ι × ι) → Matrix ι ι R) ij) : M →ₗ[R] M)

Tactic:
linearMap_apply b b ij

Premises used: Module.Basis.linearMap_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
M : Type u_2
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R M
ij : ι × ι
k : ι
⊢ Eq.{u_2 + 1} (α := M) ((((b.end : (a : ι × ι) → End R M) ij : End 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:
linearMap_apply_apply b b ij k

Premises used: Module.Basis.linearMap_apply_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)

Tactic:
b.ext fun k ↦ ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : ι
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)
⊢ ⁅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)

Tactic:
refine b.ext fun k ↦ ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : ι
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
⊢ 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:
simp only [Ring.lie_def, LinearMap.sub_apply, End.mul_apply, LinearMap.smul_apply,
    Basis.end_apply_apply, smul_ite, smul_zero, sub_smul]

Premises used: LinearMap.smul_apply, sub_smul, Module.Basis.end_apply_apply, smul_zero, smul_ite, Ring.lie_def, LinearMap.sub_apply, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : ι
⊢ 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:
simp [hs, Basis.end_apply_apply]

Premises used: Module.Basis.end_apply_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : ι
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:
simp [hs, Basis.end_apply_apply, hjk]

Premises used: Module.Basis.end_apply_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 j : ι
x y : M
⊢ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j (x + y)) i =
    HAdd.hAdd (α := M) (β := M) ((f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i : M)
      ((f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j y) i : M)

Tactic:
simp [Pi.single_add]

Premises used: Pi.single_add
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 j : ι
x : A
y : M
⊢ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j (x • y)) i =
    HSMul.hSMul (α := A) (β := M) ((RingHom.id A : (a : A) → A) x : A)
      ((f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j y) i : M)

Tactic:
simp [Pi.single_smul]

Premises used: Pi.single_smul
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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
⊢ (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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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
⊢ (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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
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:
simp [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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' := ⋯,
                        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)
⊢ (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

Tactic:
ext i x j
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : ι
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)
⊢ 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)

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, coe_comp, coe_single, Function.comp_apply]

Premises used: LinearMap.coe_mk, LinearMap.coe_comp, LinearMap.coe_single, Function.comp_apply, AddHom.coe_mk
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 : ι
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)
⊢ 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:
rw [← Fintype.sum_apply, ← map_sum]

Premises used: map_sum, Fintype.sum_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 (α := ι → M) (∑ x_1 : ι, Pi.single (M := fun (a : ι) ↦ M) x_1 (Pi.single (M := fun (i : ι) ↦ M) i x x_1))
    (Pi.single (M := fun (i : ι) ↦ M) i x)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
    ((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:
exact congr_arg₂ _ (by aesop) rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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' := ⋯, 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)
              i j :
            (a : M) → M)
          x :
        M)
      ((m i j : (a : M) → M) x : 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

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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' := ⋯, 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)
            i j :
          (a : M) → M)
        x :
      M)
    ((m i j : (a : M) → M) x : M)

Tactic:
simp [Pi.single_apply, apply_ite]

Premises used: Pi.single_apply, apply_ite