case mp
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
⊢ EssentiallySmall C → Small (Skeleton C) ∧ LocallySmall C

case mpr
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
⊢ Small (Skeleton C) ∧ LocallySmall C → EssentiallySmall C
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
⊢ EssentiallySmall C ↔ Small (Skeleton C) ∧ LocallySmall C
fconstructor
case mp
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ Small (Skeleton C) ∧ LocallySmall C
case mp
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
⊢ EssentiallySmall C → Small (Skeleton C) ∧ LocallySmall C
intro h
case mp.left
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ Small (Skeleton C)

case mp.right
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ LocallySmall C
case mp
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ Small (Skeleton C) ∧ LocallySmall C
fconstructor
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small (Skeleton C)
case mp.left
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ Small (Skeleton C)
rcases h with ⟨S, 𝒮, ⟨e⟩⟩
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small (Skeleton C)
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small (Skeleton C)
skip
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Skeleton C ≃ Skeleton S
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small (Skeleton C)
refine' ⟨⟨Skeleton S, ⟨_⟩⟩⟩
no goals
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Skeleton C ≃ Skeleton S
exact e.skeletonEquiv
case mp.right
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ LocallySmall C
case mp.right
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ LocallySmall C
skip
no goals
case mp.right
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
h : EssentiallySmall C
⊢ LocallySmall C
infer_instance
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall C
case mpr
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
⊢ Small (Skeleton C) ∧ LocallySmall C → EssentiallySmall C
rintro ⟨⟨S, ⟨e⟩⟩, L⟩
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall C
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall C
skip
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms C) ≃ Skeleton C := (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C)).symm
⊢ EssentiallySmall C
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall C
let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms C) ≃ Skeleton C := (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C)).symm
this : Category S := InducedCategory.category ↑(e'.trans e).symm
⊢ EssentiallySmall C
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms C) ≃ Skeleton C := (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C)).symm
⊢ EssentiallySmall C
letI : Category S := InducedCategory.category (e'.trans e).symm
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms C) ≃ Skeleton C := (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C)).symm
this : Category S := InducedCategory.category ↑(e'.trans e).symm
⊢ C ≌ S
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms C) ≃ Skeleton C := (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C)).symm
this : Category S := InducedCategory.category ↑(e'.trans e).symm
⊢ EssentiallySmall C
refine' ⟨⟨S, this, ⟨_⟩⟩⟩
no goals
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category C✝
C : Type u
inst✝ : Category C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms C) ≃ Skeleton C := (Equivalence.skeletonEquiv (ShrinkHoms.equivalence C)).symm
this : Category S := InducedCategory.category ↑(e'.trans e).symm
⊢ C ≌ S
refine' (ShrinkHoms.equivalence C).trans <|
  (skeletonEquivalence (ShrinkHoms C)).symm.trans
    ((inducedFunctor (e'.trans e).symm).asEquivalence.symm)