-- 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 (((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) ⟨i, x⟩) ⟨j, y⟩

Tactic:
rw [←
  show _ = Sigma.mk j y 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⟩)
    (((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) ⟨j, y⟩)

Proof state:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y → D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
delta GlueData.ι

Result:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) x =
      (ConcreteCategory.hom (Multicoequalizer.π D.diagram j)) y →
    D.Rel ⟨i, x⟩ ⟨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 = x
e₂ : (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) = y
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
rw [← e₁, ← e₂] at *

Result:
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))

Proof state:
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)

Tactic:
obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
  (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x

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))
⊢ InvImage D.Rel (⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom))
    ((ConcreteCategory.hom D.diagram.fstSigmaMap)
      ((ConcreteCategory.hom (sigmaIsoSigma D.diagram.left).inv) ⟨(i, j), y⟩))
    ((ConcreteCategory.hom D.diagram.sndSigmaMap)
      ((ConcreteCategory.hom (sigmaIsoSigma D.diagram.left).inv) ⟨(i, j), y⟩))

Proof state:
case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩ → (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
rintro ⟨z, e₁, e₂⟩

Result:
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, x⟩.fst ⟨j, y⟩.fst)) z = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨j, y⟩.fst)) z) = ⟨j, y⟩.snd
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι 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 (((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) ⟨i, x⟩)
    (((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) ⟨j, y⟩)

Tactic:
change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _

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
⊢ InvImage D.Rel (⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((sigmaIsoSigma D.U).inv.hom' ⟨i, x⟩)
    ((sigmaIsoSigma D.U).inv.hom' ⟨j, y⟩)

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

Tactic:
erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc,
  ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc]

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
        ((Cofan.mk (∐ D.diagram.right) fun b =>
                  D.diagram.fst b ≫ Sigma.ι D.diagram.right ((MultispanShape.prod D.J).fst b)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (∐ D.diagram.right) fun b =>
                  D.diagram.snd b ≫ Sigma.ι D.diagram.right ((MultispanShape.prod D.J).snd b)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)

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 ⟨(MultispanShape.prod D.J).fst { as := (i, j) }.as, (D.diagram.fst { as := (i, j) }.as).hom' y⟩
    ⟨(MultispanShape.prod D.J).snd { as := (i, j) }.as, (D.diagram.snd { as := (i, j) }.as).hom' y⟩

Tactic:
exact ⟨y, ⟨rfl, rfl⟩⟩

Result:
no goals