awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≫ f) ≫ h = (p ≫ f) ≫ h
⊢ m ≫ (PullbackCone.mk f g comm).fst = p ≫ (PullbackCone.mk f g comm).fst

Tactic:
simp only [PullbackCone.mk_π_app, ← cancel_mono h]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.cancel_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
⊢ (m ≫ f) ≫ h = (p ≫ f) ≫ h

Tactic:
grind [Fork.ofι, PullbackCone.mk]

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.PullbackCone.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)
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
⊢ m ≫ (PullbackCone.mk f g comm).snd = p ≫ (PullbackCone.mk f g comm).snd

Tactic:
z
-- 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
⊢ m ≫ (PullbackCone.mk f g comm).snd = p ≫ (PullbackCone.mk f g comm).snd

Tactic:
exact z
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
apply : z ≫ v ≫ h.left = z ≫ v ≫ h.right
⊢ v ≫ h.left = v ≫ h.right

Tactic:
apply (cancel_epi z).1

Premises used: Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
rw : (u ≫ f) ≫ h.left = z ≫ v ≫ h.right
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right

Tactic:
rw [← Category.assoc, ← eq_whisker sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
rw : (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
⊢ (u ≫ f) ≫ h.left = z ≫ v ≫ h.right

Tactic:
rw [← Category.assoc, ← eq_whisker sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
repeat : (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right

Tactic:
simp only [Category.assoc, RegularMono.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 : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ v ≫ h.left = v ≫ h.right

Tactic:
have : v ≫ h.left = v ≫ h.right := by
        apply (cancel_epi z).1
        repeat (rw [← Category.assoc, ← eq_whisker sq.w])
        simp only [Category.assoc, RegularMono.w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this_1 : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
obtain : ∀ (t : B ⟶ X) (ht : t ≫ f = v), sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨t, ht⟩ := RegularMono.lift' _ _ this

Premises used: CategoryTheory.RegularMono.lift'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this_1 : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
t : B ⟶ X
ht : t ≫ f = v
⊢ sq.HasLift

Tactic:
CommSq.HasLift.mk' ⟨t, (cancel_mono f).1 ?_, ht⟩

Premises used: CategoryTheory.CommSq.HasLift.mk', CategoryTheory.cancel_mono, CategoryTheory.CommSq.LiftStruct.mk, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this_1 : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
t : B ⟶ X
ht : t ≫ f = v
refine : (z ≫ t) ≫ f = u ≫ f
⊢ sq.HasLift

Tactic:
refine CommSq.HasLift.mk' ⟨t, (cancel_mono f).1 ?_, ht⟩

Premises used: CategoryTheory.CommSq.HasLift.mk', CategoryTheory.cancel_mono, CategoryTheory.CommSq.LiftStruct.mk, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this_1 : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
t : B ⟶ X
ht : t ≫ f = v
⊢ (z ≫ t) ≫ f = u ≫ f

Tactic:
simp only [Category.assoc, ht, sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.w
-- 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
⊢ StrongMono f

Tactic:
IsRegularMono.getStruct f |>.strongMono

Premises used: CategoryTheory.RegularMono.strongMono, CategoryTheory.IsRegularMono.getStruct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
inst_1 : Epi f
⊢ IsIso f

Tactic:
have := RegularMono.strongMono h
  isIso_of_epi_of_strongMono _

Premises used: CategoryTheory.isIso_of_epi_of_strongMono, CategoryTheory.RegularMono.strongMono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularEpi f
⊢ Epi f

Tactic:
epi_of_isColimit_cofork h.isColimit

Premises used: CategoryTheory.RegularEpi.isColimit, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Cofork.{v₁, u₁} (𝟙 X) (𝟙 X)),
    (Cofork.ofπ e.hom ⋯).π ≫ (fun (s : Cofork.{v₁, u₁} (𝟙 X) (𝟙 X)) ↦ e.inv ≫ s.π) s = 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 : Cofork.{v₁, u₁} (𝟙 X) (𝟙 X)
m : (Cofork.ofπ e.hom ⋯).pt ⟶ s.pt
w : (Cofork.ofπ e.hom ⋯).π ≫ m = s.π
⊢ m = (fun (s : Cofork.{v₁, u₁} (𝟙 X) (𝟙 X)) ↦ e.inv ≫ s.π) 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 : RegularEpi f
simp : h.left ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom
⊢ (h.left ≫ Arrow.Hom.left e.hom) ≫ g = (h.right ≫ Arrow.Hom.left e.hom) ≫ g

Tactic:
simp only [Category.assoc, Arrow.w_mk_right, Arrow.mk_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Arrow.w_mk_right, CategoryTheory.Arrow.mk_hom
-- 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 : RegularEpi f
rw rw₁ : h.right ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom
⊢ h.left ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom

Tactic:
rw [reassoc_of% h.w]

Premises used: CategoryTheory.RegularEpi.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ regularEpi C f ↔ IsRegularEpi f

Tactic:
Iff.rfl

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

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

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

Tactic:
⟨⟨h⟩⟩

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

Tactic:
(IsRegularEpi.getStruct f).w

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

Tactic:
Cofork.IsColimit.π_desc (isColimit f)

Premises used: CategoryTheory.IsRegularEpi.desc, CategoryTheory.IsRegularEpi.isColimit, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.Cofork.IsColimit.desc, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
inst_1 : IsRegularEpi f
k : X ⟶ Z
h : Eq (α := W f ⟶ Z) (left f ≫ k) (right f ≫ k)
m : Y ⟶ Z
hm : f ≫ m = k
⊢ Cofork.π (Cofork.ofπ f ⋯) ≫ desc f k h = 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 : HasColimit (parallelPair g h)
⊢ ∀ (s : Cofork g h),
    (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).π ≫
        (fun (s : Cofork g h) ↦ (colimit.desc (parallelPair g h) s : colimit (parallelPair g h) ⟶ s.pt)) s =
      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 : HasColimit (parallelPair g h)
s : Cofork g h
m : (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).pt ⟶ s.pt
w : (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).π ≫ m = s.π
h₁ :
  coequalizer.π g h ≫ m =
    CategoryStruct.comp (Y := coequalizer g h) (coequalizer.π g h)
      ((fun (s : Cofork g h) ↦ (colimit.desc (parallelPair g h) s : colimit (parallelPair g h) ⟶ s.pt)) s)
⊢ m = (fun (s : Cofork g h) ↦ (colimit.desc (parallelPair g h) s : colimit (parallelPair g h) ⟶ s.pt)) s

Tactic:
apply coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.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 : HasColimit (parallelPair g h)
s : Cofork g h
m : (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).pt ⟶ s.pt
w : (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).π ≫ m = s.π
⊢ coequalizer.π g h ≫ m =
    CategoryStruct.comp (Y := coequalizer g h) (coequalizer.π g h)
      ((fun (s : Cofork g h) ↦ (colimit.desc (parallelPair g h) s : colimit (parallelPair g h) ⟶ s.pt)) s)

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 : HasColimit (parallelPair g h)
⊢ IsRegularEpi (Y := coequalizer g h) (coequalizer.π g h)

Tactic:
⟨⟨coequalizerRegular g h⟩⟩

Premises used: CategoryTheory.coequalizerRegular, Nonempty.intro, CategoryTheory.IsRegularEpi.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : Epi f
h :
  ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
    Eq (α := pullback f f ⟶ Z) (pullback.fst f f ≫ g) (pullback.snd f f ≫ g) → ∃ (u : B ⟶ Z), f ≫ u = g
⊢ IsRegularEpi f

Tactic:
⟨⟨regularEpiOfKernelPair _ <| Cofork.IsColimit.mk' _ fun s ↦ ?_⟩⟩

Premises used: CategoryTheory.Limits.Cofork.IsColimit.mk', Nonempty.intro, CategoryTheory.regularEpiOfKernelPair, CategoryTheory.IsRegularEpi.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : Epi f
h :
  ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
    Eq (α := pullback f f ⟶ Z) (pullback.fst f f ≫ g) (pullback.snd f f ≫ g) → ∃ (u : B ⟶ Z), f ≫ u = g
refine :
  (s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) →
    { l :
      Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt //
      Cofork.π (Cofork.ofπ f ⋯) ≫ l = s.π ∧
        ∀
          {m :
            Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
              s.pt},
          Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π → m = l }
⊢ IsRegularEpi f

Tactic:
refine ⟨⟨regularEpiOfKernelPair _ <| Cofork.IsColimit.mk' _ fun s ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : Epi f
h :
  ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
    Eq (α := pullback f f ⟶ Z) (pullback.fst f f ≫ g) (pullback.snd f f ≫ g) → ∃ (u : B ⟶ Z), f ≫ u = g
s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)
choose :
  (g : B ⟶ s.pt) →
    (hg : f ≫ g = s.π) →
      { l :
        Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
          s.pt //
        Cofork.π (Cofork.ofπ f ⋯) ≫ l = s.π ∧
          ∀
            {m :
              Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
                s.pt},
            Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π → m = l }
⊢ { l :
    Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt //
    Cofork.π (Cofork.ofπ f ⋯) ≫ l = s.π ∧
      ∀
        {m :
          Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
            s.pt},
        Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π → m = l }

Tactic:
choose g hg using h s.condition

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : Epi f
h :
  ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
    Eq (α := pullback f f ⟶ Z) (pullback.fst f f ≫ g) (pullback.snd f f ≫ g) → ∃ (u : B ⟶ Z), f ≫ u = g
s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
refine :
  ∀
    {m :
      Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt}
    (hm : Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π), m = g
⊢ { l :
    Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt //
    Cofork.π (Cofork.ofπ f ⋯) ≫ l = s.π ∧
      ∀
        {m :
          Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
            s.pt},
        Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π → m = l }

Tactic:
refine ⟨g, hg, fun hm ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : Epi f
h :
  ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
    Eq (α := pullback f f ⟶ Z) (pullback.fst f f ≫ g) (pullback.snd f f ≫ g) → ∃ (u : B ⟶ Z), f ≫ u = g
s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m : Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt
hm : Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π
rwa : f ≫ m = f ≫ g
rwa₁ rwa₂ rwa₃ rwa₄ : f ≫ m = s.π
⊢ m = g

Tactic:
rwa [← cancel_epi f, hg]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B X : C
f : X ⟶ B
h : RegularEpi f
⊢ EffectiveEpi f

Tactic:
⟨⟨effectiveEpiStructOfRegularEpi h⟩⟩

Premises used: Nonempty.intro, CategoryTheory.effectiveEpiStructOfRegularEpi, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
h : IsRegularEpi f
⊢ EffectiveEpi f

Tactic:
IsRegularEpi.getStruct f |>.effectiveEpi

Premises used: CategoryTheory.IsRegularEpi.getStruct, CategoryTheory.RegularEpi.effectiveEpi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B X : C
f : X ⟶ B
inst_1 : HasPullback f f
hc : IsColimit (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯)
⊢ EffectiveEpi f

Tactic:
RegularEpi.effectiveEpi <| regularEpiOfKernelPair f hc

Premises used: CategoryTheory.regularEpiOfKernelPair, CategoryTheory.RegularEpi.effectiveEpi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
simp : g₁ ≫ Cofork.π s = g₂ ≫ Cofork.π s
⊢ g₁ ≫ s.ι.app WalkingParallelPair.one = g₂ ≫ s.ι.app WalkingParallelPair.one

Tactic:
simp only [Cofork.app_one_eq_π]

Premises used: CategoryTheory.Limits.Cofork.app_one_eq_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
rw : g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero
⊢ g₁ ≫ Cofork.π s = g₂ ≫ Cofork.π s

Tactic:
rw [← PullbackCone.IsLimit.lift_snd hc g₁ g₂ hg,
        Category.assoc, ← Cofork.app_zero_eq_comp_π_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_right, CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
⊢ f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app WalkingParallelPair.one

Tactic:
have := EffectiveEpi.fac f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
      simp only [Cofork.app_one_eq_π]
      rw [← PullbackCone.IsLimit.lift_snd hc g₁ g₂ hg,
        Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
      simp)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
this : f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app WalkingParallelPair.one
⊢ (Cofork.ofπ f ⋯).ι.app WalkingParallelPair.zero ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ =
    s.ι.app WalkingParallelPair.zero

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
this : f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app WalkingParallelPair.one
⊢ (Cofork.ofπ f ⋯).ι.app WalkingParallelPair.one ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ =
    s.ι.app WalkingParallelPair.one

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : EffectiveEpi f
⊢ IsRegularEpi f

Tactic:
isRegularEpi_of_regularEpi <| regularEpiOfEffectiveEpi f

Premises used: CategoryTheory.isRegularEpi_of_regularEpi, CategoryTheory.regularEpiOfEffectiveEpi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
B X : C
f : X ⟶ B
inst_1 : HasPullback f f
⊢ IsRegularEpi f ↔ EffectiveEpi f

Tactic:
⟨fun ⟨_⟩ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, _private.0.CategoryTheory.isRegularEpi_iff_effectiveEpi.match_1, Iff.intro, CategoryTheory.EffectiveEpi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y Z : C
p : Y ⟶ X
hp : EffectiveEpiStruct p
p₁ p₂ : Z ⟶ Y
sq : IsPullback p₁ p₂ p p
s : Cofork p₁ p₂
T : C
g₁ g₂ : T ⟶ Y
h : g₁ ≫ p = g₂ ≫ p
obtain : ∀ (l : T ⟶ Z) (h : (l ≫ p₁) ≫ p = (l ≫ p₂) ≫ p), (l ≫ p₁) ≫ s.π = (l ≫ p₂) ≫ s.π
⊢ g₁ ≫ s.π = g₂ ≫ s.π

Tactic:
obtain ⟨l, rfl, rfl⟩ := sq.exists_lift g₁ g₂ h

Premises used: CategoryTheory.IsPullback.exists_lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y Z : C
p : Y ⟶ X
hp : EffectiveEpiStruct p
p₁ p₂ : Z ⟶ Y
sq : IsPullback p₁ p₂ p p
s : Cofork p₁ p₂
T : C
l : T ⟶ Z
h : (l ≫ p₁) ≫ p = (l ≫ p₂) ≫ p
⊢ (l ≫ p₁) ≫ s.π = (l ≫ p₂) ≫ s.π

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.Cofork.condition