-- Mathlib/Topology/Gluing.lean
theorem rel_equiv : Equivalence D.Rel :=
  ⟨fun x => ⟨inv (D.f _ _) x.2, IsIso.inv_hom_id_apply (D.f x.fst x.fst) _,
    -- Use `elementwise_of%` elaborator instead of `IsIso.inv_hom_id_apply` to work around
    -- `ConcreteCategory`/`HasForget` mismatch:
    by simp [elementwise_of% IsIso.inv_hom_id (D.f x.fst x.fst)]⟩, by
    rintro a b ⟨x, e₁, e₂⟩
    exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩, by
    rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ ⟨x, e₁, e₂⟩
    rintro ⟨y, e₃, e₄⟩
    let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩
    have eq₁ : (D.t j i) ((pullback.fst _ _ : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x

Proof state:
case mk.mk.mk.intro.intro.intro.intro
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩

Result:
case mk.mk.mk.intro.intro.intro.intro
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Proof state:
case mk.mk.mk.intro.intro.intro.intro
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k))
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
use (pullback.fst _ _ : _ ⟶ D.V (i, k)) (D.t' _ _ _ z)

Result:
case h
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k))
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨k, c⟩.fst))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      ⟨i, a⟩.snd ∧
    (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨i, a⟩.fst))
        ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨k, c⟩.fst))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      ⟨k, c⟩.snd

Proof state:
D : GlueData
a b : (i : D.J) × ↑(D.U i)
x : ↑(D.V (a.fst, b.fst))
e₁ : (ConcreteCategory.hom (D.f a.fst b.fst)) x = a.snd
e₂ : (ConcreteCategory.hom (D.f b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x) = b.snd
⊢ (ConcreteCategory.hom (D.f a.fst b.fst))
      ((ConcreteCategory.hom (D.t b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x)) =
    a.snd

Tactic:
rw [← e₁, D.t_inv_apply]

Result:
no goals

Proof state:
case h
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
⊢ (ConcreteCategory.hom (D.f i k))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      (ConcreteCategory.hom (D.f i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z)) ∧
    (ConcreteCategory.hom (D.f k i))
        ((ConcreteCategory.hom (D.t i k))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      (ConcreteCategory.hom (D.f k j))
        ((ConcreteCategory.hom (D.t j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z))

Tactic:
have h₁ : D.t' j i k ≫ pullback.fst _ _ ≫ D.f i k = pullback.fst _ _ ≫ D.t j i ≫ D.f i j := by
  rw [← 𝖣.t_fac_assoc]; congr 1; exact pullback.condition

Result:
case h
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (ConcreteCategory.hom (D.f i k))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      (ConcreteCategory.hom (D.f i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z)) ∧
    (ConcreteCategory.hom (D.f k i))
        ((ConcreteCategory.hom (D.t i k))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      (ConcreteCategory.hom (D.f k j))
        ((ConcreteCategory.hom (D.t j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z))