awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : Cofork (F.map left) (F.map right)
rw :
  F.map (𝟙 zero) ≫
      NatTrans.app
        (Cocone.ι
          { pt := G.pt,
            ι :=
              Iso.hom
                  (diagramIsoParallelPair
                    {
                      obj := fun (X : WalkingParallelPair) ↦
                        F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                      map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                        F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                      map_id := ⋯, map_comp := ⋯ }) ≫
                G.ι })
        WalkingParallelPair.one =
    G.π
⊢ NatTrans.app
      (Cocone.ι
        (Functor.obj (C :=
          Cocone.{0, v, 0, u} (J := WalkingParallelPair) (C := C)
            { obj := fun (X : WalkingParallelPair) ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
              map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
              map_id := ⋯, map_comp := ⋯ })
          Functor.Final.extendCocone
          { pt := G.pt,
            ι :=
              Iso.hom
                  (diagramIsoParallelPair
                    {
                      obj := fun (X : WalkingParallelPair) ↦
                        F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                      map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                        F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                      map_id := ⋯, map_comp := ⋯ }) ≫
                G.ι }))
      zero =
    G.π

Tactic:
rw [Functor.Final.extendCocone_obj_ι_app' (Y := .one) (f := 𝟙 zero)]

Premises used: CategoryTheory.Functor.Final.extendCocone_obj_ι_app'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : Cofork (F.map left) (F.map right)
⊢ F.map (𝟙 zero) ≫
      NatTrans.app
        (Cocone.ι
          { pt := G.pt,
            ι :=
              Iso.hom
                  (diagramIsoParallelPair
                    {
                      obj := fun (X : WalkingParallelPair) ↦
                        F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                      map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                        F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                      map_id := ⋯, map_comp := ⋯ }) ≫
                G.ι })
        WalkingParallelPair.one =
    G.π

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π ≫
      Iso.hom (Iso.refl ((reflexiveCoforkEquivCofork F).functor.obj G).pt) =
    G.toCofork.π

Tactic:
simp [reflexiveCoforkEquivCofork, Cofork.π]

Premises used: CategoryTheory.Limits.reflexiveCoforkEquivCofork, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
⊢ HasColimit F ↔ HasCoequalizer (F.map left) (F.map right)

Tactic:
simpa only [hasColimit_iff_hasInitial_cocone]
    using Equivalence.hasInitial_iff (reflexiveCoforkEquivCofork F)

Premises used: CategoryTheory.Limits.reflexiveCoforkEquivCofork, CategoryTheory.Equivalence.hasInitial_iff, CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
h : HasCoequalizer (F.map left) (F.map right)
⊢ HasColimit F

Tactic:
hasReflexiveCoequalizer_iff_hasCoequalizer _ |>.mpr h

Premises used: Iff.mpr, CategoryTheory.Limits.hasReflexiveCoequalizer_iff_hasCoequalizer
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
inst_1 : HasCoequalizer (F.map left) (F.map right)
⊢ Eq (α := F.obj zero ⟶ coequalizer (F.map left) (F.map right))
    (colimit.ι F zero ≫ Iso.hom (reflexiveCoequalizerIsoCoequalizer F)) (coequalizer.π (F.map left) (F.map right))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom
    ((ReflexiveCofork.isColimitEquiv F _).symm _) _ WalkingParallelPair.one

Premises used: CategoryTheory.Limits.ReflexiveCofork.isColimitEquiv, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, Equiv.symm, CategoryTheory.Limits.parallelPair, DFunLike.coe, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
inst_1 : HasCoequalizer (F.map left) (F.map right)
rw :
  Eq (α := F.obj zero ⟶ colimit F)
    (CategoryStruct.comp (Y := coequalizer (F.map left) (F.map right)) (coequalizer.π (F.map left) (F.map right))
        (Iso.inv
          (IsColimit.coconePointUniqueUpToIso
            ((Equiv.symm (ReflexiveCofork.isColimitEquiv F (colimit.cocone F)) :
                (a : IsColimit (colimit.cocone F)) → IsColimit (ReflexiveCofork.toCofork (colimit.cocone F)))
              (colimit.isColimit F))
            (colimit.isColimit (parallelPair (F.map left) (F.map right))))) :
      F.obj zero ⟶ colimit F)
    (colimit.ι F zero : F.obj zero ⟶ colimit F)
⊢ Eq (α := F.obj zero ⟶ colimit F)
    (CategoryStruct.comp (Y := coequalizer (F.map left) (F.map right)) (coequalizer.π (F.map left) (F.map right))
        (Iso.inv (reflexiveCoequalizerIsoCoequalizer F)) :
      F.obj zero ⟶ colimit F)
    (colimit.ι F zero : F.obj zero ⟶ colimit F)

Tactic:
rw [reflexiveCoequalizerIsoCoequalizer]

Premises used: CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
inst_1 : HasCoequalizer (F.map left) (F.map right)
⊢ Eq (α := F.obj zero ⟶ colimit F)
    (CategoryStruct.comp (Y := coequalizer (F.map left) (F.map right)) (coequalizer.π (F.map left) (F.map right))
        (Iso.inv
          (IsColimit.coconePointUniqueUpToIso
            ((Equiv.symm (ReflexiveCofork.isColimitEquiv F (colimit.cocone F)) :
                (a : IsColimit (colimit.cocone F)) → IsColimit (ReflexiveCofork.toCofork (colimit.cocone F)))
              (colimit.isColimit F))
            (colimit.isColimit (parallelPair (F.map left) (F.map right))))) :
      F.obj zero ⟶ colimit F)
    (colimit.ι F zero : F.obj zero ⟶ colimit F)

Tactic:
simp only [colimit.comp_coconePointUniqueUpToIso_inv, Cofork.ofπ_pt, colimit.cocone_x,
    Cofork.ofπ_ι_app, colimit.cocone_ι]

Premises used: CategoryTheory.Limits.colimit.cocone_ι, CategoryTheory.Limits.colimit.cocone_x, CategoryTheory.Limits.Cofork.ofπ_pt, CategoryTheory.Limits.Cofork.ofπ_ι_app, CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
h : HasCoequalizer f g
⊢ HasColimit (ofIsReflexivePair f g)

Tactic:
hasReflexiveCoequalizer_iff_hasCoequalizer _ |>.mpr h

Premises used: Iff.mpr, CategoryTheory.Limits.hasReflexiveCoequalizer_iff_hasCoequalizer
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
h : HasCoequalizer f g
⊢ Eq (α := (ofIsReflexivePair f g).obj zero ⟶ coequalizer f g)
    (colimit.ι (ofIsReflexivePair f g) zero ≫ Iso.hom colimitOfIsReflexivePairIsoCoequalizer) (coequalizer.π f g)

Tactic:
@ι_reflexiveCoequalizerIsoCoequalizer_hom _ _ _ h

Premises used: CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
h : HasCoequalizer f g
⊢ Eq (α := B ⟶ colimit (ofIsReflexivePair f g))
    (CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (Iso.inv colimitOfIsReflexivePairIsoCoequalizer) :
      B ⟶ colimit (ofIsReflexivePair f g))
    (colimit.ι (ofIsReflexivePair f g) zero : (ofIsReflexivePair f g).obj zero ⟶ colimit (ofIsReflexivePair f g))

Tactic:
@π_reflexiveCoequalizerIsoCoequalizer_inv _ _ (ofIsReflexivePair f g) h

Premises used: CategoryTheory.Limits.ofIsReflexivePair, CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
⊢ HasColimitsOfShape.{0, 0, v, u} WalkingReflexivePair C ↔ HasReflexiveCoequalizers.{v, u} C

Tactic:
⟨fun _ ↦ ⟨fun _ _ f g _ ↦ (hasReflexiveCoequalizer_iff_hasCoequalizer
      (reflexivePair f g (commonSection f g))).1 inferInstance⟩,
    fun _ ↦ ⟨inferInstance⟩⟩

Premises used: CategoryTheory.Limits.hasReflexiveCoequalizer_iff_hasCoequalizer, CategoryTheory.Limits.HasColimitsOfShape.mk, inferInstance, CategoryTheory.commonSection, CategoryTheory.Limits.HasReflexiveCoequalizers.mk, Iff.intro, Iff.mp, CategoryTheory.Limits.reflexivePair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
⊢ Mono f

Tactic:
mono_of_isLimit_fork h.isLimit

Premises used: CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.Limits.Fork.ι, CategoryTheory.RegularMono.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Fork.{v₁, u₁} (𝟙 Y) (𝟙 Y)), (fun (s : Fork.{v₁, u₁} (𝟙 Y) (𝟙 Y)) ↦ s.ι ≫ e.inv) s ≫ (Fork.ofι e.hom ⋯).ι = s.ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
s : Fork.{v₁, u₁} (𝟙 Y) (𝟙 Y)
m : s.pt ⟶ (Fork.ofι e.hom ⋯).pt
w : m ≫ (Fork.ofι e.hom ⋯).ι = s.ι
⊢ m = (fun (s : Fork.{v₁, u₁} (𝟙 Y) (𝟙 Y)) ↦ s.ι ≫ e.inv) s

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularMono f
⊢ g ≫ Arrow.Hom.right e.inv ≫ h.left = g ≫ Arrow.Hom.right e.inv ≫ h.right

