C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) 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)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) 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)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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)
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) 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)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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)
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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)
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) 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)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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)
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) 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)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : TX.hom ((forget C).map (D.ι.app i) x) = TX.hom ((forget C).map (D.ι.app j) y)
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : (forget C).map (D.ι.app i) x = (forget C).map (D.ι.app j) 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
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
replace h := congr_arg TX.hom h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : TX.hom ((forget C).map (D.ι.app i) x) = TX.hom ((forget C).map (D.ι.app j) y)
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
change (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y at h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : G.ι.app i x = G.ι.app j y
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
erw [T.hom.w, T.hom.w] at h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : G.ι.app i x = G.ι.app j y
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
replace h := Quot.exact _ h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
⊢ ∀ (a b : (j : J) × (forget C).obj (F.obj j)),
    EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b →
      ∃ k f g, (forget C).map (F.map f) a.snd = (forget C).map (F.map g) b.snd
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
suffices
  ∀ (a b : Σj, F.obj j) (_ : EqvGen (Limits.Types.Quot.Rel.{v, v} (F ⋙ forget C)) a b),
    ∃ (k : _)(f : a.1 ⟶ k)(g : b.1 ⟶ k), F.map f a.2 = F.map g b.2
  by exact this ⟨i, x⟩ ⟨j, y⟩ h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b : (j : J) × (forget C).obj (F.obj j)
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b
⊢ ∃ k f g, (forget C).map (F.map f) a.snd = (forget C).map (F.map g) b.snd
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
⊢ ∀ (a b : (j : J) × (forget C).obj (F.obj j)),
    EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b →
      ∃ k f g, (forget C).map (F.map f) a.snd = (forget C).map (F.map g) b.snd
intro a b h
case rel
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : Types.Quot.Rel (F ⋙ forget C) x✝ y✝
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd

case refl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) x✝.snd

case symm
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) x✝.snd

case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b : (j : J) × (forget C).obj (F.obj j)
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b
⊢ ∃ k f g, (forget C).map (F.map f) a.snd = (forget C).map (F.map g) b.snd
induction h
case refl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) x✝.snd

case symm
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) x✝.snd

case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case rel
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : Types.Quot.Rel (F ⋙ forget C) x✝ y✝
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd

case refl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) x✝.snd

case symm
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) x✝.snd

case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case rel x y hh =>
  obtain ⟨e, he⟩ := hh
  use y.1, e, 𝟙 _
  simpa using he.symm
case symm
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) x✝.snd

case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case refl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) x✝.snd

case symm
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) x✝.snd

case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case refl x =>
  exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case symm
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) x✝.snd

case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case symm x y _ hh =>
  obtain ⟨k, f, g, hh⟩ := hh
  exact ⟨k, g, f, hh.symm⟩
no goals
case trans
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) y✝.snd
a_ih✝ : ∃ k f g, (forget C).map (F.map f) y✝.snd = (forget C).map (F.map g) z✝.snd
⊢ ∃ k f g, (forget C).map (F.map f) x✝.snd = (forget C).map (F.map g) z✝.snd
case trans x y z _ _ hh1 hh2 =>
  obtain ⟨k1, f1, g1, h1⟩ := hh1
  obtain ⟨k2, f2, g2, h2⟩ := hh2
  let k0 : J := IsFiltered.max k1 k2
  let e1 : k1 ⟶ k0 := IsFiltered.leftToMax _ _
  let e2 : k2 ⟶ k0 := IsFiltered.rightToMax _ _
  let k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
  let e : k0 ⟶ k := IsFiltered.coeqHom _ _
  use k, f1 ≫ e1 ≫ e, g2 ≫ e2 ≫ e
  simp only [F.map_comp, comp_apply, h1, ← h2]
  simp only [← comp_apply, ← F.map_comp]
  rw [IsFiltered.coeq_condition]
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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
this :
  ∀ (a b : (j : J) × (forget C).obj (F.obj j)),
    EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b →
      ∃ k f g, (forget C).map (F.map f) a.snd = (forget C).map (F.map g) b.snd
