-- Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean
theorem over_hasTerminal (B : C) : HasTerminal (Over B) where
  has_limit F := HasLimit.mk
    { cone :=
        { pt := Over.mk (𝟙 _)
          π :=
            { app := fun p => p.as.elim } }
      isLimit :=
        { lift := fun s => Over.homMk s.pt.hom
          fac := fun _ j => j.as.elim
          uniq := fun s m _ => by
            simp only
            ext
            rw [Over.homMk_left _]
            have := m.w
            dsimp at this
            rwa [Category.comp_id, Category.comp_id] at this } }

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
this :
  (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt.hom =
    s.pt.hom ≫ (Functor.fromPUnit B).map m.right
⊢ m.left = s.pt.hom

Tactic:
dsimp at this

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B
⊢ m.left = s.pt.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m = homMk s.pt.hom ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m.left = (homMk s.pt.hom ⋯).left

Proof state:
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m = (fun s => homMk s.pt.hom ⋯) s

Tactic:
simp only

Result:
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m = homMk s.pt.hom ⋯

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m.left = (homMk s.pt.hom ⋯).left

Tactic:
rw [Over.homMk_left _]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m.left = s.pt.hom

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m.left = s.pt.hom

Tactic:
have := m.w

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
this :
  (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt.hom =
    s.pt.hom ≫ (Functor.fromPUnit B).map m.right
⊢ m.left = s.pt.hom

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p => p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B
⊢ m.left = s.pt.hom

Tactic:
rwa [Category.comp_id, Category.comp_id] at this

Result:
no goals