Tactic:
simp only [← (Arrow.w_mk_assoc e.inv), h.w]

Premises used: CategoryTheory.Arrow.w_mk_assoc, CategoryTheory.RegularMono.w, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ regularMono C f ↔ IsRegularMono f

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.regularMono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
⊢ RespectsIso.{v₁, u₁} (regularMono C)

Tactic:
RespectsIso.of_respects_arrow_iso _ (fun _ _ e h ↦ ⟨⟨.ofArrowIso e (h := h.regularMono.some)⟩⟩)

Premises used: CategoryTheory.RegularMono.ofArrowIso, Nonempty.some, CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso, CategoryTheory.IsRegularMono.regularMono, Nonempty.intro, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
⊢ IsRegularMono f

Tactic:
⟨⟨h⟩⟩

Premises used: Nonempty.intro, CategoryTheory.IsRegularMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsRegularMono f
⊢ Eq (α := X ⟶ Z f) (f ≫ left f) (f ≫ right f)

Tactic:
(IsRegularMono.getStruct f).w

Premises used: CategoryTheory.IsRegularMono.Z, CategoryTheory.IsRegularMono.getStruct, CategoryTheory.IsRegularMono.left, CategoryTheory.RegularMono.w, CategoryTheory.IsRegularMono.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y W : C
f : X ⟶ Y
inst_1 : IsRegularMono f
k : W ⟶ Y
h : Eq (α := W ⟶ Z f) (k ≫ left f) (k ≫ right f)
⊢ lift f k h ≫ f = k

