[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongEpi f
inst✝ : StrongEpi g
⊢ ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : Mono z], HasLiftingProperty (f ≫ g) z
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongEpi f
inst✝¹ : StrongEpi g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Mono z✝
⊢ HasLiftingProperty (f ≫ g) z✝
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono f
inst✝ : StrongMono g
⊢ ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : Epi z], HasLiftingProperty z (f ≫ g)
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongMono f
inst✝¹ : StrongMono g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Epi z✝
⊢ HasLiftingProperty z✝ (f ≫ g)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ HasLiftingProperty g z
[PROOFSTEP]
constructor
[GOAL]
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), CommSq.HasLift sq
[PROOFSTEP]
intro u v sq
[GOAL]
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ CommSq.HasLift sq
[PROOFSTEP]
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ (f ≫ u) ≫ z = (f ≫ g) ≫ v
[PROOFSTEP]
simp only [Category.assoc, sq.w]
[GOAL]
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact
  CommSq.HasLift.mk'
    ⟨(CommSq.mk h₀).lift, by simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ g ≫ CommSq.lift (_ : CommSq (f ≫ u) (f ≫ g) z v) = u
[PROOFSTEP]
simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ CommSq.lift (_ : CommSq (f ≫ u) (f ≫ g) z v) ≫ z = v
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Epi z], HasLiftingProperty z f
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z f
[PROOFSTEP]
constructor
[GOAL]
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ ∀ {f_1 : X ⟶ P} {g : Y ⟶ Q} (sq : CommSq f_1 z f g), CommSq.HasLift sq
[PROOFSTEP]
intro u v sq
[GOAL]
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ CommSq.HasLift sq
[PROOFSTEP]
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ u ≫ f ≫ g = z ≫ v ≫ g
[PROOFSTEP]
rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
[GOAL]
case sq_hasLift
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ CommSq.HasLift sq
[PROOFSTEP]
exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ z ≫ CommSq.lift (_ : CommSq u z (f ≫ g) (v ≫ g)) = u
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst✝ : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ CommSq.lift (_ : CommSq u z (f ≫ g) (v ≫ g)) ≫ f = v
[PROOFSTEP]
simp [← cancel_epi z, sq.w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ Epi f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ Mono f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi g
[PROOFSTEP]
rw [Arrow.iso_w' e]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi (e.inv.left ≫ f ≫ e.hom.right)
[PROOFSTEP]
haveI := epi_comp f e.hom.right
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
this : Epi (f ≫ e.hom.right)
⊢ Epi (e.inv.left ≫ f ≫ e.hom.right)
[PROOFSTEP]
apply epi_comp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Mono z], HasLiftingProperty g z
[PROOFSTEP]
intro
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
inst✝ : Mono z
⊢ HasLiftingProperty g z
[PROOFSTEP]
apply HasLiftingProperty.of_arrow_iso_left e z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono g
[PROOFSTEP]
rw [Arrow.iso_w' e]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
[PROOFSTEP]
haveI := mono_comp f e.hom.right
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
this : Mono (f ≫ e.hom.right)
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
[PROOFSTEP]
apply mono_comp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Epi z], HasLiftingProperty z g
[PROOFSTEP]
intro
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z g
[PROOFSTEP]
apply HasLiftingProperty.of_arrow_iso_right z e
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f ↔ StrongEpi g
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f → StrongEpi g
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi g → StrongEpi f
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongEpi f
⊢ StrongEpi g
case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongEpi g
⊢ StrongEpi f
[PROOFSTEP]
exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongMono f ↔ StrongMono g
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongMono f → StrongMono g
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongMono g → StrongMono f
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongMono f
⊢ StrongMono g
case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q R : C
f✝ : P ⟶ Q
g✝ : Q ⟶ R
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongMono g
⊢ StrongMono f
[PROOFSTEP]
exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Mono f
inst✝ : StrongEpi f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Mono f
inst✝ : StrongEpi f
⊢ f ≫ CommSq.lift (_ : CommSq (𝟙 P) f f (𝟙 Q)) = 𝟙 P ∧ CommSq.lift (_ : CommSq (𝟙 P) f f (𝟙 Q)) ≫ f = 𝟙 Q
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Epi f
inst✝ : StrongMono f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Epi f
inst✝ : StrongMono f
⊢ f ≫ CommSq.lift (_ : CommSq (𝟙 P) f f (𝟙 Q)) = 𝟙 P ∧ CommSq.lift (_ : CommSq (𝟙 P) f f (𝟙 Q)) ≫ f = 𝟙 Q
[PROOFSTEP]
aesop_cat


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π
[PROOFSTEP]
rw [← F.map_comp, q.condition, F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)
[PROOFSTEP]
rw [← F.map_comp, q.rightSection_π, F.map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← F.map_comp, q.leftSection_bottom, F.map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection
[PROOFSTEP]
rw [← F.map_comp, q.leftSection_top, F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ Cofork.π (asCofork t) ≫ t.rightSection ≫ Cofork.π s = Cofork.π s
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ h ≫ t.rightSection ≫ Cofork.π s = Cofork.π s
[PROOFSTEP]
rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj (asCofork t).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (asCofork t) ≫ m✝ = Cofork.π s
⊢ m✝ = t.rightSection ≫ Cofork.π s
[PROOFSTEP]
simp [← hm]


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesLimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cone K} → IsLimit c → IsLimit (F.mapCone c)
⊢ { preserves := a } = { preserves := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesColimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cocone K} → IsColimit c → IsColimit (F.mapCocone c)
⊢ { preserves := a } = { preserves := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : PreservesLimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → PreservesLimit K F
⊢ PreservesLimitsOfShape.mk = PreservesLimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : PreservesColimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → PreservesColimit K F
⊢ PreservesColimitsOfShape.mk = PreservesColimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesLimitsOfShape J F
⊢ PreservesLimitsOfSize.mk = PreservesLimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_preservesLimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesLimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_preservesLimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesLimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesColimitsOfShape J F
⊢ PreservesColimitsOfSize.mk = PreservesColimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_preservesColimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesColimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_preservesColimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → PreservesColimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app ((𝟭 C).mapCone c).π j =
      NatTrans.app s.π j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit c
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app ((𝟭 C).mapCone c).π j =
      NatTrans.app s.π j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j =
      NatTrans.app s.π j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
j : J
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
      NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j =
    NatTrans.app s.π j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝¹, π := NatTrans.mk app✝ }
j : J
pt✝ : C
π✝ : (Functor.const J).obj pt✝ ⟶ Functor.mk toPrefunctor✝ ⋙ 𝟭 C
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) { pt := pt✝, π := π✝ } ≫
      NatTrans.app ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝ }).π j =
    NatTrans.app { pt := pt✝, π := π✝ }.π j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone c).pt),
    (∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone c).π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit c
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone c).pt),
    (∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone c).π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).pt),
    (∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝, π := NatTrans.mk app✝ }
