awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ⟶ functor r ⋙ G
x x_1 : Quotient r
X Y : C
f_1 : Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)
f : as (r := r) (mk (r := r) X) ⟶ as (r := r) (mk (r := r) Y)
⊢ Eq (α := F.obj (mk (r := r) X) ⟶ G.obj (mk (r := r) Y))
    (F.map (Quot.mk (HomRel.CompClosure r) f) ≫
      match (motive := (x : Quotient r) → F.obj x ⟶ G.obj x) mk (r := r) Y with
      | { as := X } => τ.app X)
    ((match (motive := (x : Quotient r) → F.obj x ⟶ G.obj x) mk (r := r) X with
      | { as := X } => τ.app X) ≫
      G.map (Quot.mk (HomRel.CompClosure r) f))

Tactic:
exact τ.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ⟶ functor r ⋙ G
X : C
⊢ (natTransLift r τ).app ((functor r).obj X) = τ.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F G H : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ⟶ functor r ⋙ G
τ' : functor r ⋙ G ⟶ functor r ⋙ H
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : natTransLift r τ ≫ natTransLift r τ' = natTransLift r (τ ≫ τ')
⊢ natTransLift r τ ≫ natTransLift r τ' = natTransLift r (τ ≫ τ')

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F
⊢ natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
rw : natTransLift r (τ.hom ≫ τ.inv) = 𝟙 F
rw₁ : natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F
rw₂ rw₃ : 𝟙 F = 𝟙 F
⊢ natTransLift r τ.hom ≫ natTransLift r τ.inv = 𝟙 F

Tactic:
rw [comp_natTransLift, τ.hom_inv_id, natTransLift_id]

Premises used: CategoryTheory.Quotient.natTransLift_id, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Quotient.comp_natTransLift
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F_1.map f₁ = F_1.map f₂
F G : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
τ : functor r ⋙ F ≅ functor r ⋙ G
rw : natTransLift r (τ.inv ≫ τ.hom) = 𝟙 G
rw₁ : natTransLift r (𝟙 (functor r ⋙ G)) = 𝟙 G
rw₂ rw₃ : 𝟙 G = 𝟙 G
⊢ natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G

Tactic:
rw [comp_natTransLift, τ.inv_hom_id, natTransLift_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Quotient.natTransLift_id, CategoryTheory.Quotient.comp_natTransLift
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D
f :
  obj (obj (whiskeringLeft C (Quotient r) D) (functor r)) X ⟶ obj (obj (whiskeringLeft C (Quotient r) D) (functor r)) Y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  map (obj (whiskeringLeft C (Quotient r) D) (functor r)) (natTransLift r f) = f
⊢ map (obj (whiskeringLeft C (Quotient r) D) (functor r)) (natTransLift r f) = f

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ {X Y : Functor.{v_1, v_2, u_1, u_2} (Quotient r) D},
    Function.Injective (α := X ⟶ Y) (β :=
      obj (obj (whiskeringLeft C (Quotient r) D) (functor r)) X ⟶
        obj (obj (whiskeringLeft C (Quotient r) D) (functor r)) Y)
      (map (obj (whiskeringLeft C (Quotient r) D) (functor r)))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Quotient.natTrans_ext
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.Full
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.Full
X Y : C
f : L.obj X ⟶ L.obj Y
obtain :
  ∀ (f : X ⟶ Y),
    ∃ (a : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) X) (Quotient.mk (r := L.homRel) Y)),
      (Quotient.lift L.homRel L ⋯).map a = L.map f
⊢ ∃ (a : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) X) (Quotient.mk (r := L.homRel) Y)),
    (Quotient.lift L.homRel L ⋯).map a = f

Tactic:
obtain ⟨f, rfl⟩ := L.map_surjective f

Premises used: rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.Full
X Y : C
f : X ⟶ Y
⊢ ∃ (a : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) X) (Quotient.mk (r := L.homRel) Y)),
    (Quotient.lift L.homRel L ⋯).map a = L.map f

Tactic:
⟨(Quotient.functor _).map f, rfl⟩

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Functor.map, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.Full
X Y : C
f : X ⟶ Y
⊢ ∃ (a : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) X) (Quotient.mk (r := L.homRel) Y)),
    (Quotient.lift L.homRel L ⋯).map a = L.map f

Tactic:
exact ⟨(Quotient.functor _).map f, rfl⟩
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
as as_1 : C
a₁ : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) as) (Quotient.mk (r := L.homRel) as_1)
a :
  Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as) ⟶
    Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as_1)
a₂ : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) as) (Quotient.mk (r := L.homRel) as_1)
a_1 :
  Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as) ⟶
    Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as_1)
h :
  (Quotient.lift L.homRel L ⋯).map (Quot.mk (HomRel.CompClosure L.homRel) a) =
    (Quotient.lift L.homRel L ⋯).map (Quot.mk (HomRel.CompClosure L.homRel) a_1)
⊢ Eq (α := Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) as) (Quotient.mk (r := L.homRel) as_1))
    (Quot.mk (HomRel.CompClosure L.homRel) a) (Quot.mk (HomRel.CompClosure L.homRel) a_1)