Tactic:
Fork.IsLimit.lift_ι (isLimit f)

Premises used: CategoryTheory.IsRegularMono.isLimit, CategoryTheory.Limits.Fork.IsLimit.lift, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.IsRegularMono.lift, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y W : C
f : X ⟶ Y
inst_1 : IsRegularMono f
k : W ⟶ Y
h : Eq (α := W ⟶ Z f) (k ≫ left f) (k ≫ right f)
m : W ⟶ X
hm : m ≫ f = k
⊢ lift f k h ≫ Fork.ι (Fork.ofι f ⋯) = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst_1 : HasLimit (parallelPair g h)
⊢ ∀ (s : Fork g h),
    (fun (s : Fork g h) ↦ (limit.lift (parallelPair g h) s : s.pt ⟶ limit (parallelPair g h))) s ≫
        (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).ι =
      s.ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst_1 : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).pt
w : m ≫ (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).ι = s.ι
h₁ :
  m ≫ equalizer.ι g h =
    CategoryStruct.comp (Y := Limits.equalizer g h)
      ((fun (s : Fork g h) ↦ (limit.lift (parallelPair g h) s : s.pt ⟶ limit (parallelPair g h))) s) (equalizer.ι g h)
⊢ m = (fun (s : Fork g h) ↦ (limit.lift (parallelPair g h) s : s.pt ⟶ limit (parallelPair g h))) s

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst_1 : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).pt
w : m ≫ (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).ι = s.ι
⊢ m ≫ equalizer.ι g h =
    CategoryStruct.comp (Y := Limits.equalizer g h)
      ((fun (s : Fork g h) ↦ (limit.lift (parallelPair g h) s : s.pt ⟶ limit (parallelPair g h))) s) (equalizer.ι g h)

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst_1 : HasLimit (parallelPair g h)
⊢ IsRegularMono (X := equalizer g h) (equalizer.ι g h)

