-- Mathlib/CategoryTheory/PUnit.lean
theorem equiv_punit_iff_unique :
    Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ x ⟶ h.inverse.obj { as := PUnit.unit }

Tactic:
convert h.unit.app x

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y

Tactic:
intro z

Result:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
z : x ⟶ y
⊢ z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ h.inverse.obj { as := PUnit.unit } ⟶ y

Tactic:
convert h.unitInv.app y

Result:
no goals

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ Unique (x ⟶ y)

Tactic:
suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ Subsingleton (x ⟶ y)

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})

Tactic:
rintro ⟨⟨p⟩, h⟩

Result:
case mpr.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1})

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ x ⟶ y

Tactic:
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x

Result:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ (Functor.const (Discrete PUnit.{w + 1})).obj p ⋙ (Functor.const C).obj { as := PUnit.unit } ≅
    𝟭 (Discrete PUnit.{w + 1})

Tactic:
apply Functor.punitExt

Result:
no goals

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
⊢ Subsingleton (x ⟶ y)

Tactic:
apply Subsingleton.intro

Result:
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
⊢ ∀ (a b : x ⟶ y), a = b

Proof state:
case mp.intro.allEq.e_a.e_a.e_a.h
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ (h.functor.map a).down = (h.functor.map b).down

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit } ⟶ y
⊢ x ⟶ y

Tactic:
exact hx ≫ hy

Result:
no goals

Proof state:
case mpr.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1})

Tactic:
haveI := fun x y => (h x y).some

Result:
case mpr.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1})

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

Tactic:
refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ Unique (x ⟶ y)

Proof state:
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y

Tactic:
simp only [Functor.comp_map]

Result:
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
    h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y

Proof state:
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
    h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y

Tactic:
congr 3

Result:
case mp.intro.allEq.e_a.e_a.e_a
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b

Proof state:
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ a = b

Tactic:
rw [this a, this b]

Result:
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  let_fun hx := ⋯.mpr (h.unit.app x);
  let_fun hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1}) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})