[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
⊢ f = g
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
x✝ : β
⊢ f x✝ = g x✝
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ eqToHom h i = eqToHom (_ : x i = x' i)
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ (comap C f).obj X b = (comap C g).obj X b
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (f b) = X (g b)
[PROOFSTEP]
simp only [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ (comap C g).obj X b = (comap C f).obj X b
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (g b) = X (f b)
[PROOFSTEP]
simp only [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
⊢ comapEq C (_ : g = f) = (comapEq C h).symm
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g h : β → γ
k : f = g
l : g = h
⊢ comapEq C (_ : f = h) = comapEq C k ≪≫ comapEq C l
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ X b = Y b
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ eqToHom h b = eqToHom (_ : X b = Y b)
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ eqToHom (_ : X = X) b = eqToHom (_ : X b = X b)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ (fun i => i) = ↑e.symm ∘ ↑e
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : β
⊢ x✝ = (↑e.symm ∘ ↑e) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ ↑e ∘ ↑e.symm = fun i => i
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : γ
⊢ (↑e ∘ ↑e.symm) x✝ = x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
⊢ (fun b => b + 0 • s) = id
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
⊢ (fun b => b + (m + n) • s) = (fun b => b + m • s) ∘ fun b => b + n • s
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = ((fun b => b + m • s) ∘ fun b => b + n • s) x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = x✝ + n • s + m • s
[PROOFSTEP]
rw [add_comm m n, add_zsmul, add_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
⊢ HasZeroObject (GradedObject β C)
[PROOFSTEP]
refine' ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨fun b => 0⟩, fun f => _⟩⟩⟩⟩
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
X : GradedObject β C
f : (fun x => 0) ⟶ X
⊢ f = default
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
X : GradedObject β C
f : X ⟶ fun x => 0
⊢ f = default
[PROOFSTEP]
aesop_cat
[GOAL]
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
⊢ f = g
[PROOFSTEP]
ext i
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
i : β
⊢ f i = g i
[PROOFSTEP]
replace w := Sigma.ι (fun i : β => X i) i ≫= w
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w : Sigma.ι (fun i => X i) i ≫ (total β C).map f = Sigma.ι (fun i => X i) i ≫ (total β C).map g
⊢ f i = g i
[PROOFSTEP]
erw [colimit.ι_map, colimit.ι_map] at w
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w✝¹ : Sigma.ι (fun i => X i) i ≫ (total β C).map f = Sigma.ι (fun i => X i) i ≫ (total β C).map g
w✝ :
  NatTrans.app (Discrete.natTrans fun X => (fun i => f i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun i => Y i) { as := i } =
    Sigma.ι (fun i => X i) i ≫ (total β C).map g
w :
  NatTrans.app (Discrete.natTrans fun X => (fun i => f i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun i => Y i) { as := i } =
    NatTrans.app (Discrete.natTrans fun X => (fun i => g i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun i => Y i) { as := i }
⊢ f i = g i
[PROOFSTEP]
simp at *
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w✝¹ : Sigma.ι (fun i => X i) i ≫ (total β C).map f = Sigma.ι (fun i => X i) i ≫ (total β C).map g
w✝ : f i ≫ colimit.ι (Discrete.functor fun i => Y i) { as := i } = Sigma.ι (fun i => X i) i ≫ (total β C).map g
w :
  f i ≫ colimit.ι (Discrete.functor fun i => Y i) { as := i } =
    g i ≫ colimit.ι (Discrete.functor fun i => Y i) { as := i }
⊢ f i = g i
[PROOFSTEP]
exact Mono.right_cancellation _ _ w


[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]