[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit
X : C
⊢ F.obj X = G.obj X
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit
X : C
⊢ F.obj X = G.obj X
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
[PROOFSTEP]
refine' ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro _⟩
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
⊢ Unique (x ⟶ y)
[PROOFSTEP]
let f : x ⟶ y := by
  have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
  have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
  exact hx ≫ hy
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
⊢ x ⟶ y
[PROOFSTEP]
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
⊢ x ⟶ h.inverse.obj { as := PUnit.unit }
[PROOFSTEP]
convert h.unit.app x
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y
[PROOFSTEP]
have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ h.inverse.obj { as := PUnit.unit } ⟶ y
[PROOFSTEP]
convert h.unitInv.app y
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit } ⟶ y
⊢ x ⟶ y
[PROOFSTEP]
exact hx ≫ hy
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
⊢ Unique (x ⟶ y)
[PROOFSTEP]
suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
⊢ Subsingleton (x ⟶ y)
[PROOFSTEP]
have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y :=
  by
  intro z
  simp [congrArg (· ≫ h.unitInv.app y) (h.unit.naturality z)]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
⊢ ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
intro z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
z : x ⟶ y
⊢ z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
simp [congrArg (· ≫ h.unitInv.app y) (h.unit.naturality z)]
[GOAL]
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
⊢ Subsingleton (x ⟶ y)
[PROOFSTEP]
apply Subsingleton.intro
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
⊢ ∀ (a b : x ⟶ y), a = b
[PROOFSTEP]
intro a b
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ a = b
[PROOFSTEP]
rw [this a, this b]
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map a ≫ NatTrans.app (Equivalence.unitInv h) y =
    NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map b ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
simp only [Functor.comp_map]
[GOAL]
case mp.intro.allEq
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ NatTrans.app (Equivalence.unit h) x ≫ h.inverse.map (h.functor.map a) ≫ NatTrans.app (Equivalence.unitInv h) y =
    NatTrans.app (Equivalence.unit h) x ≫ h.inverse.map (h.functor.map b) ≫ NatTrans.app (Equivalence.unitInv h) y
[PROOFSTEP]
congr 3
[GOAL]
case mp.intro.allEq.e_a.e_a.e_a
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b
[PROOFSTEP]
apply ULift.ext
[GOAL]
case mp.intro.allEq.e_a.e_a.e_a.h
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      (id (NatTrans.app (Equivalence.unit h) x));
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      (id (NatTrans.app (Equivalence.unitInv h) y));
  hx ≫ hy
this :
  ∀ (z : x ⟶ y),
    z = NatTrans.app (Equivalence.unit h) x ≫ (h.functor ⋙ h.inverse).map z ≫ NatTrans.app (Equivalence.unitInv h) y
a b : x ⟶ y
⊢ (h.functor.map a).down = (h.functor.map b).down
[PROOFSTEP]
simp
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit)
[PROOFSTEP]
rintro ⟨⟨p⟩, h⟩
[GOAL]
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)
[PROOFSTEP]
haveI := fun x y => (h x y).some
[GOAL]
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)
[PROOFSTEP]
refine'
  Nonempty.intro
    (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩) ((@Functor.const <| Discrete PUnit).obj p) ?_
      (by apply Functor.punitExt))
[GOAL]
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)).obj p ⋙ (Functor.const C).obj { as := PUnit.unit } ≅ 𝟭 (Discrete PUnit)
[PROOFSTEP]
apply Functor.punitExt
[GOAL]
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)
⊢ 𝟭 C ≅ (Functor.const C).obj { as := PUnit.unit } ⋙ (Functor.const (Discrete PUnit)).obj p
[PROOFSTEP]
exact
  NatIso.ofComponents fun _ =>
    { hom := default
      inv := default }
