awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat R
f : M ⟶ N
x y : (↑N : Type u)
m : (↑M : Type u)
w :
  x =
    HAdd.hAdd (β := (↑N : Type u)) y
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑M : Type u)) → (↑N : Type u))
          m :
        (↑N : Type u))
⊢ Eq (α := (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        x :
      (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        y :
      (↑(cokernel f) : Type u))
have subst : Eq (α := (↑(cokernel f) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
          cokernel f) (cokernel.π f) :
        (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
      (HAdd.hAdd (β := (↑N : Type u)) y
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
                f :
              (a : (↑M : Type u)) → (↑N : Type u))
            m :
          (↑N : Type u))) :
    (↑(cokernel f) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
          cokernel f) (cokernel.π f) :
        (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
      y :
    (↑(cokernel f) : Type u))
Tactic: subst w
Cleared hypotheses: x, w
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.LeftResolution (hypothesis)
Goal:
R : Type u
inst : Ring R
X : Type u
M N : ModuleCat R
f : Functor.obj (free R) X ⟶ N
p : M ⟶ N
hp : Epi p
⊢ ∃ (f' : Functor.obj (free R) X ⟶ M), f' ≫ p = f
have hp₁ : Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) p) :
    (a : (↑M : Type u)) → (↑N : Type u))
Tactic: rw [epi_iff_surjective] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.LeftResolution (goal)
Goal:
R : Type u
inst : Ring R
X : Type u
M N : ModuleCat R
f : Functor.obj (free R) X ⟶ N
p : M ⟶ N
hp :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) p) :
      (a : (↑M : Type u)) → (↑N : Type u))
