awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑(M₂.obj X) : Type v))
    ((ModuleCat.Hom.hom ((n • f).app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
have hf : Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) ((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map (n • f)) :
        (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
          (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
      x :
    (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
  ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x : (↑(M₂.obj X) : Type v))
Tactic: change (toPresheaf R ⋙ (evaluation _ _).obj X).map (n • f) x = _
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : (↑(M₁.obj X) : Type v)
⊢ Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) ((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map (n • f)) :
          (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
            (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
        x :
      (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
    ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x :
      (↑(M₂.obj X) : Type v))
have hf : Eq (α := (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (n • (toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).map f) :
        (a : (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₁) : Type v)) →
          (↑((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).obj M₂) : Type v))
      x :
    (↑((toPresheaf R ⋙ Functor.obj (evaluation Cᵒᵖ Ab) X).obj M₂) : Type v))
  ((ModuleCat.Hom.hom (n • f.app X) : (a : (↑(M₁.obj X) : Type v)) → (↑(M₂.obj X) : Type v)) x : (↑(M₂.obj X) : Type v))
Tactic: rw [Functor.map_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (unit R).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom
          ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj Y) : Type u) ℤ (↑(M.obj Y) : Type u)) :
              (a : (↑(M.obj Y) : Type u)) → (↑(R.obj Y) : Type u) →ₗ[(↑(R.obj Y) : Type u)] (↑(M.obj Y) : Type u))
            ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y))) =
    ModuleCat.ofHom
        ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
            (a : (↑(M.obj X) : Type u)) → (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
          ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)) ≫
      M.map f
