[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall C ↔ EssentiallySmall D
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall C → EssentiallySmall D
[PROOFSTEP]
rintro ⟨S, 𝒮, ⟨f⟩⟩
[GOAL]
case mp.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall D
[PROOFSTEP]
skip
[GOAL]
case mp.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall D
[PROOFSTEP]
exact EssentiallySmall.mk' (e.symm.trans f)
[GOAL]
case mpr
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall D → EssentiallySmall C
[PROOFSTEP]
rintro ⟨S, 𝒮, ⟨f⟩⟩
[GOAL]
case mpr.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall C
[PROOFSTEP]
skip
[GOAL]
case mpr.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall C
[PROOFSTEP]
exact EssentiallySmall.mk' (e.trans f)
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ LocallySmall C ↔ LocallySmall D
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ LocallySmall C → LocallySmall D
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mp.mk
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
L : ∀ (X Y : C), Small.{w, v} (X ⟶ Y)
⊢ LocallySmall D
[PROOFSTEP]
fconstructor
[GOAL]
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
L : ∀ (X Y : C), Small.{w, v} (X ⟶ Y)
⊢ autoParam (∀ (X Y : D), Small.{w, v'} (X ⟶ Y)) _auto✝
[PROOFSTEP]
intro X Y
[GOAL]
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
L : ∀ (X Y : C), Small.{w, v} (X ⟶ Y)
X Y : D
⊢ Small.{w, v'} (X ⟶ Y)
[PROOFSTEP]
specialize L (e.inverse.obj X) (e.inverse.obj Y)
[GOAL]
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
X Y : D
L : Small.{w, v} (e.inverse.obj X ⟶ e.inverse.obj Y)
⊢ Small.{w, v'} (X ⟶ Y)
[PROOFSTEP]
refine' (small_congr _).mpr L
[GOAL]
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
X Y : D
L : Small.{w, v} (e.inverse.obj X ⟶ e.inverse.obj Y)
⊢ (X ⟶ Y) ≃ (e.inverse.obj X ⟶ e.inverse.obj Y)
[PROOFSTEP]
exact equivOfFullyFaithful e.inverse
[GOAL]
case mpr
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ LocallySmall D → LocallySmall C
[PROOFSTEP]
rintro ⟨L⟩
[GOAL]
case mpr.mk
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
L : ∀ (X Y : D), Small.{w, v'} (X ⟶ Y)
⊢ LocallySmall C
[PROOFSTEP]
fconstructor
[GOAL]
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
L : ∀ (X Y : D), Small.{w, v'} (X ⟶ Y)
⊢ autoParam (∀ (X Y : C), Small.{w, v} (X ⟶ Y)) _auto✝
[PROOFSTEP]
intro X Y
[GOAL]
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
L : ∀ (X Y : D), Small.{w, v'} (X ⟶ Y)
X Y : C
⊢ Small.{w, v} (X ⟶ Y)
[PROOFSTEP]
specialize L (e.functor.obj X) (e.functor.obj Y)
[GOAL]
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
X Y : C
L : Small.{w, v'} (e.functor.obj X ⟶ e.functor.obj Y)
⊢ Small.{w, v} (X ⟶ Y)
[PROOFSTEP]
refine' (small_congr _).mpr L
[GOAL]
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
X Y : C
L : Small.{w, v'} (e.functor.obj X ⟶ e.functor.obj Y)
⊢ (X ⟶ Y) ≃ (e.functor.obj X ⟶ e.functor.obj Y)
[PROOFSTEP]
exact equivOfFullyFaithful e.functor
[GOAL]
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
⊢ EssentiallySmall C ↔ Small.{w, u} (Skeleton C) ∧ LocallySmall C
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
⊢ EssentiallySmall C → Small.{w, u} (Skeleton C) ∧ LocallySmall C
[PROOFSTEP]
intro h
[GOAL]
case mp
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall C
[PROOFSTEP]
fconstructor
[GOAL]
case mp.left
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall C
⊢ Small.{w, u} (Skeleton C)
[PROOFSTEP]
rcases h with ⟨S, 𝒮, ⟨e⟩⟩
[GOAL]
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small.{w, u} (Skeleton C)
[PROOFSTEP]
skip
[GOAL]
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Small.{w, u} (Skeleton C)
[PROOFSTEP]
refine' ⟨⟨Skeleton S, ⟨_⟩⟩⟩
[GOAL]
case mp.left.mk.intro.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Skeleton C ≃ Skeleton S
[PROOFSTEP]
exact e.skeletonEquiv
[GOAL]
case mp.right
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall C
⊢ LocallySmall C
[PROOFSTEP]
skip
[GOAL]
case mp.right
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall C
⊢ LocallySmall C
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall C → EssentiallySmall C
[PROOFSTEP]
rintro ⟨⟨S, ⟨e⟩⟩, L⟩
[GOAL]
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall C
[PROOFSTEP]
skip
[GOAL]
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall C
S : Type w
e : Skeleton C ≃ S
⊢ EssentiallySmall C
[PROOFSTEP]
let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm
[GOAL]
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} 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
[PROOFSTEP]
letI : Category S := InducedCategory.category (e'.trans e).symm
[GOAL]
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} 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.{w, w} S := InducedCategory.category ↑(e'.trans e).symm
⊢ EssentiallySmall C
[PROOFSTEP]
refine' ⟨⟨S, this, ⟨_⟩⟩⟩
[GOAL]
case mpr.intro.mk.intro.intro
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u
inst✝ : Category.{v, u} 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.{w, w} S := InducedCategory.category ↑(e'.trans e).symm
⊢ C ≌ S
[PROOFSTEP]
refine'
  (ShrinkHoms.equivalence C).trans <|
    (skeletonEquivalence (ShrinkHoms C)).symm.trans ((inducedFunctor (e'.trans e).symm).asEquivalence.symm)
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
⊢ EssentiallySmall C ↔ Small.{w, u} (Skeleton C)
[PROOFSTEP]
simp [essentiallySmall_iff, CategoryTheory.locallySmall_of_thin]
