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 : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
dsimp :
  (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) (β := (↑M : Type u_1)) (single j i 1)
          (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
        ⋯) =
    v
⊢ (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)))
      ((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)))
        v) =
    v

Tactic:
dsimp
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
h :
  ∀ (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) (β := (↑M : Type u_1)) (single j i 1)
              (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
            ⋯) :
        (↑M : Type u_1)) =
      (↑(v i) : (↑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) (β := (↑M : Type u_1)) (single j i 1)
          (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
        ⋯) =
    v

Tactic:
ext i
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
h :
  ∑ x : ι,
      HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
        (HSMul.hSMul (α := Matrix ι ι R) (single x j 1) (↑(v x) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))
⊢ (↑(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) (β := (↑M : Type u_1)) (single j i 1)
            (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
          ⋯) :
      (↑M : Type u_1)) =
    (↑(v i) : (↑M : Type u_1))

Tactic:
simp only [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 : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i b : ι
h : Membership.mem (γ := Finset ι) Finset.univ b
hb : b ≠ i
⊢ HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single b j 1) (↑(v b) : (↑M : Type u_1))) =
    0

Tactic:
simp [← mul_smul, single_mul_single_of_ne _ _ _ _ hb.symm]

Premises used: Ne.symm, Matrix.single_mul_single_of_ne, 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
⊢ i ∉ Finset.univ →
    HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
        (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
      0

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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
h :
  HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))
⊢ ∑ x : ι,
      HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
        (HSMul.hSMul (α := Matrix ι ι R) (single x j 1) (↑(v x) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))

Tactic:
rw [Finset.sum_eq_single i (fun b _ hb ↦ by
      simp [← mul_smul, single_mul_single_of_ne _ _ _ _ hb.symm]) (by simp)]

Premises used: Finset.sum_eq_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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
⊢ ∃ (y : (↑M : Type u_1)), HSMul.hSMul (α := Matrix ι ι R) (single j j 1) y = (↑(v i) : (↑M : Type u_1))

Tactic:
simpa [-SetLike.coe_mem] using (v i).2

Premises used: SetLike.coe_mem, Subtype.property
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
h :
  ∀ (y : (↑M : Type u_1)) (hy : HSMul.hSMul (α := Matrix ι ι R) (single j j 1) y = (↑(v i) : (↑M : Type u_1))),
    HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
        (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
      (↑(v i) : (↑M : Type u_1))
⊢ HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))

Tactic:
obtain ⟨y, hy⟩ := by simpa [-SetLike.coe_mem] using (v i).2
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
y : (↑M : Type u_1)
hy : HSMul.hSMul (α := Matrix ι ι R) (single j j 1) y = (↑(v i) : (↑M : Type u_1))
⊢ HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))