⊢ ∃ k f g, (forget C).map (F.map f) x = (forget C).map (F.map g) y
exact this ⟨i, x⟩ ⟨j, y⟩ h
case intro
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
e : x.fst ⟶ y.fst
he : y.snd = (F ⋙ forget C).map e x.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
hh : Types.Quot.Rel (F ⋙ forget C) x y
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
obtain ⟨e, he⟩ := hh
case intro
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
e : x.fst ⟶ y.fst
he : y.snd = (F ⋙ forget C).map e x.snd
⊢ (forget C).map (F.map e) x.snd = (forget C).map (F.map (𝟙 y.fst)) y.snd
case intro
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
e : x.fst ⟶ y.fst
he : y.snd = (F ⋙ forget C).map e x.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
use y.1, e, 𝟙 _
no goals
case intro
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
e : x.fst ⟶ y.fst
he : y.snd = (F ⋙ forget C).map e x.snd
⊢ (forget C).map (F.map e) x.snd = (forget C).map (F.map (𝟙 y.fst)) y.snd
simpa using he.symm
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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y }
a b x : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) x.snd
exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
case 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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hh : (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
⊢ ∃ k f g, (forget C).map (F.map f) y.snd = (forget C).map (F.map g) x.snd
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
hh : ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
⊢ ∃ k f g, (forget C).map (F.map f) y.snd = (forget C).map (F.map g) x.snd
obtain ⟨k, f, g, hh⟩ := hh
no goals
case 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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hh : (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
⊢ ∃ k f g, (forget C).map (F.map f) y.snd = (forget C).map (F.map g) x.snd
exact ⟨k, g, f, hh.symm⟩
case 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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
hh2 : ∃ k f g, (forget C).map (F.map f) y.snd = (forget C).map (F.map g) z.snd
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
hh1 : ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) y.snd
hh2 : ∃ k f g, (forget C).map (F.map f) y.snd = (forget C).map (F.map g) z.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
obtain ⟨k1, f1, g1, h1⟩ := hh1
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
case 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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
hh2 : ∃ k f g, (forget C).map (F.map f) y.snd = (forget C).map (F.map g) z.snd
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
obtain ⟨k2, f2, g2, h2⟩ := hh2
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
let k0 : J := IsFiltered.max k1 k2
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
let e1 : k1 ⟶ k0 := IsFiltered.leftToMax _ _
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
let e2 : k2 ⟶ k0 := IsFiltered.rightToMax _ _
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
let k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
let e : k0 ⟶ k := IsFiltered.coeqHom _ _
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ (forget C).map (F.map (f1 ≫ e1 ≫ e)) x.snd = (forget C).map (F.map (g2 ≫ e2 ≫ e)) z.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ ∃ k f g, (forget C).map (F.map f) x.snd = (forget C).map (F.map g) z.snd
use k, f1 ≫ e1 ≫ e, g2 ≫ e2 ≫ e
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ (forget C).map (F.map (IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      ((forget C).map (F.map (IsFiltered.leftToMax k1 k2)) ((forget C).map (F.map g1) y.snd)) =
    (forget C).map (F.map (IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      ((forget C).map (F.map (IsFiltered.rightToMax k1 k2)) ((forget C).map (F.map f2) y.snd))
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ (forget C).map (F.map (f1 ≫ e1 ≫ e)) x.snd = (forget C).map (F.map (g2 ≫ e2 ≫ e)) z.snd
simp only [F.map_comp, comp_apply, h1, ← h2]
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ (forget C).map
      (F.map
        ((g1 ≫ IsFiltered.leftToMax k1 k2) ≫
          IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      y.snd =
    (forget C).map
      (F.map
        ((f2 ≫ IsFiltered.rightToMax k1 k2) ≫
          IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      y.snd
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ (forget C).map (F.map (IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      ((forget C).map (F.map (IsFiltered.leftToMax k1 k2)) ((forget C).map (F.map g1) y.snd)) =
    (forget C).map (F.map (IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      ((forget C).map (F.map (IsFiltered.rightToMax k1 k2)) ((forget C).map (F.map f2) y.snd))
simp only [← comp_apply, ← F.map_comp]
no goals
case intro.intro.intro.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)
inst✝ : IsFiltered J
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
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : (forget C).map (F.map f1) x.snd = (forget C).map (F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : (forget C).map (F.map f2) y.snd = (forget C).map (F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ (forget C).map
      (F.map
        ((g1 ≫ IsFiltered.leftToMax k1 k2) ≫
          IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      y.snd =
    (forget C).map
      (F.map
        ((f2 ≫ IsFiltered.rightToMax k1 k2) ≫
          IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      y.snd
rw [IsFiltered.coeq_condition]