-- Mathlib/Topology/Gluing.lean
theorem eqvGen_of_π_eq
    -- Porting note: was `{x y : ∐ D.U} (h : 𝖣.π x = 𝖣.π y)`
    {x y : sigmaObj (β := D.toGlueData.J) (C := TopCat) D.toGlueData.U}
    (h : 𝖣.π x = 𝖣.π y) :
    Relation.EqvGen
      (Function.Coequalizer.Rel 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap) x y

Proof state:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom
      ((ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y) =
    (⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
        (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom)
      y

Tactic:
simp

Result:
no goals

Proof state:
D : GlueData
x y : ↑(∐ D.U)
h : (ConcreteCategory.hom D.π) x = (ConcreteCategory.hom D.π) y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
delta GlueData.π Multicoequalizer.sigmaπ at h

Result:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom
        (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv))
      x =
    (ConcreteCategory.hom
        (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv))
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Proof state:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ colimit.ι diagram one x = colimit.ι diagram one y

Tactic:
dsimp only [coequalizer.π] at h

Result:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ colimit.ι diagram one x = colimit.ι diagram one y

Proof state:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
have : colimit.ι diagram one x = colimit.ι diagram one y := by
  dsimp only [coequalizer.π] at h
  rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_coe, types_comp_apply]
  erw [h]
  simp

Result:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this : colimit.ι diagram one x = colimit.ι diagram one y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Proof state:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this✝ : colimit.ι diagram one x = colimit.ι diagram one y
this :
  (colimit.ι diagram one ≫
        colim.map (diagramIsoParallelPair diagram).hom ≫
          (colimit.isoColimitCocone
              (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                (diagram.map WalkingParallelPairHom.right))).hom)
      x =
    (colimit.ι diagram one ≫
        colim.map (diagramIsoParallelPair diagram).hom ≫
          (colimit.isoColimitCocone
              (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                (diagram.map WalkingParallelPairHom.right))).hom)
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
rw [colimit.ι_map_assoc, diagramIsoParallelPair_hom_app, eqToHom_refl,
  colimit.isoColimitCocone_ι_hom, types_comp_apply, types_id_apply, types_comp_apply,
  types_id_apply] at this

Result:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this✝ : colimit.ι diagram one x = colimit.ι diagram one y
this :
  (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
              (diagram.map WalkingParallelPairHom.right)).cocone.ι.app
      one x =
    (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
              (diagram.map WalkingParallelPairHom.right)).cocone.ι.app
      one y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Proof state:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this✝ : colimit.ι diagram one x = colimit.ι diagram one y
this :
  (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
              (diagram.map WalkingParallelPairHom.right)).cocone.ι.app
      one x =
    (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
              (diagram.map WalkingParallelPairHom.right)).cocone.ι.app
      one y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
exact Quot.eq.1 this

Result:
no goals