Tactic:
simp [← mul_smul, ← hy]

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 ι
i : ι
X Y : ModuleCat (Matrix ι ι R)
f : X ⟶ Y
hf :
  ∀ (x : (↑(Functor.obj (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) X) : Type (max v u_1))),
    Eq (α := (↑(Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y) : Type (max v u_1)))
      ((ModuleCat.Hom.hom
              (CategoryTheory.Functor.map (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) f ≫
                Iso.hom
                  ((fun (X : ModuleCat (Matrix ι ι R)) ↦
                      ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
                        Iso (C := ModuleCat (Matrix ι ι R))
                          (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                          (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
                    Y)) :
            (a : (↑((toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).obj X) : Type (max v u_1))) →
              (↑((𝟭 (ModuleCat (Matrix ι ι R))).obj Y) : Type (max v u_1)))
          x :
        (↑(Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y) : Type (max v u_1)))
      ((ModuleCat.Hom.hom
              (Iso.hom
                  ((fun (X : ModuleCat (Matrix ι ι R)) ↦
                      ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
                        Iso (C := ModuleCat (Matrix ι ι R))
                          (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                          (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
                    X) ≫
                CategoryTheory.Functor.map (𝟭 (ModuleCat (Matrix ι ι R))) f) :
            (a : (↑((toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).obj X) : Type (max v u_1))) →
              (↑((𝟭 (ModuleCat (Matrix ι ι R))).obj Y) : Type (max v u_1)))
          x :
        (↑(Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y) : Type (max v u_1)))
⊢ Eq (α :=
    Functor.obj (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) X ⟶ Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y)
    (CategoryTheory.Functor.map (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) f ≫
      Iso.hom
        ((fun (X : ModuleCat (Matrix ι ι R)) ↦
            ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
              Iso (C := ModuleCat (Matrix ι ι R))
                (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
          Y))
    (Iso.hom
        ((fun (X : ModuleCat (Matrix ι ι R)) ↦
            ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
              Iso (C := ModuleCat (Matrix ι ι R))
                (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
          X) ≫
      CategoryTheory.Functor.map (𝟭 (ModuleCat (Matrix ι ι R))) f)

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

Tactic:
simp [toModuleCatFromModuleCatLinearEquiv]

Premises used: toModuleCatFromModuleCatLinearEquiv
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X : ModuleCat R
hf :
  Eq (α :=
    LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1))
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    (Hom.hom
      (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
        NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X)))
    (Hom.hom (𝟙 (Functor.obj (toMatrixModCat R ι) X)))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat (Matrix ι ι R)) (Functor.obj (toMatrixModCat R ι) X)
      (Functor.obj (toMatrixModCat R ι) X))
    (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
      NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X))
    (𝟙 (Functor.obj (toMatrixModCat R ι) X))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X : ModuleCat R
this :
  (↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
        (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
          (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
      LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) =
    LinearMap.id
⊢ Eq (α :=
    LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1))
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    (Hom.hom
      (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
        NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X)))
    (Hom.hom (𝟙 (Functor.obj (toMatrixModCat R ι) X)))

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X : ModuleCat R
hf :
  (↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
        (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
          (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
      LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) =
    LinearMap.id
⊢ Eq (α :=
    LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1))
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    (Hom.hom
      (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
        NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X)))
    (Hom.hom (𝟙 (Functor.obj (toMatrixModCat R ι) X)))

Tactic:
suffices (toModuleCatFromModuleCatLinearEquiv R ((ModuleCat.toMatrixModCat R ι).obj X)
      i).symm.toLinearMap ∘ₗ LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom
      ((unitIso R i).inv.app X)) = LinearMap.id by simpa using this
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X : ModuleCat R
hf :
  ∀ (x : ι → (↑(Functor.obj (𝟭 (ModuleCat R)) X) : Type (max v u_1))),
    Eq (α := (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
      (((↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
                (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
                  (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
              LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) :
            (a : ι → (↑((𝟭 (ModuleCat R)).obj X) : Type (max v u_1))) →
              (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)))
          x :
        (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
      ((LinearMap.id :
            (a : ι → (↑((𝟭 (ModuleCat R)).obj X) : Type (max v u_1))) →
              (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)))
          x :
        (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
⊢ (↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
        (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
          (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
      LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) =
    LinearMap.id

Tactic:
ext x
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X : ModuleCat R
x : ι → (↑(Functor.obj (𝟭 (ModuleCat R)) X) : Type (max v u_1))
⊢ Eq (α := (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    (((↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
              (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
                (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
            LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) :
          (a : ι → (↑((𝟭 (ModuleCat R)).obj X) : Type (max v u_1))) →
            (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)))
        x :
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    ((LinearMap.id :
          (a : ι → (↑((𝟭 (ModuleCat R)).obj X) : Type (max v u_1))) →
            (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)))
        x :
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))

Tactic:
simp [unitIso, toModuleCatFromModuleCatLinearEquiv, fromModuleCatToModuleCatLinearEquiv,
      fromModuleCatToModuleCatLinearEquivtoModuleCatObj, Finset.univ_sum_single]

Premises used: Finset.univ_sum_single, toModuleCatFromModuleCatLinearEquiv, MatrixModCat.unitIso, fromModuleCatToModuleCatLinearEquivtoModuleCatObj, fromModuleCatToModuleCatLinearEquiv
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
hf :
  ∀ (v : ι → (↑X : Type (max u v))),
    Eq (α := (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
      ((ModuleCat.Hom.hom (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) (r • f)) :
            (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
              (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
          v :
        (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
      ((ModuleCat.Hom.hom
              (HSMul.hSMul (β :=
                Quiver.Hom (V := ModuleCat (Matrix ι ι R))
                  (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) X)
                  (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y))
                r (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) f)) :
            (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
              (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
          v :
        (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
⊢ CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) (r • f) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := ModuleCat (Matrix ι ι R)) (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) X)
        (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y))
      r (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) f)

Tactic:
ext (v : ι → X)
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
hf :
  (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
      v =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
⊢ Eq (α := (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
    ((ModuleCat.Hom.hom (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) (r • f)) :
          (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
            (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
        v :
      (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
    ((ModuleCat.Hom.hom
            (HSMul.hSMul (β :=
              Quiver.Hom (V := ModuleCat (Matrix ι ι R))
                (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) X)
                (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y))
              r (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) f)) :
          (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
            (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
        v :
      (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))

Tactic:
simp only [ModuleCat.matrixEquivalence_functor, ModuleCat.toMatrixModCat_obj_carrier,
      ModuleCat.toMatrixModCat_map, ModuleCat.hom_smul, ModuleCat.hom_ofHom, LinearMap.smul_apply]

Premises used: ModuleCat.toMatrixModCat_map, ModuleCat.toMatrixModCat_obj_carrier, LinearMap.smul_apply, ModuleCat.hom_smul, ModuleCat.matrixEquivalence_functor, ModuleCat.hom_ofHom
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
hf :
  ∀ (i_1 : ι),
    (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) :
          (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
        v i_1 =
      HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
        ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) :
              (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
            v :
          ι → (↑Y : Type (max u v)))
        i_1
⊢ (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
      v =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))

Tactic:
ext i
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i_1 : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
i : ι
hf :
  HSMul.hSMul (β := (↑Y : Type (max u v))) r
      ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i
⊢ (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
      v i =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i

Tactic:
simp only [LinearMap.mapMatrixModule_apply, LinearMap.compLeft_apply, Function.comp_apply,
      LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.mapMatrixModule_apply, LinearMap.compLeft_apply, Function.comp_apply