awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
N : Type u_2
inst_7 : AddCommGroup N
inst_8 : Module (Matrix ι ι R) N
i : ι
inst_9 : Module R N
inst_10 : IsScalarTower R (Matrix ι ι R) N
f : LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) M N
y : M
hx : Membership.mem (γ := Submodule R M) (toModuleCatObj R M i) (HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y)
⊢ Membership.mem (α := N) (γ := Submodule R N) (toModuleCatObj R N i)
    (((↑R :
              {S : Type (max u v)} →
                {M : Type u_1} →
                  {M₂ : Type u_2} →
                    [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₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → N)
        (HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y) :
      N)

Tactic:
exact ⟨f y, map_smul _ _ _ |>.symm⟩
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : (↑M : Type u_1)
rw : (r • m) • x = HMul.hMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) m • x
rw₁ : (r • m) • x = ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x
rw₂ rw₃ : ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x = ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x
⊢ (r • m) • x = HSMul.hSMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) (m • x)

Tactic:
rw [← mul_smul, Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul]

Premises used: Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
⊢ ∀ (x y : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))),
    ∑ i_1 : ι, (↑(x + y) : ι → M) i_1 = HAdd.hAdd (α := M) (∑ i_1 : ι, (↑x : ι → M) i_1) (∑ i_1 : ι, (↑y : ι → M) i_1)

