-- Mathlib/CategoryTheory/GlueData.lean
theorem types_ι_jointly_surjective (D : GlueData (Type v)) (x : D.glued) :
    ∃ (i : _) (y : D.U i), D.ι i y = x

Proof state:
case intro
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ i y,
    (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y =
      D.π
        ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv
          ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom x'))

Tactic:
rcases (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩

Result:
case intro.mk
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ ∃ i_1 y_1,
    (Sigma.ι D.diagram.right i_1 ≫ Multicoequalizer.sigmaπ D.diagram) y_1 =
      D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ⟨i, y⟩)

Proof state:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, Multicoequalizer.π D.diagram i y = x

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]

Result:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = x

Proof state:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y =
    D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ⟨i, y⟩)

Tactic:
simp [← Multicoequalizer.ι_sigmaπ]

Result:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ Multicoequalizer.sigmaπ D.diagram (Sigma.ι D.U i y) =
    D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ⟨i, y⟩)

Proof state:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, D.ι i y = x

Tactic:
delta CategoryTheory.GlueData.ι

Result:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, Multicoequalizer.π D.diagram i y = x

Proof state:
case intro.mk
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ ∃ i_1 y_1,
    (Sigma.ι D.diagram.right i_1 ≫ Multicoequalizer.sigmaπ D.diagram) y_1 =
      D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ⟨i, y⟩)

Tactic:
exact ⟨i, y, by
  simp [← Multicoequalizer.ι_sigmaπ]
  rfl ⟩

Result:
no goals

Proof state:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = x

Tactic:
rcases D.types_π_surjective x with ⟨x', rfl⟩

Result:
case intro
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = D.π x'

Proof state:
case intro
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = D.π x'

Tactic:
rw [← show (colimit.isoColimitCocone (Types.coproductColimitCocone.{v, v} _)).inv _ = x' from
    ConcreteCategory.congr_hom
      (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']

Result:
case intro
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ i y,
    (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y =
      D.π
        ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv
          ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom x'))

Proof state:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ Multicoequalizer.sigmaπ D.diagram (Sigma.ι D.U i y) =
    D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ⟨i, y⟩)

Tactic:
rfl

Result:
no goals