Tactic:
Quotient.sound _ h

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
as as_1 : C
a₁ : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) as) (Quotient.mk (r := L.homRel) as_1)
a :
  Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as) ⟶
    Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as_1)
a₂ : Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) as) (Quotient.mk (r := L.homRel) as_1)
a_1 :
  Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as) ⟶
    Quotient.as (r := L.homRel) (Quotient.mk (r := L.homRel) as_1)
h :
  (Quotient.lift L.homRel L ⋯).map (Quot.mk (HomRel.CompClosure L.homRel) a) =
    (Quotient.lift L.homRel L ⋯).map (Quot.mk (HomRel.CompClosure L.homRel) a_1)
⊢ Eq (α := Quiver.Hom (V := Quotient L.homRel) (Quotient.mk (r := L.homRel) as) (Quotient.mk (r := L.homRel) as_1))
    (Quot.mk (HomRel.CompClosure L.homRel) a) (Quot.mk (HomRel.CompClosure L.homRel) a_1)

Tactic:
exact Quotient.sound _ h

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.EssSurj
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.Full
inst_3 : L.EssSurj
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst_2 : HasPullback f g
inst_3 : IsRegularEpi f
apply : MorphismProperty.regularEpi C f
⊢ IsRegularEpi (X := pullback f g) (pullback.snd f g)

Tactic:
apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback (IsPullback.of_hasPullback f g)

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst_2 : HasPullback f g
inst_3 : IsRegularEpi f
⊢ IsRegularEpi f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst_2 : HasPullback f g
inst_3 : IsRegularEpi g
apply : MorphismProperty.regularEpi C g
⊢ IsRegularEpi (X := pullback f g) (pullback.fst f g)

Tactic:
apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback (IsPullback.of_hasPullback f g).flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst_2 : HasPullback f g
inst_3 : IsRegularEpi g
⊢ IsRegularEpi g

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
⊢ HasCoequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)

Tactic:
Regular.hasCoequalizer_of_isKernelPair <| IsKernelPair.of_hasPullback f

Premises used: CategoryTheory.IsKernelPair.of_hasPullback, CategoryTheory.Regular.hasCoequalizer_of_isKernelPair
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
apply :
  Eq (α :=
    pullback (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Y :=
        coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f ⋯)
        (coequalizer.desc f ⋯) ⟶
      coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f))
    (pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
    (pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯))
⊢ Mono (X := coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (coequalizer.desc f ⋯)

Tactic:
apply (IsKernelPair.of_hasPullback _).mono_of_eq_fst_snd

Premises used: CategoryTheory.IsKernelPair.mono_of_eq_fst_snd, CategoryTheory.IsKernelPair.of_hasPullback
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
⊢ Eq (α := pullback f f ⟶ Y) ((pullback.fst f f ≫ e) ≫ m) ((pullback.snd f f ≫ e) ≫ m)

Tactic:
simp [m, e, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
⊢ pullback.fst f f ≫ e = d ≫ k₁

Tactic:
simp [d, k₁]
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
⊢ d ≫ k₂ = pullback.snd f f ≫ e

Tactic:
simp [d, k₂]
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ g₁ ≫ pullback.snd e k₁ = g₂ ≫ pullback.fst k₂ e

Tactic:
simp [g₁, g₂]
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
refine : IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)
⊢ IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)

Tactic:
refine .of_right ?_ (by simp [g₁, g₂]) (.of_hasPullback e k₁)
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)

Tactic:
.of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))

Premises used: CategoryTheory.IsPullback.of_bot, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
refine_1 : IsPullback (g₁ ≫ pullback.fst e k₁) (g₂ ≫ pullback.snd k₂ e) (e ≫ m) (e ≫ m)
refine_2 : (g₁ ≫ pullback.fst e k₁) ≫ e = g₂ ≫ pullback.fst k₂ e ≫ k₁
⊢ IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)

Tactic:
refine .of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback (g₁ ≫ pullback.fst e k₁) (g₂ ≫ pullback.snd k₂ e) (e ≫ m) (e ≫ m)

Tactic:
simpa [g₁, g₂, e, m, pullback.lift_fst, pullback.lift_snd] using .of_hasPullback f f

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ (g₁ ≫ pullback.fst e k₁) ≫ e = g₂ ≫ pullback.fst k₂ e ≫ k₁

Tactic:
simp [g₁, g₂, k₁, d]
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)

Tactic:
have h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e) := by
    refine .of_right ?_ (by simp [g₁, g₂]) (.of_hasPullback e k₁)
    refine .of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))
    · simpa [g₁, g₂, e, m, pullback.lift_fst, pullback.lift_snd] using .of_hasPullback f f
    · simp [g₁, g₂, k₁, d]
-- Module: Mathlib.CategoryTheory.RegularCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Regular.{u, v} C
X Y : C
f : X ⟶ Y
m : coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) :=
  coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (X := pullback f f) (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
apply : MorphismProperty.regularEpi C (X := pullback k₂ e) (pullback.fst k₂ e)
⊢ IsRegularEpi g₁

Tactic:
apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback h.flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback