[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


[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
⊢ f.left ≫ NatTrans.app ((fun c => { pt := c.left, π := c.hom }) Y✝).π j =
    NatTrans.app ((fun c => { pt := c.left, π := c.hom }) X✝).π j
[PROOFSTEP]
convert congr_fun (congr_arg NatTrans.app f.w) j
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (((fun c => { pt := c.left, π := c.hom }) X✝).pt ⟶ F.obj j) =
    (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)
e_6✝ : F = (fromPUnit F).obj Y✝.right
⊢ ((fun c => { pt := c.left, π := c.hom }) X✝).π = X✝.hom ≫ (fromPUnit F).map f.right
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (((fun c => { pt := c.left, π := c.hom }) X✝).pt ⟶ F.obj j) =
    (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)
e_6✝ : F = (fromPUnit F).obj Y✝.right
⊢ X✝.hom = X✝.hom ≫ 𝟙 F
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ Function.LeftInverse
    (fun h s => { toInhabited := { default := IsTerminal.from h s }, uniq := (_ : ∀ (a : s ⟶ c), a = default) })
    fun h => IsTerminal.ofUnique c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ Function.RightInverse
    (fun h s => { toInhabited := { default := IsTerminal.from h s }, uniq := (_ : ∀ (a : s ⟶ c), a = default) })
    fun h => IsTerminal.ofUnique c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
⊢ NatTrans.app ((fun c => { pt := c.right, ι := c.hom }) X✝).ι j ≫ f.right =
    NatTrans.app ((fun c => { pt := c.right, ι := c.hom }) Y✝).ι j
[PROOFSTEP]
convert (congr_fun (congr_arg NatTrans.app f.w) j).symm
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (F.obj j ⟶ ((fun c => { pt := c.right, ι := c.hom }) Y✝).pt) =
    (((fromPUnit F).obj X✝.left).obj j ⟶ ((const J).obj Y✝.right).obj j)
e_5✝ : F = (fromPUnit F).obj X✝.left
⊢ ((fun c => { pt := c.right, ι := c.hom }) Y✝).ι = (fromPUnit F).map f.left ≫ Y✝.hom
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h.h.e'_7.h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
e_1✝ :
  (F.obj j ⟶ ((fun c => { pt := c.right, ι := c.hom }) Y✝).pt) =
    (((fromPUnit F).obj X✝.left).obj j ⟶ ((const J).obj Y✝.right).obj j)
e_5✝ : F = (fromPUnit F).obj X✝.left
⊢ Y✝.hom = 𝟙 F ≫ Y✝.hom
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ Function.LeftInverse
    (fun h s => { toInhabited := { default := IsInitial.to h s }, uniq := (_ : ∀ (a : c ⟶ s), a = default) }) fun h =>
    IsInitial.ofUnique c
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ Function.RightInverse
    (fun h s => { toInhabited := { default := IsInitial.to h s }, uniq := (_ : ∀ (a : c ⟶ s), a = default) }) fun h =>
    IsInitial.ofUnique c
[PROOFSTEP]
aesop_cat


[GOAL]
β : Type v
f : β → Type v
P : Type v
s : (b : β) → P ⟶ f b
b : β
x : P
⊢ Pi.π f b (Pi.lift s x) = s b x
[PROOFSTEP]
simp
[GOAL]
β : Type v
f g : β → Type v
α : (j : β) → f j ⟶ g j
b : β
x : ∏ fun b => f b
⊢ Pi.π g b (Pi.map α x) = α b (Pi.π f b x)
[PROOFSTEP]
simp
[GOAL]
x✝ : Cone (Functor.empty (Type u))
⊢ ∀ (j : Discrete PEmpty),
    (fun x x => PUnit.unit) x✝ ≫
        NatTrans.app { pt := PUnit, π := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PUnit)).hom }.π
          j =
      NatTrans.app x✝.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
x✝² : Cone (Functor.empty (Type u))
x✝¹ : x✝².pt ⟶ { pt := PUnit, π := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PUnit)).hom }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    x✝¹ ≫
        NatTrans.app { pt := PUnit, π := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PUnit)).hom }.π
          j =
      NatTrans.app x✝².π j
