-- Mathlib/Topology/Gluing.lean
theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) :
    𝖣.ι i x = 𝖣.ι j y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Proof state:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
rw [←
  show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]

Result:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel (((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) ⟨i, x⟩) ⟨j, y⟩

Proof state:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ ∀ (a b : ↑(∐ D.U)),
    Function.Coequalizer.Rel (⇑(ConcreteCategory.hom D.diagram.fstSigmaMap))
        (⇑(ConcreteCategory.hom D.diagram.sndSigmaMap)) a b →
      InvImage D.Rel (⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) a b

Tactic:
rintro _ _ ⟨x⟩

Result:
case mp.intro
D : GlueData
i j : D.J
x✝ : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x✝ =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
x : ↑(∐ D.diagram.left)
⊢ InvImage D.Rel (⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((ConcreteCategory.hom D.diagram.fstSigmaMap) x)
    ((ConcreteCategory.hom D.diagram.sndSigmaMap) x)

Proof state:
case mp.intro.intro.mk.mk
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (Sigma.desc fun b => D.diagram.fst b ≫ Sigma.ι D.diagram.right ((MultispanShape.prod D.J).fst b)))
        ((ConcreteCategory.hom (sigmaIsoSigma D.diagram.left).inv) ⟨(i, j), y⟩)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (Sigma.desc fun b => D.diagram.snd b ≫ Sigma.ι D.diagram.right ((MultispanShape.prod D.J).snd b)))
        ((ConcreteCategory.hom (sigmaIsoSigma D.diagram.left).inv) ⟨(i, j), y⟩)))

Tactic:
rw [sigmaIsoSigma_inv_apply]

Result:
case mp.intro.intro.mk.mk
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (Sigma.desc fun b => D.diagram.fst b ≫ Sigma.ι D.diagram.right ((MultispanShape.prod D.J).fst b)))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (Sigma.desc fun b => D.diagram.snd b ≫ Sigma.ι D.diagram.right ((MultispanShape.prod D.J).snd b)))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))

Proof state:
case mpr.intro.intro
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = (ConcreteCategory.hom (D.f i j)) z
e₂ :
  (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) =
    (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z)
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) =
    (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z))

Tactic:
rw [D.glue_condition_apply]

Result:
no goals