-- 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
        (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

Tactic:
replace h : coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap x =
    coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap y :=
  (TopCat.mono_iff_injective (Multicoequalizer.isoCoequalizer 𝖣.diagram).inv).mp
  inferInstance h

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
⊢ 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 (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)) x) =
    (⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
        (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom)
      y

Tactic:
erw [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
⊢ (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

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
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
let diagram := parallelPair 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap ⋙ forget _

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
⊢ 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
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
have :
  (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ =
    (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ :=
  (congr_arg
      (colim.map (diagramIsoParallelPair diagram).hom ≫
        (colimit.isoColimitCocone (Types.coequalizerColimit _ _)).hom)
      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 :
  (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

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
⊢ colimit.ι diagram one x = colimit.ι diagram one y

Tactic:
rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_coe, types_comp_apply]

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
⊢ (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom
      ((ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x) =
    (⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
        (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom)
      y