Tactic:
isRegularMono_of_regularMono <| RegularMono.equalizer g h

Premises used: CategoryTheory.isRegularMono_of_regularMono, CategoryTheory.RegularMono.equalizer
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsSplitMono f
⊢ IsRegularMono f

Tactic:
isRegularMono_of_regularMono <| .ofIsSplitMono f

Premises used: CategoryTheory.isRegularMono_of_regularMono, CategoryTheory.RegularMono.ofIsSplitMono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
rw : (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
rw [← Category.assoc, ← eq_whisker comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
rw : (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
⊢ (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
rw [← Category.assoc, ← eq_whisker comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
repeat : (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
repeat (rw [← Category.assoc, ← eq_whisker comm])

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right

Tactic:
simp only [Category.assoc, hr.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.RegularMono.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
apply :
  (s : Fork (k ≫ hr.left) (k ≫ hr.right)) →
    { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
      l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
⊢ IsLimit (Fork.ofι g ⋯)

Tactic:
apply Fork.IsLimit.mk' _ _

Premises used: CategoryTheory.Limits.Fork.IsLimit.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
rw : s.ι ≫ k ≫ hr.left = (s.ι ≫ k) ≫ hr.right
rw₁ : s.ι ≫ k ≫ hr.right = (s.ι ≫ k) ≫ hr.right
rw₂ rw₃ : s.ι ≫ k ≫ hr.right = s.ι ≫ k ≫ hr.right
⊢ (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right

Tactic:
rw [Category.assoc, s.condition, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
⊢ (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right

Tactic:
have l₁ : (Fork.ι s ≫ k) ≫ hr.left = (Fork.ι s ≫ k) ≫ hr.right := by
      rw [Category.assoc, s.condition, Category.assoc]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
obtain :
  (l : s.pt ⟶ (Fork.ofι h ⋯).pt) →
    (hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k) →
      { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
        l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift', CategoryTheory.RegularMono.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
obtain :
  (p : s.pt ⟶ (PullbackCone.mk f g comm).pt) →
    p ≫ (PullbackCone.mk f g comm).fst = l →
      (hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι) →
        { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
          l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
refine : ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = p
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
refine ⟨p, hp₂, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
⊢ m ≫ g = p ≫ g

Tactic:
have z : m ≫ g = p ≫ g := w.trans hp₂.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
apply : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j
⊢ m = p

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
⊢ Mono h

Tactic:
have := hr.mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
h₀ : m ≫ (PullbackCone.mk f g comm).fst = p ≫ (PullbackCone.mk f g comm).fst
h₁ : m ≫ (PullbackCone.mk f g comm).snd = p ≫ (PullbackCone.mk f g comm).snd
⊢ ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j

Tactic:
apply (PullbackCone.mk f g comm).equalizer_ext

Premises used: CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.PullbackCone.equalizer_ext