have hf : Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
  ((ModuleCat.Hom.hom
          ((unit R).map f ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              (ModuleCat.ofHom
                ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj Y) : Type u) ℤ (↑(M.obj Y) : Type u)) :
                    (a : (↑(M.obj Y) : Type u)) → (↑(R.obj Y) : Type u) →ₗ[(↑(R.obj Y) : Type u)] (↑(M.obj Y) : Type u))
                  ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y)))) :
        (a : (↑(R.obj X) : Type u)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
      1 :
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
  ((ModuleCat.Hom.hom
          (ModuleCat.ofHom
              ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                  (a : (↑(M.obj X) : Type u)) → (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)) ≫
            M.map f) :
        (a : (↑(R.obj X) : Type u)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
      1 :
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    ((ModuleCat.Hom.hom
            ((unit R).map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                (ModuleCat.ofHom
                  ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj Y) : Type u) ℤ (↑(M.obj Y) : Type u)) :
                      (a : (↑(M.obj Y) : Type u)) →
                        (↑(R.obj Y) : Type u) →ₗ[(↑(R.obj Y) : Type u)] (↑(M.obj Y) : Type u))
                    ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) Y)))) :
          (a : (↑(R.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                    (a : (↑(M.obj X) : Type u)) → (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                  ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)) ≫
              M.map f) :
          (a : (↑(R.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
        1 :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
have hf : HSMul.hSMul (α := (↑(R.obj Y) : Type u))
    ((1 : (a : (↑((unit R).obj Y) : Type u)) → (↑(R.obj Y) : Type u))
        ((ModuleCat.Hom.hom ((unit R).map f) :
              (a : (↑(R.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u))
            1 :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u)) :
      (↑(R.obj Y) : Type u))
    ((↑s : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) Y) =
  (ModuleCat.Hom.hom (M.map f) :
      (a : (↑(M.obj X) : Type u)) → (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    (HSMul.hSMul (α := (↑(R.obj X) : Type u)) 1 ((↑s : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HSMul.hSMul (α := (↑(R.obj Y) : Type u))
      ((1 : (a : (↑((unit R).obj Y) : Type u)) → (↑(R.obj Y) : Type u))
          ((ModuleCat.Hom.hom ((unit R).map f) :
                (a : (↑(R.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u))
              1 :
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((unit R).obj Y)) : Type u)) :
        (↑(R.obj Y) : Type u))
      ((↑s : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) Y) =
    (ModuleCat.Hom.hom (M.map f) :
        (a : (↑(M.obj X) : Type u)) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
      (HSMul.hSMul (α := (↑(R.obj X) : Type u)) 1 ((↑s : (j : Cᵒᵖ) → (↑(M.obj j) : Type u)) X))
have hf : HSMul.hSMul (α := (↑(R.obj Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.map f) :
          (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u))
        1 :
      (↑(R.obj Y) : Type u))
    (s.eval Y) =
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
        LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) (M.map f) :
      (a : (↑(M.obj X) : Type u)) → (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Y)) : Type u))
    (HSMul.hSMul (α := (↑(R.obj X) : Type u)) 1 (s.eval X))
Tactic: change R.map f 1 • s.eval Y = M.map f (1 • s.eval X)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
f : unit R ⟶ M
⊢ (fun (s : M.sections) ↦
        ({
            app := fun (X : Cᵒᵖ) ↦
              ModuleCat.ofHom
                ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                    (a : (↑(M.obj X) : Type u)) → (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                  ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
            naturality := ⋯ } :
          (unit R).Hom M))
      ((fun (f : unit R ⟶ M) ↦
          sectionsMk
            (fun (X : Cᵒᵖ) ↦
              (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                    LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u)
                      (↑x2 : Type u))
                    (CC := ModuleCat.carrier) (f.app X) :
                  (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                1)
            ⋯)
        f) =
    f
have h : ∀ (X : Cᵒᵖ),
  ModuleCat.Hom.hom
      (Hom.app
        ((fun (s : M.sections) ↦
            ({
                app := fun (X : Cᵒᵖ) ↦
                  ModuleCat.ofHom
                    ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                        (a : (↑(M.obj X) : Type u)) →
                          (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                      ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                naturality := sorry } :
              (unit R).Hom M))
          ((fun (f : unit R ⟶ M) ↦
              sectionsMk
                (fun (X : Cᵒᵖ) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                        LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u)
                          (↑x2 : Type u))
                        (CC := ModuleCat.carrier) (f.app X) :
                      (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                    1)
                sorry)
            f))
        X) =
    ModuleCat.Hom.hom (f.app X)
Tactic: ext X : 2
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
M : PresheafOfModules R
s : M.sections
⊢ (fun (f : unit R ⟶ M) ↦
        sectionsMk
          (fun (X : Cᵒᵖ) ↦
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                  LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u)
                    (↑x2 : Type u))
                  (CC := ModuleCat.carrier) (f.app X) :
                (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
              1)
          ⋯)
      ((fun (s : M.sections) ↦
          ({
              app := fun (X : Cᵒᵖ) ↦
                ModuleCat.ofHom
                  ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                      (a : (↑(M.obj X) : Type u)) →
                        (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                    ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
              naturality := ⋯ } :
            (unit R).Hom M))
        s) =
    s
have h : ∀ (X : Cᵒᵖ),
  (↑((fun (f : unit R ⟶ M) ↦
              sectionsMk
                (fun (X : Cᵒᵖ) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                        LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u)
                          (↑x2 : Type u))
                        (CC := ModuleCat.carrier) (f.app X) :
                      (a : (↑((unit R).obj X) : Type u)) → (↑(M.obj X) : Type u))
                    1)
                sorry)
            ((fun (s : M.sections) ↦
                ({
                    app := fun (X : Cᵒᵖ) ↦
                      ModuleCat.ofHom
                        ((LinearEquiv.symm (ringLmapEquivSelf (↑(R.obj X) : Type u) ℤ (↑(M.obj X) : Type u)) :
                            (a : (↑(M.obj X) : Type u)) →
                              (↑(R.obj X) : Type u) →ₗ[(↑(R.obj X) : Type u)] (↑(M.obj X) : Type u))
                          ((↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X)),
                    naturality := sorry } :
                  (unit R).Hom M))
              s)) :
        (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j)
      X =
    (↑s : (j : Cᵒᵖ) → (M.presheaf ⋙ forget Ab).obj j) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : (↑(R.obj X) : Type u)
x : (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v)
⊢ HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (R.map (hX.to Y ≫ f)) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u))
          r :
        (↑(R.obj Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map f) :
            (a : (↑(M.obj Y) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v)) =
    HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β := (↑(M.obj Z) : Type v))
      ((RingCat.Hom.hom (R.map (hX.to Z)) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u)) r :
        (↑(R.obj Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map f) :
            (a : (↑(M.obj Y) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
have e_a : hX.to Y ≫ f = hX.to Z
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Products (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone.{u, v, w} Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone.{u, v, w} Z).π.app j = s.π.app j
⊢ m = ↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦ Hom.hom (s.π.app { as := j }))
have hf : ∀ (x : (↑s.pt : Type (max v w))),
  Eq (α := (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
    ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x :
      (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
    ((Hom.hom
            (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                Hom.hom (s.π.app { as := j }))) :
          (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
        x :
      (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Products (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone.{u, v, w} Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone.{u, v, w} Z).π.app j = s.π.app j
x : (↑s.pt : Type (max v w))
⊢ Eq (α := (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
    ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x :
      (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
    ((Hom.hom
            (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                Hom.hom (s.π.app { as := j }))) :
          (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
        x :
      (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
have hf : ∀ (i : ι),
  Eq (α := (↑(Z i) : Type (max v w)))
    ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x i :
      (↑(Z i) : Type (max v w)))
    ((Hom.hom
            (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                Hom.hom (s.π.app { as := j }))) :
          (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
        x i :
      (↑(Z i) : Type (max v w)))
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Products (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
i : ι
⊢ Eq (α := Functor.obj (Discrete.functor Z) { as := i : Discrete ι } ⟶ s.pt)
    ((coproductCocone.{u, v, w} Z).ι.app { as := i : Discrete ι } ≫
      ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))
    (s.ι.app { as := i })
have hf : ∀ (x : (↑(Z i) : Type (max v w))),
  Eq (α := (↑s.pt : Type (max v w)))
    ((Hom.hom
            ((coproductCocone.{u, v, w} Z).ι.app { as := i : Discrete ι } ≫
              ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
                  Hom.hom (s.ι.app { as := i }))) :
          (a : (↑((Discrete.functor Z).obj { as := i }) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))
    ((Hom.hom (s.ι.app { as := i }) :
          (a : (↑((Discrete.functor Z).obj { as := i }) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))
Tactic: ext (x : Z i)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Products (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
⊢ f =
    ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
        Hom.hom (s.ι.app { as := i }))
have hf : Hom.hom f =
  Hom.hom
    (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
        Hom.hom (s.ι.app { as := i })))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Products (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
⊢ Hom.hom f =
    Hom.hom
      (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))
have hf : ∀ (i : ι),
  Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i =
    Hom.hom
        (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
            Hom.hom (s.ι.app { as := i }))) ∘ₗ
      lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i
Tactic: refine DirectSum.linearMap_ext _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Products (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
i : ι
⊢ Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i =
    Hom.hom
        (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
            Hom.hom (s.ι.app { as := i }))) ∘ₗ
      lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i
have hf : ∀ (x : (↑(Z i) : Type (max v w))),
  Eq (α := (↑s.pt : Type (max v w)))
    ((Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i :
          (a : (↑(Z i) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))
    ((Hom.hom
              (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
                  Hom.hom (s.ι.app { as := i }))) ∘ₗ
            lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i :
          (a : (↑(Z i) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Projective (goal)
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
⊢ CategoryTheory.Projective P
have refine : ∀ {E X : ModuleCat.{v, u} R} (E_1 : P ⟶ X) (X_1 : E ⟶ X) (epi : Epi X_1), ∃ (f' : P ⟶ E), f' ≫ X_1 = E_1
Tactic: refine ⟨fun E X epi => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Projective (goal)
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
E_1 X_1 : ModuleCat.{v, u} R
E : P ⟶ X_1
X : E_1 ⟶ X_1
epi : Epi X
⊢ ∃ (f' : P ⟶ E_1), f' ≫ X = E
have obtain : ∀ (f : (↑P : Type v) →ₗ[R] (↑E_1 : Type v)) (h : Hom.hom X ∘ₗ f = Hom.hom E), ∃ (f' : P ⟶ E_1), f' ≫ X = E
Tactic: obtain ⟨f, h⟩ := Module.projective_lifting_property X.hom E.hom
    ((ModuleCat.epi_iff_surjective _).mp epi)