[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
