case mp
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ EssentiallySmall C → EssentiallySmall D

case mpr
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ EssentiallySmall D → EssentiallySmall C
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ EssentiallySmall C ↔ EssentiallySmall D
fconstructor
case mp.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall D
case mp
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ EssentiallySmall C → EssentiallySmall D
rintro ⟨S, 𝒮, ⟨f⟩⟩
case mp.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall D
case mp.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall D
skip
no goals
case mp.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall D
exact EssentiallySmall.mk' (e.symm.trans f)
case mpr.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall C
case mpr
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ EssentiallySmall D → EssentiallySmall C
rintro ⟨S, 𝒮, ⟨f⟩⟩
case mpr.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall C
case mpr.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall C
skip
no goals
case mpr.mk.intro.intro.intro
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall C
exact EssentiallySmall.mk' (e.trans f)