⊢ x✝¹ = (fun x x => PUnit.unit) x✝²
[PROOFSTEP]
funext
[GOAL]
case h
x✝³ : Cone (Functor.empty (Type u))
x✝² : x✝³.pt ⟶ { pt := PUnit, π := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PUnit)).hom }.pt
x✝¹ :
  ∀ (j : Discrete PEmpty),
    x✝² ≫
        NatTrans.app { pt := PUnit, π := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PUnit)).hom }.π
          j =
      NatTrans.app x✝³.π j
x✝ : x✝³.pt
⊢ x✝² x✝ = (fun x x => PUnit.unit) x✝³ x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
X : Type u
⊢ IsTerminal X ≃ (X ≅ PUnit)
[PROOFSTEP]
calc
  IsTerminal X ≃ Unique X := isTerminalEquivUnique _
  _ ≃ (X ≃ PUnit.{u + 1}) := (uniqueEquivEquivUnique _ _)
  _ ≃ (X ≅ PUnit) := equivEquivIso
[GOAL]
x✝ : Cocone (Functor.empty (Type u))
⊢ { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.pt ⟶ x✝.pt
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
x✝ : Cocone (Functor.empty (Type u))
⊢ ∀ (j : Discrete PEmpty),
    NatTrans.app { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.ι
          j ≫
        (fun x a => PEmpty.casesOn (fun x_1 => x.pt) a) x✝ =
      NatTrans.app x✝.ι j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
x✝² : Cocone (Functor.empty (Type u))
x✝¹ : { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.pt ⟶ x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.ι
          j ≫
        x✝¹ =
      NatTrans.app x✝².ι j
⊢ x✝¹ = (fun x a => PEmpty.casesOn (fun x_1 => x.pt) a) x✝²
[PROOFSTEP]
funext x
[GOAL]
case h
x✝² : Cocone (Functor.empty (Type u))
x✝¹ : { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.pt ⟶ x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty),
    NatTrans.app { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.ι
          j ≫
        x✝¹ =
      NatTrans.app x✝².ι j
x : { pt := PEmpty, ι := (Functor.uniqueFromEmpty ((Functor.const (Discrete PEmpty)).obj PEmpty)).inv }.pt
⊢ x✝¹ x = (fun x a => PEmpty.casesOn (fun x_1 => x.pt) a) x✝² x
[PROOFSTEP]
cases x
[GOAL]
⊢ binaryProductFunctor ≅ prod.functor
[PROOFSTEP]
refine' NatIso.ofComponents (fun X => _) (fun _ => _)
[GOAL]
case refine'_1
X : Type u
⊢ binaryProductFunctor.obj X ≅ prod.functor.obj X
[PROOFSTEP]
refine' NatIso.ofComponents (fun Y => _) (fun _ => _)
[GOAL]
case refine'_1.refine'_1
X Y : Type u
⊢ (binaryProductFunctor.obj X).obj Y ≅ (prod.functor.obj X).obj Y
[PROOFSTEP]
exact ((limit.isLimit _).conePointUniqueUpToIso (binaryProductLimit X Y)).symm
[GOAL]
case refine'_1.refine'_2
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫
      ((fun Y => (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm) Y✝).hom =
    ((fun Y => (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm) X✝).hom ≫
      (prod.functor.obj X).map x✝
[PROOFSTEP]
apply Limits.prod.hom_ext
[GOAL]
case refine'_1.refine'_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((fun Y => (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm) Y✝).hom) ≫
      prod.fst =
    (((fun Y => (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm) X✝).hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.fst
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2.h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((fun Y => (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm) Y✝).hom) ≫
      prod.snd =
    (((fun Y => (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm) X✝).hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.snd
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫ _root_.Prod.fst = _root_.Prod.fst
[PROOFSTEP]
rfl
[GOAL]
case refine'_1.refine'_2.h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫ _root_.Prod.snd = _root_.Prod.snd ≫ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ binaryProductFunctor.map x✝ ≫
      ((fun X =>
            NatIso.ofComponents fun Y =>
              (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
          Y✝).hom =
    ((fun X =>
            NatIso.ofComponents fun Y =>
              (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
          X✝).hom ≫
      prod.functor.map x✝
[PROOFSTEP]
ext : 2
[GOAL]
case refine'_2.w.h
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ NatTrans.app
      (binaryProductFunctor.map x✝¹ ≫
        ((fun X =>
              NatIso.ofComponents fun Y =>
                (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
            Y✝).hom)
      x✝ =
    NatTrans.app
      (((fun X =>
              NatIso.ofComponents fun Y =>
                (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
            X✝).hom ≫
        prod.functor.map x✝¹)
      x✝
[PROOFSTEP]
apply Limits.prod.hom_ext
[GOAL]
case refine'_2.w.h.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ NatTrans.app
        (binaryProductFunctor.map x✝¹ ≫
          ((fun X =>
                NatIso.ofComponents fun Y =>
                  (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
              Y✝).hom)
        x✝ ≫
      prod.fst =
    NatTrans.app
        (((fun X =>
                NatIso.ofComponents fun Y =>
                  (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
              X✝).hom ≫
          prod.functor.map x✝¹)
        x✝ ≫
      prod.fst
[PROOFSTEP]
simp
[GOAL]
case refine'_2.w.h.h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ NatTrans.app
        (binaryProductFunctor.map x✝¹ ≫
          ((fun X =>
                NatIso.ofComponents fun Y =>
                  (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
              Y✝).hom)
        x✝ ≫
      prod.snd =
    NatTrans.app
        (((fun X =>
                NatIso.ofComponents fun Y =>
                  (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)).symm)
              X✝).hom ≫
          prod.functor.map x✝¹)
        x✝ ≫
      prod.snd
[PROOFSTEP]
simp
[GOAL]
case refine'_2.w.h.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ NatTrans.app (binaryProductFunctor.map x✝¹) x✝ ≫ _root_.Prod.fst = _root_.Prod.fst ≫ x✝¹
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.w.h.h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ NatTrans.app (binaryProductFunctor.map x✝¹) x✝ ≫ _root_.Prod.snd = _root_.Prod.snd
[PROOFSTEP]
rfl
[GOAL]
X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    Injective (BinaryCofan.inl c) ∧
      Injective (BinaryCofan.inr c) ∧ IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
[PROOFSTEP]
classical
constructor
· rintro ⟨h⟩
  rw [← show _ = c.inl from h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩, ←
    show _ = c.inr from h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]
  dsimp [binaryCoproductCocone]
  refine'
    ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp Sum.inl_injective,
      (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp Sum.inr_injective, _⟩
  erw [Set.range_comp, ← eq_compl_iff_isCompl, Set.range_comp _ Sum.inr, ←
    Set.image_compl_eq (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
  simp
· rintro ⟨h₁, h₂, h₃⟩
  have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr :=
    by
    rw [eq_compl_iff_isCompl.mpr h₃.symm]
    exact fun _ => or_not
  refine' ⟨BinaryCofan.IsColimit.mk _ _ _ _ _⟩
  · intro T f g x
    exact
      if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
      else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)
  · intro T f g
    funext x
    dsimp
    simp [h₁.eq_iff]
  · intro T f g
    funext x
    dsimp
    simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff, forall_exists_index]
    intro y e
    have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
    rw [disjoint_iff.mp h₃.1] at this
    exact this.elim
  · rintro T _ _ m rfl rfl
    funext x
    dsimp
    split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
[GOAL]
X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    Injective (BinaryCofan.inl c) ∧
      Injective (BinaryCofan.inr c) ∧ IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    Injective (BinaryCofan.inl c) ∧
      Injective (BinaryCofan.inr c) ∧ IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective (BinaryCofan.inl c) ∧
    Injective (BinaryCofan.inr c) ∧ IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
[PROOFSTEP]
rw [← show _ = c.inl from h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩, ←
  show _ = c.inr from h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]
[GOAL]
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      (NatTrans.app (binaryCoproductCocone X Y).ι { as := left } ≫
        (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
    Injective
        (NatTrans.app (binaryCoproductCocone X Y).ι { as := right } ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
      IsCompl
        (Set.range
          (NatTrans.app (binaryCoproductCocone X Y).ι { as := left } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
        (Set.range
          (NatTrans.app (binaryCoproductCocone X Y).ι { as := right } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
[PROOFSTEP]
dsimp [binaryCoproductCocone]
[GOAL]
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective (Sum.inl ≫ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
    Injective (Sum.inr ≫ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
      IsCompl (Set.range (Sum.inl ≫ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
        (Set.range (Sum.inr ≫ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
[PROOFSTEP]
refine'
  ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp Sum.inl_injective,
    (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp Sum.inr_injective, _⟩
[GOAL]
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl (Set.range (Sum.inl ≫ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
    (Set.range (Sum.inr ≫ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
[PROOFSTEP]
erw [Set.range_comp, ← eq_compl_iff_isCompl, Set.range_comp _ Sum.inr, ←
  Set.image_compl_eq (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
[GOAL]
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv '' Set.range Sum.inl =
    ↑(IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).symm.toEquiv '' (Set.range Sum.inr)ᶜ
[PROOFSTEP]
simp
[GOAL]
case mpr
X Y : Type u
c : BinaryCofan X Y
⊢ Injective (BinaryCofan.inl c) ∧
      Injective (BinaryCofan.inr c) ∧ IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c)) →
    Nonempty (IsColimit c)
[PROOFSTEP]
rintro ⟨h₁, h₂, h₃⟩
[GOAL]
case mpr.intro.intro
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
⊢ Nonempty (IsColimit c)
[PROOFSTEP]
have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr :=
  by
  rw [eq_compl_iff_isCompl.mpr h₃.symm]
  exact fun _ => or_not
[GOAL]
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
⊢ ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
[PROOFSTEP]
rw [eq_compl_iff_isCompl.mpr h₃.symm]
[GOAL]
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
⊢ ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ (Set.range (BinaryCofan.inl c))ᶜ
[PROOFSTEP]
exact fun _ => or_not
[GOAL]
case mpr.intro.intro
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
⊢ Nonempty (IsColimit c)
[PROOFSTEP]
refine' ⟨BinaryCofan.IsColimit.mk _ _ _ _ _⟩
[GOAL]
case mpr.intro.intro.refine'_1
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
⊢ {T : Type u} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)
[PROOFSTEP]
intro T f g x
[GOAL]
case mpr.intro.intro.refine'_1
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : c.pt
⊢ T
[PROOFSTEP]
exact
  if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
  else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)
[GOAL]
case mpr.intro.intro.refine'_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (BinaryCofan.inl c ≫ fun x =>
        if h : x ∈ Set.range (BinaryCofan.inl c) then
          f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
        else
          g
            (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
              { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })) =
      f
[PROOFSTEP]
intro T f g
[GOAL]
case mpr.intro.intro.refine'_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inl c ≫ fun x =>
      if h : x ∈ Set.range (BinaryCofan.inl c) then
        f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
      else
        g
          (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
            { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })) =
    f
[PROOFSTEP]
funext x
[GOAL]
case mpr.intro.intro.refine'_2.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := left }
⊢ (BinaryCofan.inl c ≫ fun x =>
        if h : x ∈ Set.range (BinaryCofan.inl c) then
          f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
        else
          g
            (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
              { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) }))
      x =
    f x
[PROOFSTEP]
dsimp
[GOAL]
case mpr.intro.intro.refine'_2.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := left }
⊢ (if h : BinaryCofan.inl c x ∈ Set.range (BinaryCofan.inl c) then
      f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := BinaryCofan.inl c x, property := h })
    else
      g
        (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
          { val := BinaryCofan.inl c x, property := (_ : BinaryCofan.inl c x ∈ Set.range (BinaryCofan.inr c)) })) =
    f x
[PROOFSTEP]
simp [h₁.eq_iff]
[GOAL]
case mpr.intro.intro.refine'_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (BinaryCofan.inr c ≫ fun x =>
        if h : x ∈ Set.range (BinaryCofan.inl c) then
          f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
        else
          g
            (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
              { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })) =
      g
[PROOFSTEP]
intro T f g
[GOAL]
case mpr.intro.intro.refine'_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
⊢ (BinaryCofan.inr c ≫ fun x =>
      if h : x ∈ Set.range (BinaryCofan.inl c) then
        f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
      else
        g
          (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
            { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })) =
    g
[PROOFSTEP]
funext x
[GOAL]
case mpr.intro.intro.refine'_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
⊢ (BinaryCofan.inr c ≫ fun x =>
        if h : x ∈ Set.range (BinaryCofan.inl c) then
          f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
        else
          g
            (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
              { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) }))
      x =
    g x
[PROOFSTEP]
dsimp
[GOAL]
case mpr.intro.intro.refine'_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
⊢ (if h : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inl c) then
      f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := BinaryCofan.inr c x, property := h })
    else
      g
        (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
          { val := BinaryCofan.inr c x, property := (_ : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inr c)) })) =
    g x
[PROOFSTEP]
simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff, forall_exists_index]
[GOAL]
case mpr.intro.intro.refine'_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
⊢ ∀ (x_1 : X) (h : BinaryCofan.inl c x_1 = BinaryCofan.inr c x),
    f
        (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm
          { val := BinaryCofan.inr c x, property := (_ : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inl c)) }) =
      g x
[PROOFSTEP]
intro y e
[GOAL]
case mpr.intro.intro.refine'_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : BinaryCofan.inl c y = BinaryCofan.inr c x
⊢ f
      (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm
        { val := BinaryCofan.inr c x, property := (_ : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inl c)) }) =
    g x
[PROOFSTEP]
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
[GOAL]
case mpr.intro.intro.refine'_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this✝ :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : BinaryCofan.inl c y = BinaryCofan.inr c x
this : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inl c) ⊓ Set.range (BinaryCofan.inr c)
⊢ f
      (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm
        { val := BinaryCofan.inr c x, property := (_ : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inl c)) }) =
    g x
[PROOFSTEP]
rw [disjoint_iff.mp h₃.1] at this
[GOAL]
case mpr.intro.intro.refine'_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this✝ :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : BinaryCofan.inl c y = BinaryCofan.inr c x
this : BinaryCofan.inr c x ∈ ⊥
⊢ f
      (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm
        { val := BinaryCofan.inr c x, property := (_ : BinaryCofan.inr c x ∈ Set.range (BinaryCofan.inl c)) }) =
    g x
[PROOFSTEP]
exact this.elim
[GOAL]
case mpr.intro.intro.refine'_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T),
    BinaryCofan.inl c ≫ m = f →
      BinaryCofan.inr c ≫ m = g →
        m = fun x =>
          if h : x ∈ Set.range (BinaryCofan.inl c) then
            f (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
          else
            g
              (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
                { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })
[PROOFSTEP]
rintro T _ _ m rfl rfl
[GOAL]
case mpr.intro.intro.refine'_4
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
m : c.pt ⟶ T
⊢ m = fun x =>
    if h : x ∈ Set.range (BinaryCofan.inl c) then
      (BinaryCofan.inl c ≫ m) (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
    else
      (BinaryCofan.inr c ≫ m)
        (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
          { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })
[PROOFSTEP]
funext x
[GOAL]
case mpr.intro.intro.refine'_4.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
m : c.pt ⟶ T
x : c.pt
⊢ m x =
    if h : x ∈ Set.range (BinaryCofan.inl c) then
      (BinaryCofan.inl c ≫ m) (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h })
    else
      (BinaryCofan.inr c ≫ m)
        (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
          { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) })
[PROOFSTEP]
dsimp
[GOAL]
case mpr.intro.intro.refine'_4.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
m : c.pt ⟶ T
x : c.pt
⊢ m x =
    if h : x ∈ Set.range (BinaryCofan.inl c) then
      m (BinaryCofan.inl c (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h }))
    else
      m
        (BinaryCofan.inr c
          (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
            { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) }))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : x ∈ Set.range (BinaryCofan.inl c)
⊢ m x = m (BinaryCofan.inl c (↑(Equiv.ofInjective (BinaryCofan.inl c) h₁).symm { val := x, property := h✝ }))
[PROOFSTEP]
exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
[GOAL]
case neg
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective (BinaryCofan.inl c)
h₂ : Injective (BinaryCofan.inr c)
h₃ : IsCompl (Set.range (BinaryCofan.inl c)) (Set.range (BinaryCofan.inr c))
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range (BinaryCofan.inl c) ∨ x ∈ Set.range (BinaryCofan.inr c)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ¬x ∈ Set.range (BinaryCofan.inl c)
⊢ m x =
    m
      (BinaryCofan.inr c
        (↑(Equiv.ofInjective (BinaryCofan.inr c) h₂).symm
          { val := x, property := (_ : x ∈ Set.range (BinaryCofan.inr c)) }))
[PROOFSTEP]
exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
[GOAL]
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsColimit (BinaryCofan.mk f Subtype.val)
[PROOFSTEP]
apply Nonempty.some
[GOAL]
case h
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Nonempty (IsColimit (BinaryCofan.mk f Subtype.val))
[PROOFSTEP]
rw [binaryCofan_isColimit_iff]
[GOAL]
case h
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Injective (BinaryCofan.inl (BinaryCofan.mk f Subtype.val)) ∧
    Injective (BinaryCofan.inr (BinaryCofan.mk f Subtype.val)) ∧
      IsCompl (Set.range (BinaryCofan.inl (BinaryCofan.mk f Subtype.val)))
        (Set.range (BinaryCofan.inr (BinaryCofan.mk f Subtype.val)))
[PROOFSTEP]
refine' ⟨(mono_iff_injective f).mp inferInstance, Subtype.val_injective, _⟩
[GOAL]
case h
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsCompl (Set.range (BinaryCofan.inl (BinaryCofan.mk f Subtype.val)))
    (Set.range (BinaryCofan.inr (BinaryCofan.mk f Subtype.val)))
[PROOFSTEP]
symm
[GOAL]
case h
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsCompl (Set.range (BinaryCofan.inr (BinaryCofan.mk f Subtype.val)))
    (Set.range (BinaryCofan.inl (BinaryCofan.mk f Subtype.val)))
[PROOFSTEP]
rw [← eq_compl_iff_isCompl]
[GOAL]
case h
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Set.range (BinaryCofan.inr (BinaryCofan.mk f Subtype.val)) =
    (Set.range (BinaryCofan.inl (BinaryCofan.mk f Subtype.val)))ᶜ
[PROOFSTEP]
exact Subtype.range_val
[GOAL]
J : Type v
F : J → Type u
inst✝ : UnivLE.{v, u}
s : Cone (Discrete.functor F)
m :
  s.pt ⟶
    { pt := Shrink ((j : J) → F j),
        π :=
          Discrete.natTrans fun x f =>
            match x, f with
            | { as := j }, f => ↑(equivShrink ((j : J) → F j)).symm f j }.pt
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          { pt := Shrink ((j : J) → F j),
              π :=
                Discrete.natTrans fun x f =>
                  match x, f with
                  | { as := j }, f => ↑(equivShrink ((j : J) → F j)).symm f j }.π
          j =
      NatTrans.app s.π j
x : s.pt
j : J
⊢ ↑(equivShrink ((j : J) → F j)).symm (m x) j =
    ↑(equivShrink ((j : J) → F j)).symm
      ((fun s x =>
          ↑(equivShrink ((j : J) → (Discrete.functor F).obj { as := j })) fun j => NatTrans.app s.π { as := j } x)
        s x)
      j
[PROOFSTEP]
simpa using (congr_fun (w ⟨j⟩) x : _)
[GOAL]
J : Type u
F : J → Type u
s : Cocone (Discrete.functor F)
m :
  { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun x x_1 =>
            match x, x_1 with
            | { as := j }, x => { fst := j, snd := x } }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    NatTrans.app
          { pt := (j : J) × F j,
              ι :=
                Discrete.natTrans fun x x_1 =>
                  match x, x_1 with
                  | { as := j }, x => { fst := j, snd := x } }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ m = (fun s x => NatTrans.app s.ι { as := x.fst } x.snd) s
[PROOFSTEP]
funext ⟨j, x⟩
[GOAL]
case h
J : Type u
F : J → Type u
s : Cocone (Discrete.functor F)
m :
  { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun x x_1 =>
            match x, x_1 with
            | { as := j }, x => { fst := j, snd := x } }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    NatTrans.app
          { pt := (j : J) × F j,
              ι :=
                Discrete.natTrans fun x x_1 =>
                  match x, x_1 with
                  | { as := j }, x => { fst := j, snd := x } }.ι
          j ≫
        m =
      NatTrans.app s.ι j
j : J
x : F j
⊢ m { fst := j, snd := x } = (fun s x => NatTrans.app s.ι { as := x.fst } x.snd) s { fst := j, snd := x }
[PROOFSTEP]
exact congr_fun (w ⟨j⟩) x
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
⊢ { l //
    l ≫ Fork.ι (Fork.ofι f w) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι f w).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι f w) = Fork.ι s → m = l }
[PROOFSTEP]
refine' ⟨fun i => _, _, _⟩
[GOAL]
case refine'_1
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
i : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ ((Functor.const WalkingParallelPair).obj (Fork.ofι f w).pt).obj WalkingParallelPair.zero
[PROOFSTEP]
apply Classical.choose (t (s.ι i) _)
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
i : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ g (Fork.ι s i) = h (Fork.ι s i)
[PROOFSTEP]
apply congr_fun s.condition i
[GOAL]
case refine'_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
⊢ (fun i => Classical.choose (_ : ∃! x, f x = Fork.ι s i)) ≫ Fork.ι (Fork.ofι f w) = Fork.ι s
[PROOFSTEP]
funext i
[GOAL]
case refine'_2.h
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
i : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ ((fun i => Classical.choose (_ : ∃! x, f x = Fork.ι s i)) ≫ Fork.ι (Fork.ofι f w)) i = Fork.ι s i
[PROOFSTEP]
exact (Classical.choose_spec (t (s.ι i) (congr_fun s.condition i))).1
[GOAL]
case refine'_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (Fork.ofι f w).pt).obj WalkingParallelPair.zero},
    m ≫ Fork.ι (Fork.ofι f w) = Fork.ι s → m = fun i => Classical.choose (_ : ∃! x, f x = Fork.ι s i)
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι f w).pt).obj WalkingParallelPair.zero
hm : m ≫ Fork.ι (Fork.ofι f w) = Fork.ι s
⊢ m = fun i => Classical.choose (_ : ∃! x, f x = Fork.ι s i)
[PROOFSTEP]
funext i
[GOAL]
case refine'_3.h
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), g y = h y → ∃! x, f x = y
s : Fork g h
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι f w).pt).obj WalkingParallelPair.zero
hm : m ≫ Fork.ι (Fork.ofι f w) = Fork.ι s
i : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ m i = Classical.choose (_ : ∃! x, f x = Fork.ι s i)
[PROOFSTEP]
exact (Classical.choose_spec (t (s.ι i) (congr_fun s.condition i))).2 _ (congr_fun hm i)
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
⊢ ∃! x, f x = y
[PROOFSTEP]
let y' : PUnit ⟶ Y := fun _ => y
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
⊢ ∃! x, f x = y
[PROOFSTEP]
have hy' : y' ≫ g = y' ≫ h := funext fun _ => hy
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
⊢ ∃! x, f x = y
[PROOFSTEP]
refine' ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_fun (Fork.IsLimit.lift' t y' _).2 ⟨⟩, _⟩
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
⊢ ∀ (y_1 : X), (fun x => f x = y) y_1 → y_1 = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
[PROOFSTEP]
intro x' hx'
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ x' = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
[PROOFSTEP]
suffices : (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
this : (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
⊢ x' = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
[PROOFSTEP]
rw [← this]
[GOAL]
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
[PROOFSTEP]
apply Fork.IsLimit.hom_ext t
[GOAL]
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') ≫ Fork.ι (Fork.ofι f w) = ↑(Fork.IsLimit.lift' t y' hy') ≫ Fork.ι (Fork.ofι f w)
[PROOFSTEP]
funext ⟨⟩
[GOAL]
case this.h
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ ((fun x => x') ≫ Fork.ι (Fork.ofι f w)) PUnit.unit =
    (↑(Fork.IsLimit.lift' t y' hy') ≫ Fork.ι (Fork.ofι f w)) PUnit.unit
[PROOFSTEP]
apply hx'.trans (congr_fun (Fork.IsLimit.lift' t _ hy').2 ⟨⟩).symm
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
i : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ g (Fork.ι s i) = h (Fork.ι s i)
[PROOFSTEP]
apply congr_fun s.condition i
[GOAL]
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
⊢ (equalizerIso g h).hom ≫ Subtype.val = equalizer.ι g h
[PROOFSTEP]
rfl
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
a b : Y
h : CoequalizerRel f g a b
⊢ Cofork.π s a = Cofork.π s b
[PROOFSTEP]
cases h
[GOAL]
case Rel
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
x✝ : X
⊢ Cofork.π s (f x✝) = Cofork.π s (g x✝)
[PROOFSTEP]
apply congr_fun s.condition
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
⊢ π ⁻¹' (π '' U) = U
[PROOFSTEP]
have lem : ∀ x y, CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U) :=
  by
  rintro _ _ ⟨x⟩
  change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
  rw [H]
    -- porting note: tidy was able to fill the structure automatically
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
⊢ ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
[PROOFSTEP]
rintro _ _ ⟨x⟩
[GOAL]
case Rel
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ f x ∈ U ↔ g x ∈ U
[PROOFSTEP]
change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
[GOAL]
case Rel
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
[PROOFSTEP]
rw [H]
  -- porting note: tidy was able to fill the structure automatically
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ π ⁻¹' (π '' U) = U
[PROOFSTEP]
have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U :=
  { refl := by tauto
    symm := by tauto
    trans := by tauto }
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ (x : Y), x ∈ U ↔ x ∈ U
[PROOFSTEP]
tauto
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ {x y : Y}, (x ∈ U ↔ y ∈ U) → (y ∈ U ↔ x ∈ U)
[PROOFSTEP]
tauto
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ {x y z : Y}, (x ∈ U ↔ y ∈ U) → (y ∈ U ↔ z ∈ U) → (x ∈ U ↔ z ∈ U)
[PROOFSTEP]
tauto
[GOAL]
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
⊢ π ⁻¹' (π '' U) = U
[PROOFSTEP]
ext
[GOAL]
case h
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) ↔ x✝ ∈ U
[PROOFSTEP]
constructor
[GOAL]
case h.mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) → x✝ ∈ U
[PROOFSTEP]
rw [← show _ = π from h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2 WalkingParallelPair.one]
[GOAL]
case h.mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈
      (NatTrans.app (coequalizerColimit f g).cocone.ι WalkingParallelPair.one ≫
          (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv) ⁻¹'
        ((NatTrans.app (coequalizerColimit f g).cocone.ι WalkingParallelPair.one ≫
            (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv) ''
          U) →
    x✝ ∈ U
[PROOFSTEP]
rintro ⟨y, hy, e'⟩
[GOAL]
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' :
  (NatTrans.app (coequalizerColimit f g).cocone.ι WalkingParallelPair.one ≫
        (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv)
      y =
    (NatTrans.app (coequalizerColimit f g).cocone.ι WalkingParallelPair.one ≫
        (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv)
      x✝
⊢ x✝ ∈ U
[PROOFSTEP]
dsimp at e'
[GOAL]
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' :
  (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv
      (Cofork.π (coequalizerColimit f g).cocone y) =
    (IsColimit.coconePointUniqueUpToIso h (coequalizerColimit f g).isColimit).inv
      (Cofork.π (coequalizerColimit f g).cocone x✝)
⊢ x✝ ∈ U
[PROOFSTEP]
replace e' :=
  (mono_iff_injective (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp inferInstance e'
[GOAL]
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' : Cofork.π (coequalizerColimit f g).cocone y = Cofork.π (coequalizerColimit f g).cocone x✝
⊢ x✝ ∈ U
[PROOFSTEP]
exact (eqv.eqvGen_iff.mp (EqvGen.mono lem (Quot.exact _ e'))).mp hy
[GOAL]
case h.mpr
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), CoequalizerRel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ U → x✝ ∈ π ⁻¹' (π '' U)
[PROOFSTEP]
exact fun hx => ⟨_, hx, rfl⟩
[GOAL]
W X Y Z : Type u
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (s : PullbackCone f g),
    (fun s x =>
            { val := (PullbackCone.fst s x, PullbackCone.snd s x),
              property := (_ : (PullbackCone.fst s ≫ f) x = (PullbackCone.snd s ≫ g) x) })
          s ≫
        PullbackCone.fst (pullbackCone f g) =
      PullbackCone.fst s
[PROOFSTEP]
aesop
[GOAL]
W X Y Z : Type u
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (s : PullbackCone f g),
    (fun s x =>
            { val := (PullbackCone.fst s x, PullbackCone.snd s x),
              property := (_ : (PullbackCone.fst s ≫ f) x = (PullbackCone.snd s ≫ g) x) })
          s ≫
        PullbackCone.snd (pullbackCone f g) =
      PullbackCone.snd s
[PROOFSTEP]
aesop