[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
⊢ ∀ (s : Fork g h),
    (fun s => limit.lift (parallelPair g h) s) s ≫
        Fork.ι (Fork.ofι (equalizer.ι g h) (_ : equalizer.ι g h ≫ g = equalizer.ι g h ≫ h)) =
      Fork.ι s
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (equalizer.ι g h) (_ : equalizer.ι g h ≫ g = equalizer.ι g h ≫ h)).pt
w : m ≫ Fork.ι (Fork.ofι (equalizer.ι g h) (_ : equalizer.ι g h ≫ g = equalizer.ι g h ≫ h)) = Fork.ι s
⊢ m = (fun s => limit.lift (parallelPair g h) s) s
[PROOFSTEP]
apply equalizer.hom_ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (equalizer.ι g h) (_ : equalizer.ι g h ≫ g = equalizer.ι g h ≫ h)).pt
w : m ≫ Fork.ι (Fork.ofι (equalizer.ι g h) (_ : equalizer.ι g h ≫ g = equalizer.ι g h ≫ h)) = Fork.ι s
⊢ m ≫ equalizer.ι g h = (fun s => limit.lift (parallelPair g h) s) s ≫ equalizer.ι g h
[PROOFSTEP]
simp [← w]
[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)
⊢ g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right
[PROOFSTEP]
repeat (rw [← Category.assoc, ← eq_whisker comm])
[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)
⊢ g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right
[PROOFSTEP]
rw [← Category.assoc, ← eq_whisker comm]
[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) ≫ RegularMono.left = g ≫ k ≫ RegularMono.right
[PROOFSTEP]
rw [← Category.assoc, ← eq_whisker comm]
[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) ≫ RegularMono.left = (f ≫ h) ≫ RegularMono.right
[PROOFSTEP]
rw [← Category.assoc, ← eq_whisker comm]
[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) ≫ RegularMono.left = (f ≫ h) ≫ RegularMono.right
[PROOFSTEP]
simp only [Category.assoc, hr.w]
[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)
⊢ IsLimit (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right))
[PROOFSTEP]
apply Fork.IsLimit.mk' _ _
[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 ≫ RegularMono.left) (k ≫ RegularMono.right)) →
    { l //
      l ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj
                    (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
                WalkingParallelPair.zero},
          m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = l }