Tactic:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
r : R
x_1 : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))
x : ι → M
hx : Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x
⊢ ∑ i_1 : ι,
      (↑(r •
              Subtype.mk (p := fun (x : ι → M) ↦
                Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx) :
          ι → M)
        i_1 =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      (∑ i_1 : ι,
        (↑(Subtype.mk (p := fun (x : ι → M) ↦
                Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx) :
            ι → M)
          i_1)

Tactic:
simp [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
x : M
⊢ Eq (α := ι → M)
    ((let __spread.0 : (ι → M) →+ ι → M := DistribSMul.toAddMonoidHom (M := Matrix ι ι R) (ι → M) (single i i 1);
          { toFun := (↑__spread.0 : ZeroHom (ι → M) (ι → M)).toFun, map_add' := ⋯, map_smul' := ⋯ } :
          (a : ι → M) → ι → M)
        (Function.const ι x) :
      ι → M)
    (Pi.single (M := fun (a : ι) ↦ M) i x : (j : ι) → M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
x_1 : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))
x : ι → M
hx : Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x
obtain :
  ∀ (y : ι → M) (hy : HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y = x),
    (fun (x : M) ↦
          (Subtype.mk (p := fun (x : ι → M) ↦
              Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
              (Pi.single (M := fun (a : ι) ↦ M) i x) ⋯ :
            ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
        ((fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
          (Subtype.mk (p := fun (x : ι → M) ↦
            Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx)) =
      Subtype.mk (p := fun (x : ι → M) ↦
        Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx
⊢ (fun (x : M) ↦
        (Subtype.mk (p := fun (x : ι → M) ↦
            Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
            (Pi.single (M := fun (a : ι) ↦ M) i x) ⋯ :
          ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
      ((fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
        (Subtype.mk (p := fun (x : ι → M) ↦
          Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx)) =
    Subtype.mk (p := fun (x : ι → M) ↦
      Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx

Tactic:
obtain ⟨y, hy⟩ := mem_toModuleCatObj i |>.1 hx

Premises used: MatrixModCat.mem_toModuleCatObj, Iff.mp
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
x_1 : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))
x : ι → M
hx : Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x
y : ι → M
hy : HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y = x
⊢ Pi.single (M := fun (j : ι) ↦ M) i (HSMul.hSMul.{u, u_1, u_1} (α := R) 1 (y i)) = x

Tactic:
rw [single_smul] at hy

Premises used: Matrix.Module.single_smul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
x_1 : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))
x : ι → M
hx : Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x
y : ι → M
hy : Pi.single (M := fun (j : ι) ↦ M) i (HSMul.hSMul.{u, u_1, u_1} (α := R) 1 (y i)) = x
⊢ (fun (x : M) ↦
        (Subtype.mk (p := fun (x : ι → M) ↦
            Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
            (Pi.single (M := fun (a : ι) ↦ M) i x) ⋯ :
          ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
      ((fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
        (Subtype.mk (p := fun (x : ι → M) ↦
          Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx)) =
    Subtype.mk (p := fun (x : ι → M) ↦
      Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx

Tactic:
simp [← hy]
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
i : ι
x : M
⊢ (fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
      ((fun (x : M) ↦
          (Subtype.mk (p := fun (x : ι → M) ↦
              Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
              (Pi.single (M := fun (a : ι) ↦ M) i x) ⋯ :
            ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X Y : ModuleCat R
f : X ⟶ Y
x :
  (↑(Functor.obj (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i)) X) :
    Type (max v u_1))
⊢ Eq (α := (↑(Functor.obj (𝟭 (ModuleCat R)) Y) : Type (max v u_1)))
    ((ModuleCat.Hom.hom
            (CategoryTheory.Functor.map
                (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i)) f ≫
              Iso.hom
                ((fun (X : ModuleCat R) ↦
                    (LinearEquiv.toModuleIso
                        (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X : Type (max v u_1)) i ≪≫ₗ
                          fromModuleCatToModuleCatLinearEquiv R (↑X : Type (max v u_1)) i) :
                      Iso (C := ModuleCat R)
                        (ModuleCat.of R
                          (↑(Functor.obj
                                (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι)
                                  (toModuleCat R i))
                                (ModuleCat.of R (↑X : Type (max v u_1)))) :
                            Type (max v u_1)))
                        (ModuleCat.of R (↑X : Type (max v u_1)))))
                  Y)) :
          (a : (↑((ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).obj X) : Type (max v u_1))) →
            (↑((𝟭 (ModuleCat R)).obj Y) : Type (max v u_1)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat R)) Y) : Type (max v u_1)))
    ((ModuleCat.Hom.hom
            (Iso.hom
                ((fun (X : ModuleCat R) ↦
                    (LinearEquiv.toModuleIso
                        (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X : Type (max v u_1)) i ≪≫ₗ
                          fromModuleCatToModuleCatLinearEquiv R (↑X : Type (max v u_1)) i) :
                      Iso (C := ModuleCat R)
                        (ModuleCat.of R
                          (↑(Functor.obj
                                (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι)
                                  (toModuleCat R i))
                                (ModuleCat.of R (↑X : Type (max v u_1)))) :
                            Type (max v u_1)))
                        (ModuleCat.of R (↑X : Type (max v u_1)))))
                  X) ≫
              CategoryTheory.Functor.map (𝟭 (ModuleCat R)) f) :
          (a : (↑((ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).obj X) : Type (max v u_1))) →
            (↑((𝟭 (ModuleCat R)).obj Y) : Type (max v u_1)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat R)) Y) : Type (max v u_1)))

Tactic:
simp [fromModuleCatToModuleCatLinearEquivtoModuleCatObj]

Premises used: fromModuleCatToModuleCatLinearEquivtoModuleCatObj
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
m : (↑M : Type u_1)
i : ι
⊢ (let __spread.0 : (↑M : Type u_1) →+ (↑M : Type u_1) :=
          DistribSMul.toAddMonoidHom (M := Matrix ι ι R) (↑M : Type u_1) (single j j 1);
        { toFun := (↑__spread.0 : ZeroHom (↑M : Type u_1) (↑M : Type u_1)).toFun, map_add' := ⋯, map_smul' := ⋯ } :
        (a : (↑M : Type u_1)) → (↑M : Type u_1))
      (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) m) =
    HSMul.hSMul (α := Matrix ι ι R) (single j i 1) m

Tactic:
simp [← mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x x_1 : (↑M : Type u_1)
h :
  ∀ (x_2 : ι),
    (↑(Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
            Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
            (HSMul.hSMul (α := Matrix ι ι R) (single j x_2 1) (x + x_1)) ⋯) :
        (↑M : Type u_1)) =
      (↑(HAdd.hAdd (α := ι → ↥(toModuleCatObj R (↑M : Type u_1) j)) (β := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
            (fun (i : ι) ↦
              Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
                Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
                (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x) ⋯)
            (fun (i : ι) ↦
              Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
                Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
                (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x_1) ⋯)
            x_2) :
        (↑M : Type u_1))
⊢ (fun (i : ι) ↦
      Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
        Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
        (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) (x + x_1)) ⋯) =
    HAdd.hAdd (α := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
      (fun (i : ι) ↦
        Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x) ⋯)
      fun (i : ι) ↦
      Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
        Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
        (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x_1) ⋯

Tactic:
ext
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x x_1 : (↑M : Type u_1)
x_2 : ι
⊢ (↑(Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j x_2 1) (x + x_1)) ⋯) :
      (↑M : Type u_1)) =
    (↑(HAdd.hAdd (α := ι → ↥(toModuleCatObj R (↑M : Type u_1) j)) (β := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x) ⋯)
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x_1) ⋯)
          x_2) :
      (↑M : Type u_1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
⊢ IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)

Tactic:
haveI := MatrixModCat.isScalarTower_toModuleCat R M
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
simp :
  (single j i 1 * x) • m =
    HSMul.hSMul (α := Matrix ι ι R) (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) m
⊢ (↑(Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) (x • m)) ⋯) :
      (↑M : Type u_1)) =
    (↑(HSMul.hSMul (α := Matrix ι ι R) (β := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
          ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) m) ⋯)
          i) :
      (↑M : Type u_1))

Tactic:
simp only [← mul_smul, RingHom.id_apply, Module.smul_apply,
      AddSubmonoidClass.coe_finsetSum, SetLike.val_smul, ← smul_assoc, ← Finset.sum_smul]

Premises used: Finset.sum_smul, RingHom.id_apply, smul_assoc, AddSubmonoidClass.coe_finsetSum, Matrix.Module.smul_apply, SetLike.val_smul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
e_a : single j i 1 * x = ∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)
⊢ (single j i 1 * x) • m =
    HSMul.hSMul (α := Matrix ι ι R) (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) m

Tactic:
congr
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
e_a :
  ∀ (i1 j1 : ι),
    HMul.hMul (α := Matrix ι ι R) (single j i 1) x i1 j1 =
      (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) i1 j1
⊢ single j i 1 * x = ∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)

Tactic:
ext i1 j1
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
e_a : Eq.{u + 1} (α := R) (∑ j_1 : ι, single j i 1 i1 j_1 * x j_1 j1) (∑ c : ι, single j c (x i c) i1 j1)
⊢ HMul.hMul (α := Matrix ι ι R) (single j i 1) x i1 j1 =
    (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) i1 j1

Tactic:
simp only [mul_apply, smul_single, smul_eq_mul, mul_one, sum_apply]

Premises used: Matrix.sum_apply, Matrix.mul_apply, smul_eq_mul, Matrix.smul_single, mul_one
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
⊢ Membership.mem (γ := Finset ι) Finset.univ i

Tactic:
simp
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 b : ι
h : Membership.mem (γ := Finset ι) Finset.univ b
hb : b ≠ i
⊢ single j i 1 i1 b * x b j1 = 0

Tactic:
simp [single, Ne.symm hb]

Premises used: Ne.symm, Matrix.single
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
e_a : single j i 1 i1 i * x i j1 = ∑ c : ι, single j c (x i c) i1 j1
⊢ Eq.{u + 1} (α := R) (∑ j_1 : ι, single j i 1 i1 j_1 * x j_1 j1) (∑ c : ι, single j c (x i c) i1 j1)

Tactic:
rw [Finset.sum_eq_single_of_mem (a := i) (by simp) (fun b _ hb ↦ by simp [single, Ne.symm hb])]

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
e_a : (if j = i1 then x i j1 else 0) = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0
⊢ single j i 1 i1 i * x i j1 = ∑ c : ι, single j c (x i c) i1 j1

Tactic:
simp only [single_apply, and_true, ite_mul, one_mul, zero_mul]

Premises used: and_true, MulZeroClass.zero_mul, ite_mul, Matrix.single_apply, one_mul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
pos : ∀ (h : j = i1), x i j1 = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0
neg : ∀ (h : ¬j = i1), Eq.{u + 1} (α := R) 0 (∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0)
⊢ (if j = i1 then x i j1 else 0) = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
h : j = i1
⊢ x i j1 = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
h : ¬j = i1
⊢ Eq.{u + 1} (α := R) 0 (∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
m : (↑M : Type u_1)
⊢ (fun (m : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)) ↦
        (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(m i) : (↑M : Type u_1)) : (↑M : Type u_1)))
      ((fun (m : (↑M : Type u_1)) (i : ι) ↦
          (Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) m) ⋯ :
            ↥(toModuleCatObj R (↑M : Type u_1) j)))
        m) =
    m

Tactic:
simp [← mul_smul, ← Finset.sum_smul, sum_single_one]

Premises used: Finset.sum_smul, Matrix.sum_single_one, SemigroupAction.mul_smul