s : Cone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).pt
w : ∀ (j : J), m ≫ NatTrans.app ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ }).π j = NatTrans.app s.π j
⊢ m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y = app✝¹ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit { pt := pt✝¹, π := NatTrans.mk app✝¹ }
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).map f
m : { pt := pt✝, π := NatTrans.mk app✝ }.pt ⟶ ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝¹ }).pt
w :
  ∀ (j : J),
    m ≫ NatTrans.app ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝¹ }).π j =
      NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j
⊢ m =
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j })
      { pt := pt✝, π := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    NatTrans.app ((𝟭 C).mapCocone c).ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit c
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    NatTrans.app ((𝟭 C).mapCocone c).ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (j : J),
    NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
j : J
⊢ NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
    NatTrans.app s.ι j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit { pt := pt✝¹, ι := NatTrans.mk app✝ }
j : J
pt✝ : C
ι✝ : Functor.mk toPrefunctor✝ ⋙ 𝟭 C ⟶ (Functor.const J).obj pt✝
⊢ NatTrans.app ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝ }).ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) { pt := pt✝, ι := ι✝ } =
    NatTrans.app { pt := pt✝, ι := ι✝ }.ι j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (m : ((𝟭 C).mapCocone c).pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app ((𝟭 C).mapCocone c).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit c
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)) (m : ((𝟭 C).mapCocone c).pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app ((𝟭 C).mapCocone c).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C))
    (m : ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := NatTrans.mk app✝ }
s : Cocone (Functor.mk toPrefunctor✝ ⋙ 𝟭 C)
m : ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ }).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝¹ Y = app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit { pt := pt✝¹, ι := NatTrans.mk app✝¹ }
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝ ⋙ 𝟭 C).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
m : ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝¹ }).pt ⟶ { pt := pt✝, ι := NatTrans.mk app✝ }.pt
w :
  ∀ (j : J),
    NatTrans.app ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝¹ }).ι j ≫ m =
      NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j
⊢ m =
    (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j })
      { pt := pt✝, ι := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
apply IsLimit.postcomposeInvEquiv (isoWhiskerRight h F : _) _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))
[PROOFSTEP]
have := (IsLimit.postcomposeInvEquiv h c).symm t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : (fun x => IsLimit ((Cones.postcompose h.inv).obj c)) t
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))
[PROOFSTEP]
apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : (fun x => IsLimit ((Cones.postcompose h.inv).obj c)) t
⊢ F.mapCone ((Cones.postcompose h.inv).obj c) ≅ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c)
[PROOFSTEP]
refine' Cones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
let equ := e.invFunIdAssoc (K ⋙ F)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone c)
[PROOFSTEP]
apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cones.postcompose equ.hom).obj (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c))) ≅
    F.mapCone c
[PROOFSTEP]
refine' Cones.ext (Iso.refl _) fun j => _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ NatTrans.app
      ((Cones.postcompose equ.hom).obj
          (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))).π
      j =
    (Iso.refl
          ((Cones.postcompose equ.hom).obj
              (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))).pt).hom ≫
      NatTrans.app (F.mapCone c).π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsLimit (Cone.whisker (Equivalence.symm e).functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ F.map (NatTrans.app c.π (e.functor.obj (e.inverse.obj j))) ≫
      NatTrans.app (Equivalence.invFunIdAssoc e (K ⋙ F)).hom j =
    𝟙 (F.obj c.pt) ≫ F.map (NatTrans.app c.π j)
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply IsColimit.precomposeHomEquiv (isoWhiskerRight h F : _) _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))
[PROOFSTEP]
have := (IsColimit.precomposeHomEquiv h c).symm t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : (fun x => IsColimit ((Cocones.precompose h.hom).obj c)) t
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))
[PROOFSTEP]
apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : (fun x => IsColimit ((Cocones.precompose h.hom).obj c)) t
⊢ F.mapCocone ((Cocones.precompose h.hom).obj c) ≅ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c)
[PROOFSTEP]
refine' Cocones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
let equ := e.invFunIdAssoc (K ⋙ F)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocones.precompose equ.inv).obj
      (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c
[PROOFSTEP]
refine' Cocones.ext (Iso.refl _) fun j => _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ NatTrans.app
        ((Cocones.precompose equ.inv).obj
            (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose equ.inv).obj
              (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))).pt).hom =
    NatTrans.app (F.mapCocone c).ι j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := Equivalence.invFunIdAssoc e (K ⋙ F)
this : IsColimit (Cocone.whisker (Equivalence.symm e).functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ (NatTrans.app (Equivalence.invFunIdAssoc e (K ⋙ F)).inv j ≫
        F.map (NatTrans.app c.ι (e.functor.obj (e.inverse.obj j)))) ≫
      𝟙 (F.obj c.pt) =
    F.map (NatTrans.app c.ι j)
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cone K} → IsLimit (F.mapCone c) → IsLimit c
⊢ { reflects := a } = { reflects := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimit K F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimit K F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : {c : Cocone K} → IsColimit (F.mapCocone c) → IsColimit c
⊢ { reflects := a } = { reflects := b }
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → ReflectsLimit K F
⊢ ReflectsLimitsOfShape.mk = ReflectsLimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfShape J F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimitsOfShape J F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : {K : J ⥤ C} → ReflectsColimit K F
⊢ ReflectsColimitsOfShape.mk = ReflectsColimitsOfShape.mk
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsLimitsOfShape J F
⊢ ReflectsLimitsOfSize.mk = ReflectsLimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_reflectsLimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsLimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_reflectsLimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsLimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
[PROOFSTEP]
constructor
[GOAL]
case allEq
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case allEq.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsColimitsOfShape J F
⊢ ReflectsColimitsOfSize.mk = ReflectsColimitsOfSize.mk
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_reflectsColimitsOfShape
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsColimitsOfShape J F
⊢ a = b
[PROOFSTEP]
funext
[GOAL]
case allEq.mk.mk.e_reflectsColimitsOfShape.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : {J : Type w} → [inst : Category.{w', w} J] → ReflectsColimitsOfShape J F
x✝¹ : Type w
x✝ : Category.{w', w} x✝¹
⊢ a = b
[PROOFSTEP]
congr!
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫ NatTrans.app c.π j =
      NatTrans.app s.π j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫ NatTrans.app c.π j =
      NatTrans.app s.π j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (j : J),
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
        NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j =
      NatTrans.app s.π j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
s : Cone (Functor.mk toPrefunctor✝)
j : J
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s ≫
      NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j =
    NatTrans.app s.π j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝ })
j : J
pt✝ : C
π✝ : (Functor.const J).obj pt✝ ⟶ Functor.mk toPrefunctor✝
⊢ (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) { pt := pt✝, π := π✝ } ≫
      NatTrans.app { pt := pt✝¹, π := NatTrans.mk app✝ }.π j =
    NatTrans.app { pt := pt✝, π := π✝ }.π j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cone K
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone K) (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cone (Functor.mk toPrefunctor✝)
h : IsLimit ((𝟭 C).mapCone c)
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
⊢ ∀ (s : Cone (Functor.mk toPrefunctor✝)) (m : s.pt ⟶ { pt := pt✝, π := NatTrans.mk app✝ }.pt),
    (∀ (j : J), m ≫ NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j = NatTrans.app s.π j) →
      m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := NatTrans.mk app✝ })
s : Cone (Functor.mk toPrefunctor✝)
m : s.pt ⟶ { pt := pt✝, π := NatTrans.mk app✝ }.pt
w : ∀ (j : J), m ≫ NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j = NatTrans.app s.π j
⊢ m = (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → ((Functor.const J).obj pt✝¹).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y = app✝¹ X ≫ (Functor.mk toPrefunctor✝).map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝¹, π := NatTrans.mk app✝¹ })
pt✝ : C
app✝ : (X : J) → ((Functor.const J).obj pt✝).obj X ⟶ (Functor.mk toPrefunctor✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((Functor.const J).obj pt✝).map f ≫ app✝ Y = app✝ X ≫ (Functor.mk toPrefunctor✝).map f
m : { pt := pt✝, π := NatTrans.mk app✝ }.pt ⟶ { pt := pt✝¹, π := NatTrans.mk app✝¹ }.pt
w :
  ∀ (j : J),
    m ≫ NatTrans.app { pt := pt✝¹, π := NatTrans.mk app✝¹ }.π j = NatTrans.app { pt := pt✝, π := NatTrans.mk app✝ }.π j
⊢ m =
    (fun s => IsLimit.lift h { pt := s.pt, π := NatTrans.mk fun j => NatTrans.app s.π j })
      { pt := pt✝, π := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (j : J),
    NatTrans.app c.ι j ≫ (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (j : J),
    NatTrans.app c.ι j ≫ (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (j : J),
    NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫
        (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
      NatTrans.app s.ι j
[PROOFSTEP]
intro s j
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
s : Cocone (Functor.mk toPrefunctor✝)
j : J
⊢ NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s =
    NatTrans.app s.ι j
[PROOFSTEP]
cases s
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝ })
j : J
pt✝ : C
ι✝ : Functor.mk toPrefunctor✝ ⟶ (Functor.const J).obj pt✝
⊢ NatTrans.app { pt := pt✝¹, ι := NatTrans.mk app✝ }.ι j ≫
      (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) { pt := pt✝, ι := ι✝ } =
    NatTrans.app { pt := pt✝, ι := ι✝ }.ι j
[PROOFSTEP]
exact h.fac _ j
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone K) (m : c.pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
cases K
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
c : Cocone (Functor.mk toPrefunctor✝)
h : IsColimit ((𝟭 C).mapCocone c)
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (m : c.pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app c.ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases c with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
⊢ ∀ (s : Cocone (Functor.mk toPrefunctor✝)) (m : { pt := pt✝, ι := NatTrans.mk app✝ }.pt ⟶ s.pt),
    (∀ (j : J), NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫ m = NatTrans.app s.ι j) →
      m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
intro s m w
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := NatTrans.mk app✝ })
s : Cocone (Functor.mk toPrefunctor✝)
m : { pt := pt✝, ι := NatTrans.mk app✝ }.pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j }) s
[PROOFSTEP]
rcases s with ⟨_, _, _⟩
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
toPrefunctor✝ : J ⥤q C
map_id✝ : ∀ (X : J), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
pt✝¹ : C
app✝¹ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝¹ Y = app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := NatTrans.mk app✝¹ })
pt✝ : C
app✝ : (X : J) → (Functor.mk toPrefunctor✝).obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y), (Functor.mk toPrefunctor✝).map f ≫ app✝ Y = app✝ X ≫ ((Functor.const J).obj pt✝).map f
m : { pt := pt✝¹, ι := NatTrans.mk app✝¹ }.pt ⟶ { pt := pt✝, ι := NatTrans.mk app✝ }.pt
w :
  ∀ (j : J),
    NatTrans.app { pt := pt✝¹, ι := NatTrans.mk app✝¹ }.ι j ≫ m = NatTrans.app { pt := pt✝, ι := NatTrans.mk app✝ }.ι j