[PROOFSTEP]
intro s
[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 ≫ RegularMono.left) (k ≫ RegularMono.right)
⊢ { l //
    l ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj
                  (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = l }
[PROOFSTEP]
have l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ hr.right
[GOAL]
case l₁
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
⊢ (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
⊢ { l //
    l ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj
                  (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = l }
[PROOFSTEP]
rw [Category.assoc, s.condition, Category.assoc]
[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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
⊢ { l //
    l ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj
                  (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = l }
[PROOFSTEP]
obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁
[GOAL]
case mk
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
⊢ { l //
    l ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj
                  (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = l }
[PROOFSTEP]
obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl
[GOAL]
case mk.mk.intro
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
⊢ { l //
    l ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj
                  (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = l }
[PROOFSTEP]
refine' ⟨p, hp₂, _⟩
[GOAL]
case mk.mk.intro
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj
              (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
          WalkingParallelPair.zero},
    m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s → m = p
[PROOFSTEP]
intro m w
[GOAL]
case mk.mk.intro
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj
          (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
      WalkingParallelPair.zero
w : m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s
⊢ m = p
[PROOFSTEP]
have z : m ≫ g = p ≫ g := w.trans hp₂.symm
[GOAL]
case mk.mk.intro
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj
          (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
      WalkingParallelPair.zero
w : m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s
z : m ≫ g = p ≫ g
⊢ m = p
[PROOFSTEP]
apply t.hom_ext
[GOAL]
case mk.mk.intro
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj
          (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
      WalkingParallelPair.zero
w : m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s
z : m ≫ g = p ≫ g
⊢ ∀ (j : WalkingCospan),
    m ≫ NatTrans.app (PullbackCone.mk f g comm).π j = p ≫ NatTrans.app (PullbackCone.mk f g comm).π j
[PROOFSTEP]
apply (PullbackCone.mk f g comm).equalizer_ext
[GOAL]
case mk.mk.intro.h₀
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj
          (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
      WalkingParallelPair.zero
w : m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s
z : m ≫ g = p ≫ g
⊢ m ≫ PullbackCone.fst (PullbackCone.mk f g comm) = p ≫ PullbackCone.fst (PullbackCone.mk f g comm)
[PROOFSTEP]
erw [← cancel_mono h, Category.assoc, Category.assoc, comm]
[GOAL]
case mk.mk.intro.h₀
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj
          (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
      WalkingParallelPair.zero
w : m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s
z : m ≫ g = p ≫ g
⊢ m ≫ g ≫ k = p ≫ g ≫ k
[PROOFSTEP]
simp only [← Category.assoc, eq_whisker z]
[GOAL]
case mk.mk.intro.h₁
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 ≫ RegularMono.left) (k ≫ RegularMono.right)
l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ RegularMono.right
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)).pt
hl : l ≫ Fork.ι (Fork.ofι h (_ : h ≫ RegularMono.left = h ≫ RegularMono.right)) = Fork.ι s ≫ k
p : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ PullbackCone.fst (PullbackCone.mk f g comm) = l
hp₂ : p ≫ PullbackCone.snd (PullbackCone.mk f g comm) = Fork.ι s
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj
          (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)).pt).obj
      WalkingParallelPair.zero
w : m ≫ Fork.ι (Fork.ofι g (_ : g ≫ k ≫ RegularMono.left = g ≫ k ≫ RegularMono.right)) = Fork.ι s
z : m ≫ g = p ≫ g
⊢ m ≫ PullbackCone.snd (PullbackCone.mk f g comm) = p ≫ PullbackCone.snd (PullbackCone.mk f g comm)
[PROOFSTEP]
exact z
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
⊢ ∀ (X_1 Y_1 : C) (z : X_1 ⟶ Y_1), Epi z → ∀ (u : X_1 ⟶ X) (v : Y_1 ⟶ Y) (sq : CommSq u z f v), CommSq.HasLift sq
[PROOFSTEP]
intro A B z hz u v sq
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ CommSq.HasLift sq
[PROOFSTEP]
have : v ≫ (RegularMono.left : Y ⟶ RegularMono.Z f) = v ≫ RegularMono.right :=
  by
  apply (cancel_epi z).1
  repeat (rw [← Category.assoc, ← eq_whisker sq.w])
  simp only [Category.assoc, RegularMono.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ v ≫ RegularMono.left = v ≫ RegularMono.right
[PROOFSTEP]
apply (cancel_epi z).1
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ RegularMono.left = z ≫ v ≫ RegularMono.right
[PROOFSTEP]
repeat (rw [← Category.assoc, ← eq_whisker sq.w])
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ RegularMono.left = z ≫ v ≫ RegularMono.right
[PROOFSTEP]
rw [← Category.assoc, ← eq_whisker sq.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ RegularMono.left = z ≫ v ≫ RegularMono.right
[PROOFSTEP]
rw [← Category.assoc, ← eq_whisker sq.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ RegularMono.left = (u ≫ f) ≫ RegularMono.right
[PROOFSTEP]
rw [← Category.assoc, ← eq_whisker sq.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ RegularMono.left = (u ≫ f) ≫ RegularMono.right
[PROOFSTEP]
simp only [Category.assoc, RegularMono.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ RegularMono.left = v ≫ RegularMono.right
⊢ CommSq.HasLift sq
[PROOFSTEP]
obtain ⟨t, ht⟩ := RegularMono.lift' _ _ this
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ RegularMono.left = v ≫ RegularMono.right
t : B ⟶ X
ht : t ≫ f = v
⊢ CommSq.HasLift sq
[PROOFSTEP]
refine' CommSq.HasLift.mk' ⟨t, (cancel_mono f).1 _, ht⟩
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularMono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ RegularMono.left = v ≫ RegularMono.right
t : B ⟶ X
ht : t ≫ f = v
⊢ (z ≫ t) ≫ f = u ≫ f
[PROOFSTEP]
simp only [Arrow.mk_hom, Arrow.homMk'_left, Category.assoc, ht, sq.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : SplitMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ RegularMono f
[PROOFSTEP]
haveI := isSplitMono_of_mono f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : SplitMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
this : IsSplitMono f
⊢ RegularMono f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : RegularMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ StrongMono f
[PROOFSTEP]
haveI := regularMonoOfMono f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : RegularMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
this : RegularMono f
⊢ StrongMono f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasColimit (parallelPair g h)
⊢ ∀ (s : Cofork g h),
    Cofork.π (Cofork.ofπ (coequalizer.π g h) (_ : g ≫ coequalizer.π g h = h ≫ coequalizer.π g h)) ≫
        (fun s => colimit.desc (parallelPair g h) s) s =
      Cofork.π s
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasColimit (parallelPair g h)
s : Cofork g h
m : (Cofork.ofπ (coequalizer.π g h) (_ : g ≫ coequalizer.π g h = h ≫ coequalizer.π g h)).pt ⟶ s.pt
w : Cofork.π (Cofork.ofπ (coequalizer.π g h) (_ : g ≫ coequalizer.π g h = h ≫ coequalizer.π g h)) ≫ m = Cofork.π s
⊢ m = (fun s => colimit.desc (parallelPair g h) s) s
[PROOFSTEP]
apply coequalizer.hom_ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasColimit (parallelPair g h)
s : Cofork g h
m : (Cofork.ofπ (coequalizer.π g h) (_ : g ≫ coequalizer.π g h = h ≫ coequalizer.π g h)).pt ⟶ s.pt
w : Cofork.π (Cofork.ofπ (coequalizer.π g h) (_ : g ≫ coequalizer.π g h = h ≫ coequalizer.π g h)) ≫ m = Cofork.π s
⊢ coequalizer.π g h ≫ m = coequalizer.π g h ≫ (fun s => colimit.desc (parallelPair g h) s) s
[PROOFSTEP]
simp [← w]
[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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h
[PROOFSTEP]
rw [Category.assoc, Category.assoc, comm]
[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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ RegularEpi.left ≫ g ≫ k = RegularEpi.right ≫ g ≫ k
[PROOFSTEP]
simp only [← Category.assoc, eq_whisker gr.w]
[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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h))
[PROOFSTEP]
apply Cofork.IsColimit.mk' _ _
[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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)) →
    { l //
      Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ l = Cofork.π s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj
                    (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
                WalkingParallelPair.one ⟶
              ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
          Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s →
            m = l }
[PROOFSTEP]
intro s
[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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
⊢ { l //
    Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
[GOAL]
case l₁
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
⊢ RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
⊢ { l //
    Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, s.condition]
[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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
⊢ { l //
    Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' gr.isColimit (f ≫ Cofork.π s) l₁
[GOAL]
case mk
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
⊢ { l //
    Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.symm
[GOAL]
case mk.mk.intro
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
⊢ { l //
    Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
refine' ⟨p, hp₁, _⟩
[GOAL]
case mk.mk.intro
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj
              (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
          WalkingParallelPair.one ⟶
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
    Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s → m = p
[PROOFSTEP]
intro m w
[GOAL]
case mk.mk.intro
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
⊢ m = p
[PROOFSTEP]
have z := w.trans hp₁.symm
[GOAL]
case mk.mk.intro
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z :
  Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m =
    PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
⊢ m = p
[PROOFSTEP]
apply t.hom_ext
[GOAL]
case mk.mk.intro
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z :
  Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m =
    PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
⊢ ∀ (j : WalkingSpan),
    NatTrans.app (PushoutCocone.mk h k comm).ι j ≫ m = NatTrans.app (PushoutCocone.mk h k comm).ι j ≫ p
[PROOFSTEP]
apply (PushoutCocone.mk _ _ comm).coequalizer_ext
[GOAL]
case mk.mk.intro.h₀
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z :
  Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m =
    PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
⊢ PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ m = PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
[PROOFSTEP]
exact z
[GOAL]
case mk.mk.intro.h₁
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z :
  Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m =
    PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
⊢ PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ m = PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p
[PROOFSTEP]
erw [← cancel_epi g, ← Category.assoc, ← eq_whisker comm]
[GOAL]
case mk.mk.intro.h₁
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z :
  Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m =
    PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
⊢ (f ≫ h) ≫ m = g ≫ PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p
[PROOFSTEP]
erw [← Category.assoc, ← eq_whisker comm]
[GOAL]
case mk.mk.intro.h₁
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z :
  Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m =
    PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p
[PROOFSTEP]
dsimp at z 
[GOAL]
case mk.mk.intro.h₁
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (RegularEpi.left ≫ f) (RegularEpi.right ≫ f)
l₁ : RegularEpi.left ≫ f ≫ Cofork.π s = RegularEpi.right ≫ f ≫ Cofork.π s
l :
  (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)).pt ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hl : Cofork.π (Cofork.ofπ g (_ : RegularEpi.left ≫ g = RegularEpi.right ≫ g)) ≫ l = f ≫ Cofork.π s
p : (PushoutCocone.mk h k comm).pt ⟶ ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hp₁ : PushoutCocone.inl (PushoutCocone.mk h k comm) ≫ p = Cofork.π s
right✝ : PushoutCocone.inr (PushoutCocone.mk h k comm) ≫ p = l
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
w : Cofork.π (Cofork.ofπ h (_ : (RegularEpi.left ≫ f) ≫ h = (RegularEpi.right ≫ f) ≫ h)) ≫ m = Cofork.π s
z : h ≫ m = h ≫ p
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p
[PROOFSTEP]
simp only [Category.assoc, z]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
⊢ ∀ (X_1 Y_1 : C) (z : X_1 ⟶ Y_1), Mono z → ∀ (u : X ⟶ X_1) (v : Y ⟶ Y_1) (sq : CommSq u f z v), CommSq.HasLift sq
[PROOFSTEP]
intro A B z hz u v sq
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
⊢ CommSq.HasLift sq
[PROOFSTEP]
have : (RegularEpi.left : RegularEpi.W f ⟶ X) ≫ u = RegularEpi.right ≫ u :=
  by
  apply (cancel_mono z).1
  simp only [Category.assoc, sq.w, RegularEpi.w_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
⊢ RegularEpi.left ≫ u = RegularEpi.right ≫ u
[PROOFSTEP]
apply (cancel_mono z).1
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
⊢ (RegularEpi.left ≫ u) ≫ z = (RegularEpi.right ≫ u) ≫ z
[PROOFSTEP]
simp only [Category.assoc, sq.w, RegularEpi.w_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
this : RegularEpi.left ≫ u = RegularEpi.right ≫ u
⊢ CommSq.HasLift sq
[PROOFSTEP]
obtain ⟨t, ht⟩ := RegularEpi.desc' f u this
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
this : RegularEpi.left ≫ u = RegularEpi.right ≫ u
t : Y ⟶ A
ht : f ≫ t = u
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact
  CommSq.HasLift.mk'
    ⟨t, ht, (cancel_epi f).1 (by simp only [← Category.assoc, ht, ← sq.w, Arrow.mk_hom, Arrow.homMk'_right])⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : RegularEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
this : RegularEpi.left ≫ u = RegularEpi.right ≫ u
t : Y ⟶ A
ht : f ≫ t = u
⊢ f ≫ t ≫ z = f ≫ v
[PROOFSTEP]
simp only [← Category.assoc, ht, ← sq.w, Arrow.mk_hom, Arrow.homMk'_right]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : SplitEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ RegularEpi f
[PROOFSTEP]
haveI := isSplitEpi_of_epi f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : SplitEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
this : IsSplitEpi f
⊢ RegularEpi f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : RegularEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ StrongEpi f
[PROOFSTEP]
haveI := regularEpiOfEpi f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : RegularEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
this : RegularEpi f
⊢ StrongEpi f
[PROOFSTEP]
infer_instance
