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))

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)
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))
constructor
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))
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))
rintro ⟨h⟩
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ((binaryCoproductCocone X Y).ι.app { as := left } ≫
        (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
    Injective
        ((binaryCoproductCocone X Y).ι.app { as := right } ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
      IsCompl
        (Set.range
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
        (Set.range
          ((binaryCoproductCocone X Y).ι.app { as := right } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
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))
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⟩]
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))
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ((binaryCoproductCocone X Y).ι.app { as := left } ≫
        (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
    Injective
        ((binaryCoproductCocone X Y).ι.app { as := right } ≫
          (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv) ∧
      IsCompl
        (Set.range
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
        (Set.range
          ((binaryCoproductCocone X Y).ι.app { as := right } ≫
            (IsColimit.coconePointUniqueUpToIso h (binaryCoproductColimit X Y)).inv))
dsimp [binaryCoproductCocone]
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))
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))
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, _⟩
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ᶜ
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))
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]
no goals
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ᶜ
simp
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)
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)
rintro ⟨h₁, h₂, h₃⟩
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)
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)
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
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)

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 ≫ ?mpr.intro.intro.refine'_1 f g = f

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 ≫ ?mpr.intro.intro.refine'_1 f g = g

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 = ?mpr.intro.intro.refine'_1 f g
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)
refine' ⟨BinaryCofan.IsColimit.mk _ _ _ _ _⟩
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)ᶜ
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)
rw [eq_compl_iff_isCompl.mpr h₃.symm]
no goals
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)ᶜ
exact fun _ => or_not
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
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)
intro T f g x
no goals
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
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⟩)
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
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
intro T f g
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
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
funext x
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
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
dsimp
no goals
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
simp [h₁.eq_iff]
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
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
intro T f g
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
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
funext x
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
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
dsimp
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
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
simp only [Set.mem_range, Equiv.ofInjective_symm_apply,
  dite_eq_right_iff, forall_exists_index]
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
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
intro y e
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
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
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
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
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
rw [disjoint_iff.mp h₃.1] at this
no goals
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
exact this.elim
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)) })
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)) })
rintro T _ _ m rfl rfl
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)) })
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)) })
funext x
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)) }))
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)) })
dsimp
no goals
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)) }))
split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm