C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
let E := (forget C).mapCocone D
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
let hE : IsColimit E := isColimitOfPreserves _ hD
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
let T : E ≅ G := hE.uniqueUpToIso hG
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
case a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ TX.hom ((forget C).map (D.ι.app i) x) = TX.hom ((forget C).map (D.ι.app j) y)
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
apply (show Function.Bijective TX.hom by
  rw [← isIso_iff_bijective]
  apply IsIso.of_iso).1
case a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
case a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ TX.hom ((forget C).map (D.ι.app i) x) = TX.hom ((forget C).map (D.ι.app j) y)
change (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
case a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ G.ι.app i x = G.ι.app j y
case a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
erw [T.hom.w, T.hom.w]
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
⊢ G.ι.app i x = G.ι.app j y
case a
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ G.ι.app i x = G.ι.app j y
obtain ⟨k, f, g, h⟩ := h
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
this : G.ι.app i x = G.ι.app k ((forget C).map (F.map f) x)
⊢ G.ι.app i x = G.ι.app j y
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
⊢ G.ι.app i x = G.ι.app j y
have : G.ι.app i x = (G.ι.app k (F.map f x) : G.pt) := Quot.sound ⟨f, rfl⟩
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
this : G.ι.app i x = G.ι.app k ((forget C).map (F.map f) x)
⊢ G.ι.app k ((forget C).map (F.map g) y) = G.ι.app j y
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
this : G.ι.app i x = G.ι.app k ((forget C).map (F.map f) x)
⊢ G.ι.app i x = G.ι.app j y
rw [this, h]
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
this : G.ι.app i x = G.ι.app k ((forget C).map (F.map f) x)
⊢ G.ι.app j y = G.ι.app k ((forget C).map (F.map g) y)
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
this : G.ι.app i x = G.ι.app k ((forget C).map (F.map f) x)
⊢ G.ι.app k ((forget C).map (F.map g) y) = G.ι.app j y
symm
no goals
case a.intro.intro.intro
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : (forget C).map (F.map f) x = (forget C).map (F.map g) y
this : G.ι.app i x = G.ι.app k ((forget C).map (F.map f) x)
⊢ G.ι.app j y = G.ι.app k ((forget C).map (F.map g) y)
exact Quot.sound ⟨g, rfl⟩
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ IsIso TX.hom
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ Function.Bijective TX.hom
rw [← isIso_iff_bijective]
no goals
C : Type u
inst✝³ : Category C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ IsIso TX.hom
apply IsIso.of_iso