Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁.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
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : s.pt → X'✝
hl : ∀ (x : s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) (l x)
hl' : ∀ (x : s.pt) (y : X'✝), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) y → y = l x
⊢ { l //
    l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).snd = s.snd → m = l }

Tactic:
refine ⟨↾(l), ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩

Goal state after:
case h₁.left.refine_1
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
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : s.pt → X'✝
hl : ∀ (x : s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) (l x)
hl' : ∀ (x : s.pt) (y : X'✝), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) y → y = l x
⊢ ↾l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).fst = s.fst

case h₁.left.refine_2
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
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : s.pt → X'✝
hl : ∀ (x : s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) (l x)
hl' : ∀ (x : s.pt) (y : X'✝), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) y → y = l x
l' : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).pt
h₁ : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).fst = s.fst
x✝ : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝)) αX✝ ⋯).snd = s.snd
⊢ l' = ↾l