case mp
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso (fst c)

case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso (fst c) → Nonempty (IsLimit c)
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso (fst c)
constructor
case mp.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
⊢ IsIso (fst c)
case mp
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso (fst c)
rintro ⟨H⟩
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ fst c = 𝟙 X
⊢ IsIso (fst c)
case mp.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
⊢ IsIso (fst c)
obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
no goals
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ fst c = 𝟙 X
⊢ IsIso (fst c)
exact
  ⟨⟨l,
      BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
        (h.hom_ext _ _),
      hl⟩⟩
no goals
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ fst c = 𝟙 X
⊢ (fst c ≫ l) ≫ fst c = 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }) ≫ fst c
simpa [hl, -Category.comp_id] using Category.comp_id _
case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
⊢ Nonempty (IsLimit c)
case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso (fst c) → Nonempty (IsLimit c)
intro
no goals
case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
⊢ Nonempty (IsLimit c)
exact
  ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
      (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩
no goals
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
T✝ : C
x✝¹ : T✝ ⟶ X
x✝ : T✝ ⟶ Y
⊢ (fun {T} f x => f ≫ inv (fst c)) x✝¹ x✝ ≫ fst c = x✝¹
simp
no goals
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso (fst c)
T✝ : C
x✝³ : T✝ ⟶ X
x✝² : T✝ ⟶ Y
x✝¹ : T✝ ⟶ c.pt
e : x✝¹ ≫ fst c = x✝³
x✝ : x✝¹ ≫ snd c = x✝²
⊢ x✝¹ = (fun {T} f x => f ≫ inv (fst c)) x✝³ x✝²
simp [← e]