-- Mathlib/CategoryTheory/EssentiallySmall.lean
theorem essentiallySmall_iff (C : Type u) [Category.{v} C] :
    EssentiallySmall.{w} C ↔ Small.{w} (Skeleton C) ∧ LocallySmall.{w} C

Proof state:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall.{w, v, u} C

Tactic:
let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm

Result:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
⊢ EssentiallySmall.{w, v, u} C

Proof state:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
this : Category.{w, w} S := InducedCategory.category ⇑(e'.trans e).symm
⊢ EssentiallySmall.{w, v, u} C

Tactic:
refine ⟨⟨S, this, ⟨?_⟩⟩⟩

Result:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
this : Category.{w, w} S := InducedCategory.category ⇑(e'.trans e).symm
⊢ C ≌ S

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C → EssentiallySmall.{w, v, u} C

Tactic:
rintro ⟨⟨S, ⟨e⟩⟩, L⟩

Result:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall.{w, v, u} C

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C

Tactic:
fconstructor

Result:
case mp.left
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton C)

case mp.right
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Proof state:
case mp.right
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp.left.mk.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small.{w, u} (Skeleton C)

Tactic:
refine ⟨⟨Skeleton S, ⟨?_⟩⟩⟩

Result:
case mp.left.mk.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Skeleton C ≃ Skeleton S

Proof state:
case mp.left
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton C)

Tactic:
rcases h with ⟨S, 𝒮, ⟨e⟩⟩

Result:
case mp.left.mk.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small.{w, u} (Skeleton C)

Proof state:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
⊢ EssentiallySmall.{w, v, u} C

Tactic:
letI : Category S := InducedCategory.category (e'.trans e).symm

Result:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
this : Category.{w, w} S := InducedCategory.category ⇑(e'.trans e).symm
⊢ EssentiallySmall.{w, v, u} C

Proof state:
case mpr.intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
this : Category.{w, w} S := InducedCategory.category ⇑(e'.trans e).symm
⊢ C ≌ S

Tactic:
refine (ShrinkHoms.equivalence C).trans <|
  (skeletonEquivalence (ShrinkHoms C)).symm.trans
    ((inducedFunctor (e'.trans e).symm).asEquivalence.symm)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C

Tactic:
fconstructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ EssentiallySmall.{w, v, u} C → Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C

case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C → EssentiallySmall.{w, v, u} C

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ EssentiallySmall.{w, v, u} C → Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C

Tactic:
intro h

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C

Proof state:
case mp.left.mk.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Skeleton C ≃ Skeleton S

Tactic:
exact e.skeletonEquiv

Result:
no goals