Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂.desc
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))) → Z ⟶ s.pt

pp: case fac_left
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))),
    (↾fun p ↦ (↑p).1) ≫ ?h₂.desc s = s.inl

pp: case h₂.fac_right
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))),
    (↾fun p ↦ (↑p).1) ≫ ?h₂.desc s = s.inr

pp: case h₂.uniq
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))) (m : Z ⟶ s.pt),
    (↾fun p ↦ (↑p).1) ≫ m = s.inl → (↾fun p ↦ (↑p).1) ≫ m = s.inr → m = ?h₂.desc s

Tactic:
· exact fun s => ↾fun x => dite _ (fun h => s.inl <| eX.symm ⟨x, h⟩)
        fun h => s.inr <| eY.symm ⟨x, (this x).resolve_left h⟩

Goal state after:
case fac_left
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))),
    ((↾fun p ↦ (↑p).1) ≫
        ↾fun x ↦
          if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
          else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)) =
      s.inl

case h₂.fac_right
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))),
    ((↾fun p ↦ (↑p).1) ≫
        ↾fun x ↦
          if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
          else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)) =
      s.inr

case h₂.uniq
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))) (m : Z ⟶ s.pt),
    (↾fun p ↦ (↑p).1) ≫ m = s.inl →
      (↾fun p ↦ (↑p).1) ≫ m = s.inr →
        m =
          ↾fun x ↦
            if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
            else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)