⊢ ∃ (f' : Functor.obj (free R) X ⟶ M), f' ≫ p = f
have obtain : ∀ (s : (↑N : Type u) → (↑M : Type u))
  (hs :
    Function.RightInverse s
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            p) :
        (a : (↑M : Type u)) → (↑N : Type u))),
  ∃ (f' : Functor.obj (free R) X ⟶ M), f' ≫ p = f
Tactic: obtain ⟨s, hs⟩ := hp.hasRightInverse
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
x x_1 : J
f : x ⟶ x_1
⊢ Eq.{w + 1} (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                    (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
        x ⟶
      F.obj x_1)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                    (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
        f ≫
      ↟(limitπLinearMap F x_1))
    (↟(limitπLinearMap F x) ≫ F.map f)
have hf : ∀
  (x_2 :
    (↑(Functor.obj
          (Functor.obj (Functor.const J)
            (of R
              (Types.Small.limitCone
                  (F ⋙
                    forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                      (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
          x) :
      Type w)),
  Eq (α := (↑(F.obj x_1) : Type w))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of R
                    (Types.Small.limitCone
                        (F ⋙
                          forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
                f ≫
              ↟(limitπLinearMap F x_1)) :
          (a :
              (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x) :
                Type w)) →
            (↑(F.obj x_1) : Type w))
        x_2 :
      (↑(F.obj x_1) : Type w))
    ((Hom.hom (↟(limitπLinearMap F x) ≫ F.map f) :
          (a :
              (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x) :
                Type w)) →
            (↑(F.obj x_1) : Type w))
        x_2 :
      (↑(F.obj x_1) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (hypothesis)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
c : Cone F
hc :
  IsLimit (F :=
    F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
      c)
⊢ IsLimit c
have this : HasLimit
  (F ⋙
    forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
      carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
      AddCommGrpCat.carrier))
Tactic: have : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) := ⟨_, hc⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (hypothesis)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
c : Cone F
hc :
  IsLimit (F :=
    F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
      c)
this :
  HasLimit
    (F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
⊢ IsLimit c
have this₁ : Small.{w, max v w}
  (↑(F ⋙
          forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
            (CC := carrier)).sections :
    Type (max v w))
Tactic: have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using this
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
i : ι
⊢ ↟(f i i ⋯) = 𝟙 (of R (G i))
have hf : ∀ (x : (↑(of R (G i)) : Type v)),
  Eq (α := (↑(of R (G i)) : Type v))
    ((Hom.hom (↟(f i i sorry)) : (a : (↑(of R (G i)) : Type v)) → (↑(of R (G i)) : Type v)) x : (↑(of R (G i)) : Type v))
    ((Hom.hom (𝟙 (of R (G i))) : (a : (↑(of R (G i)) : Type v)) → (↑(of R (G i)) : Type v)) x :
      (↑(of R (G i)) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
X Y Z : ι
hij : X ⟶ Y
hjk : Y ⟶ Z
⊢ ↟(f X Z ⋯) = ↟(f X Y ⋯) ≫ ↟(f Y Z ⋯)
have hf : ∀ (x : (↑(of R (G X)) : Type v)),
  Eq (α := (↑(of R (G Z)) : Type v))
    ((Hom.hom (↟(f X Z sorry)) : (a : (↑(of R (G X)) : Type v)) → (↑(of R (G Z)) : Type v)) x : (↑(of R (G Z)) : Type v))
    ((Hom.hom (↟(f X Y sorry) ≫ ↟(f Y Z sorry)) : (a : (↑(of R (G X)) : Type v)) → (↑(of R (G Z)) : Type v)) x :
      (↑(of R (G Z)) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
X Y Z : ι
hij : X ⟶ Y
hjk : Y ⟶ Z
x : (↑(of R (G X)) : Type v)
⊢ Eq (α := (↑(of R (G Z)) : Type v))
    ((Hom.hom (↟(f X Z ⋯)) : (a : (↑(of R (G X)) : Type v)) → (↑(of R (G Z)) : Type v)) x : (↑(of R (G Z)) : Type v))
    ((Hom.hom (↟(f X Y ⋯) ≫ ↟(f Y Z ⋯)) : (a : (↑(of R (G X)) : Type v)) → (↑(of R (G Z)) : Type v)) x :
      (↑(of R (G Z)) : Type v))
have hf : Eq (α := (↑(of R (G Z)) : Type v))
  ((Hom.hom (↟(f X Y sorry) ≫ ↟(f Y Z sorry)) : (a : (↑(of R (G X)) : Type v)) → (↑(of R (G Z)) : Type v)) x :
    (↑(of R (G Z)) : Type v))
  ((Hom.hom (↟(f X Z sorry)) : (a : (↑(of R (G X)) : Type v)) → (↑(of R (G Z)) : Type v)) x : (↑(of R (G Z)) : Type v))
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
x x_1 : ι
hij : x ⟶ x_1
⊢ Eq (α :=
    (directLimitDiagram G f).obj x ⟶ Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) x_1)
    ((directLimitDiagram G f).map hij ≫ ↟(DirectLimit.of R ι G f x_1))
    (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) x)
      (↟(DirectLimit.of R ι G f x))
      (CategoryTheory.Functor.map (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) hij))
have hf : ∀ (x_2 : (↑((directLimitDiagram G f).obj x) : Type v)),
  Eq (α := (↑(Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) x_1) : Type v))
    ((Hom.hom ((directLimitDiagram G f).map hij ≫ ↟(DirectLimit.of R ι G f x_1)) :
          (a : (↑((directLimitDiagram G f).obj x) : Type v)) →
            (↑(((Functor.const ι).obj (of R (Module.DirectLimit G f))).obj x_1) : Type v))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) x_1) : Type v))
    ((Hom.hom
            (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) x)
              (↟(DirectLimit.of R ι G f x))
              (CategoryTheory.Functor.map (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) hij)) :
          (a : (↑((directLimitDiagram G f).obj x) : Type v)) →
            (↑(((Functor.const ι).obj (of R (Module.DirectLimit G f))).obj x_1) : Type v))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) x_1) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ Eq (α := (↑s.1 : Type v))
    ((Hom.hom (s.ι.app j) : (a : G j) → (↑s.1 : Type v)) ((f i j h : (a : G i) → G j) x : G j) : (↑s.1 : Type v))
    ((Hom.hom (s.ι.app i) : (a : G i) → (↑s.1 : Type v)) x : (↑s.1 : Type v))
have rw : Eq (α := (↑s.1 : Type v))
  ((Hom.hom (s.ι.app j) : (a : G j) → (↑s.1 : Type v)) ((f i j h : (a : G i) → G j) x : G j) : (↑s.1 : Type v))
  ((Hom.hom ((directLimitDiagram G f).map (homOfLE h) ≫ s.ι.app j) : (a : G i) → (↑s.1 : Type v)) x : (↑s.1 : Type v))
Tactic: rw [← s.w (homOfLE h)]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
i : ι
⊢ CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const ι) (Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f))) i)
      (NatTrans.app (Cocone.ι (directLimitCocone G f)) i)
      (↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) ⋯)) =
    s.ι.app i
have hf : ∀ (x : (↑((directLimitDiagram G f).obj i) : Type v)),
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom
            (CategoryStruct.comp (Y :=
              Functor.obj
                (Functor.obj (Functor.const ι) (Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f))) i)
              (NatTrans.app (Cocone.ι (directLimitCocone G f)) i)
              (↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) sorry))) :
          (a : (↑((directLimitDiagram G f).obj i) : Type v)) → (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))
    ((Hom.hom (s.ι.app i) : (a : (↑((directLimitDiagram G f).obj i) : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
i : ι
x : (↑((directLimitDiagram G f).obj i) : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom
            (CategoryStruct.comp (Y :=
              Functor.obj
                (Functor.obj (Functor.const ι) (Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f))) i)
              (NatTrans.app (Cocone.ι (directLimitCocone G f)) i)
              (↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) ⋯))) :
          (a : (↑((directLimitDiagram G f).obj i) : Type v)) → (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))
    ((Hom.hom (s.ι.app i) : (a : (↑((directLimitDiagram G f).obj i) : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
have hf : Eq (α := (↑s.pt : Type v))
  ((Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) sorry :
        (a : (↑(((Functor.const ι).obj (of R (Module.DirectLimit G f))).obj i) : Type v)) → (↑s.pt : Type v))
      ((DirectLimit.of R ι G f i :
            (a : (↑((directLimitDiagram G f).obj i) : Type v)) →
              (↑(((Functor.const ι).obj (of R (Module.DirectLimit G f))).obj i) : Type v))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const ι) (of R (Module.DirectLimit G f))) i) : Type v)) :
    (↑s.pt : Type v))
  ((Hom.hom (s.ι.app i) : (a : (↑((directLimitDiagram G f).obj i) : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
Tactic: dsimp only [hom_comp, directLimitCocone, hom_ofHom, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
m : Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f) ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (Cocone.ι (directLimitCocone G f)) j ≫ m = s.ι.app j
⊢ s.ι.app = fun (i : ι) ↦ ↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m
have h₁ : ∀ (i : ι), s.ι.app i = ↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
m : Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f) ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (Cocone.ι (directLimitCocone G f)) j ≫ m = s.ι.app j
i : ι
⊢ s.ι.app i = ↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m
have h₁ : Eq (α := (directLimitDiagram G f).obj i ⟶ Functor.obj (Functor.obj (Functor.const ι) s.pt) i)
  (NatTrans.app (Cocone.ι (directLimitCocone G f)) i ≫ m)
  (↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (hypothesis)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
m : Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f) ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (Cocone.ι (directLimitCocone G f)) j ≫ m = s.ι.app j
⊢ m = ↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) ⋯)
have this : s.ι.app = fun (i : ι) ↦ ↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m
Tactic: have :
      s.ι.app = fun i =>
        (ofHom (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) ≫ m := by
      funext i
      rw [← h]
      rfl
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Limits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
m : Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f) ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (Cocone.ι (directLimitCocone G f)) j ≫ m = s.ι.app j
this : s.ι.app = fun (i : ι) ↦ ↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m
⊢ m = ↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) ⋯)
have hf : ∀ (x : (↑(Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f)) : Type v)),
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(directLimitCocone G f).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) sorry)) :
          (a : (↑(directLimitCocone G f).pt : Type v)) → (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Localization (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X Y Z : ModuleCat.{v, u} R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := X.localizedModule S ⟶ Z.localizedModule S) (localizedModuleMap S (f ≫ g))
    (localizedModuleMap S f ≫ localizedModuleMap S g)
have hf : ∀ (x : (↑(X.localizedModule S) : Type v)),
  Eq (α := (↑(Z.localizedModule S) : Type v))
    ((Hom.hom (localizedModuleMap S (f ≫ g)) :
          (a : (↑(X.localizedModule S) : Type v)) → (↑(Z.localizedModule S) : Type v))
        x :
      (↑(Z.localizedModule S) : Type v))
    ((Hom.hom (localizedModuleMap S f ≫ localizedModuleMap S g) :
          (a : (↑(X.localizedModule S) : Type v)) → (↑(Z.localizedModule S) : Type v))
        x :
      (↑(Z.localizedModule S) : Type v))
Tactic: ext