C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
⊢ ∃ i y, F.map (ι D i) y = x
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
⊢ ∃ i y, F.map (ι D i) y = x
let e := D.gluedIso F
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : ι (mapGlueData D F) i y = e.hom x
⊢ ∃ i y, F.map (ι D i) y = x
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
⊢ ∃ i y, F.map (ι D i) y = x
obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : e.inv (ι (mapGlueData D F) i y) = e.inv (e.hom x)
⊢ ∃ i y, F.map (ι D i) y = x
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : ι (mapGlueData D F) i y = e.hom x
⊢ ∃ i y, F.map (ι D i) y = x
replace eq := congr_arg e.inv eq
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : (ι (mapGlueData D F) i ≫ e.inv) y = (e.hom ≫ e.inv) x
⊢ ∃ i y, F.map (ι D i) y = x
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : e.inv (ι (mapGlueData D F) i y) = e.inv (e.hom x)
⊢ ∃ i y, F.map (ι D i) y = x
change ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : F.map (ι D i) y = 𝟙 (F.obj (glued D)) x
⊢ ∃ i y, F.map (ι D i) y = x
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : (ι (mapGlueData D F) i ≫ e.inv) y = (e.hom ≫ e.inv) x
⊢ ∃ i y, F.map (ι D i) y = x
rw [e.hom_inv_id, D.ι_gluedIso_inv] at eq
no goals
case intro.intro
C : Type u₁
inst✝⁵ : Category C
C' : Type u₂
inst✝⁴ : Category C'
D : GlueData C
F✝ : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F✝
inst✝³ : HasMulticoequalizer (diagram D)
inst✝² : PreservesColimit (MultispanIndex.multispan (diagram D)) F✝
F : C ⥤ Type v
inst✝¹ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
inst✝ : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
x : F.obj (glued D)
e : F.obj (glued D) ≅ glued (mapGlueData D F) := gluedIso D F
i : (mapGlueData D F).J
y : U (mapGlueData D F) i
eq : F.map (ι D i) y = 𝟙 (F.obj (glued D)) x
⊢ ∃ i y, F.map (ι D i) y = x
exact ⟨i, y, eq⟩