C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, Multicoequalizer.π (diagram D) i y = x
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, ι D i y = x
delta CategoryTheory.GlueData.ι
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y = x
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, Multicoequalizer.π (diagram D) i y = x
simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]
case intro
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
⊢ ∃ i y, (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y = π D x'
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x : glued D
⊢ ∃ i y, (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y = x
rcases D.types_π_surjective x with ⟨x', rfl⟩
case intro
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
⊢ ∃ i y,
    (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y =
      π D
        ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv
          ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom x'))
case intro
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
⊢ ∃ i y, (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y = π D x'
rw [← show (colimit.isoColimitCocone (Types.coproductColimitCocone _)).inv _ = x' from
    ConcreteCategory.congr_hom
      (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']
case intro.mk
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ ∃ i_1 y_1,
    (Sigma.ι (diagram D).right i_1 ≫ Multicoequalizer.sigmaπ (diagram D)) y_1 =
      π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
case intro
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
⊢ ∃ i y,
    (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y =
      π D
        ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv
          ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom x'))
rcases(colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩
no goals
case intro.mk
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ ∃ i_1 y_1,
    (Sigma.ι (diagram D).right i_1 ≫ Multicoequalizer.sigmaπ (diagram D)) y_1 =
      π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
exact ⟨i, y, by
  simp [← Multicoequalizer.ι_sigmaπ, -Multicoequalizer.ι_sigmaπ]
  rfl ⟩
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ Multicoequalizer.sigmaπ (diagram D) (Sigma.ι D.U i y) =
    π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ (Sigma.ι (diagram D).right i ≫ Multicoequalizer.sigmaπ (diagram D)) y =
    π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
simp [← Multicoequalizer.ι_sigmaπ, -Multicoequalizer.ι_sigmaπ]
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D✝ : GlueData C
D : GlueData (Type u_1)
x' : sigmaOpens D
i : D.J
y : U D i
⊢ Multicoequalizer.sigmaπ (diagram D) (Sigma.ι D.U i y) =
    π D ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv { fst := i, snd := y })
rfl