⊢ m =
    (fun s => IsColimit.desc h { pt := s.pt, ι := NatTrans.mk fun j => NatTrans.app s.ι j })
      { pt := pt✝, ι := NatTrans.mk app✝ }
[PROOFSTEP]
exact h.uniq _ m w
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (F.mapCone c✝)
[PROOFSTEP]
apply isLimitOfReflects G
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (G.mapCone (F.mapCone c✝))
[PROOFSTEP]
apply isLimitOfPreserves (F ⋙ G) h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit c
[PROOFSTEP]
apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone ((Cones.postcompose h.inv).obj c))
[PROOFSTEP]
apply ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F : _) _).symm t).ofIsoLimit _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cones.postcompose h.inv).obj c)
[PROOFSTEP]
exact Cones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit c
[PROOFSTEP]
apply IsLimit.ofWhiskerEquivalence e
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor c)
[PROOFSTEP]
apply isLimitOfReflects F
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone (Cone.whisker e.functor c))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor (F.mapCone c))
[PROOFSTEP]
exact IsLimit.whiskerEquivalence t _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsLimit c
[PROOFSTEP]
suffices IsIso (IsLimit.lift (limit.isLimit F) c) from by apply IsLimit.ofPointIso (limit.isLimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso (IsLimit.lift (limit.isLimit F) c)
⊢ IsLimit c
[PROOFSTEP]
apply IsLimit.ofPointIso (limit.isLimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso (IsLimit.lift (limit.isLimit F) c)
[PROOFSTEP]
change IsIso ((Cones.forget _).map ((limit.isLimit F).liftConeMorphism c))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cones.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
[PROOFSTEP]
suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by apply (Cones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c)
⊢ IsIso ((Cones.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
[PROOFSTEP]
apply (Cones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c)
[PROOFSTEP]
suffices IsIso (Prefunctor.map (Cones.functoriality F G).toPrefunctor (IsLimit.liftConeMorphism (limit.isLimit F) c))
  from by apply isIso_of_reflects_iso _ (Cones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((Cones.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
⊢ IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c)
[PROOFSTEP]
apply isIso_of_reflects_iso _ (Cones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cones.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
[PROOFSTEP]
refine' t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (F.mapCocone c)
[PROOFSTEP]
apply isColimitOfReflects G
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (G.mapCocone (F.mapCocone c))
[PROOFSTEP]
apply isColimitOfPreserves (F ⋙ G) h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit c
[PROOFSTEP]
apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone ((Cocones.precompose h.hom).obj c))
[PROOFSTEP]
apply ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F : _) _).symm t).ofIsoColimit _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅ F.mapCocone ((Cocones.precompose h.hom).obj c)
[PROOFSTEP]
exact Cocones.ext (Iso.refl _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit c
[PROOFSTEP]
apply IsColimit.ofWhiskerEquivalence e
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor c)
[PROOFSTEP]
apply isColimitOfReflects F
[GOAL]
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G : D ⥤ E
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))
[PROOFSTEP]
exact IsColimit.whiskerEquivalence t _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsColimit c
[PROOFSTEP]
suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from by apply IsColimit.ofPointIso (colimit.isColimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso (IsColimit.desc (colimit.isColimit F) c)
⊢ IsColimit c
[PROOFSTEP]
apply IsColimit.ofPointIso (colimit.isColimit F)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso (IsColimit.desc (colimit.isColimit F) c)
[PROOFSTEP]
change IsIso ((Cocones.forget _).map ((colimit.isColimit F).descCoconeMorphism c))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((Cocones.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
[PROOFSTEP]
suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by apply (Cocones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
⊢ IsIso ((Cocones.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
[PROOFSTEP]
apply (Cocones.forget F).map_isIso _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
[PROOFSTEP]
suffices
  IsIso (Prefunctor.map (Cocones.functoriality F G).toPrefunctor (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
  from by apply isIso_of_reflects_iso _ (Cocones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((Cocones.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
⊢ IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
[PROOFSTEP]
apply isIso_of_reflects_iso _ (Cocones.functoriality F G)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F✝ : C ⥤ D
G✝ : D ⥤ E
F : J ⥤ C
G : C ⥤ D
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((Cocones.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
[PROOFSTEP]
refine' (isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cones.functoriality K F).preimage (IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s))
[PROOFSTEP]
apply fun s m => (Cones.functoriality K F).map_injective _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    (Cones.functoriality K F).map m =
      (Cones.functoriality K F).map
        ((Cones.functoriality K F).preimage (IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s)))
[PROOFSTEP]
intro s m
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cones.functoriality K F).map m =
    (Cones.functoriality K F).map
      ((Cones.functoriality K F).preimage (IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s)))
[PROOFSTEP]
rw [Functor.image_preimage]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cones.functoriality K F).map m = IsLimit.liftConeMorphism t ((Cones.functoriality K F).obj s)
[PROOFSTEP]
apply t.uniq_cone_morphism
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocones.functoriality K F).preimage (IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s))
[PROOFSTEP]
apply fun s m => (Cocones.functoriality K F).map_injective _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    (Cocones.functoriality K F).map m =
      (Cocones.functoriality K F).map
        ((Cocones.functoriality K F).preimage (IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s)))
[PROOFSTEP]
intro s m
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocones.functoriality K F).map m =
    (Cocones.functoriality K F).map
      ((Cocones.functoriality K F).preimage (IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s)))
[PROOFSTEP]
rw [Functor.image_preimage]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocones.functoriality K F).map m = IsColimit.descCoconeMorphism t ((Cocones.functoriality K F).obj s)
[PROOFSTEP]
apply t.uniq_cocone_morphism


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (NatTrans.app adj.unit (G.obj B)) ≫ F.map (G.map (NatTrans.app adj.counit B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))
[PROOFSTEP]
rw [← F.map_comp, adj.right_triangle_components]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))
[PROOFSTEP]
apply F.map_id
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
⊢ HasCoequalizer f g
[PROOFSTEP]
letI := IsReflexivePair.mk' r rf rg
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
this : IsReflexivePair f g := IsReflexivePair.mk' r rf rg
⊢ HasCoequalizer f g
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
⊢ HasEqualizer f g
[PROOFSTEP]
letI := IsCoreflexivePair.mk' r fr gr
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasCoreflexiveEqualizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
this : IsCoreflexivePair f g := IsCoreflexivePair.mk' r fr gr
⊢ HasEqualizer f g
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasCoequalizers C
A B : C
f g : A ⟶ B
x✝ : IsReflexivePair f g
⊢ HasCoequalizer f g
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : HasEqualizers C
A B : C
f g : A ⟶ B
x✝ : IsCoreflexivePair f g
⊢ HasEqualizer f g
[PROOFSTEP]
infer_instance