awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
mp :
  D.Rel
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) :
        (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) :
        (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y))
⊢ D.Rel
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) :
        (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)

Tactic:
rw [←
      show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
mp :
  InvImage (α := (↑(∐ D.U) : Type u)) D.Rel
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (sigmaIsoSigma D.U).hom) :
        (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x) :
      (↑(∐ D.U) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y) :
      (↑(∐ D.U) : Type u))
⊢ D.Rel
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) :
        (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) :
        (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y))

Tactic:
change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
mp :
  Relation.EqvGen (α := (↑(∐ D.U) : Type u))
    (InvImage D.Rel
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (sigmaIsoSigma D.U).hom) :
          (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (↑(∐ D.U) : Type u) → (↑(∐ D.U) : Type u) → Prop)
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x) :
      (↑(∐ D.U) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y) :
      (↑(∐ D.U) : Type u))
⊢ InvImage (α := (↑(∐ D.U) : Type u)) D.Rel
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (sigmaIsoSigma D.U).hom) :
        (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x) :
      (↑(∐ D.U) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y) :
      (↑(∐ D.U) : Type u))

Tactic:
rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]

Premises used: TopCat.GlueData.rel_equiv, InvImage.equivalence, Equivalence.eqvGen_iff
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
⊢ Relation.EqvGen (α := (↑(∐ D.U) : Type u))
    (InvImage D.Rel
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (sigmaIsoSigma D.U).hom) :
          (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (↑(∐ D.U) : Type u) → (↑(∐ D.U) : Type u) → Prop)
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x) :
      (↑(∐ D.U) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y) :
      (↑(∐ D.U) : Type u))

Tactic:
Relation.EqvGen.mono ?_ (D.eqvGen_of_π_eq h :)

Premises used: TopCat.GlueData.eqvGen_of_π_eq, Relation.EqvGen.mono
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
mp :
  ∀ (a b : (↑(∐ D.U) : Type u)),
    Function.Coequalizer.Rel (α := (↑(∐ D.diagram.left) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap) :
          (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.sndSigmaMap) :
          (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
        a b →
      InvImage D.Rel
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (sigmaIsoSigma D.U).hom) :
          (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
        a b
⊢ Relation.EqvGen (α := (↑(∐ D.U) : Type u))
    (InvImage D.Rel
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (sigmaIsoSigma D.U).hom) :
          (a : (↑(∐ D.U) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) :
      (↑(∐ D.U) : Type u) → (↑(∐ D.U) : Type u) → Prop)
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x) :
      (↑(∐ D.U) : Type u))
    (((sigmaIsoSigma D.U).inv.hom' : (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(∐ D.U) : Type u))
        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y) :
      (↑(∐ D.U) : Type u))

Tactic:
refine Relation.EqvGen.mono ?_ (D.eqvGen_of_π_eq h :)

Premises used: TopCat.GlueData.eqvGen_of_π_eq, Relation.EqvGen.mono
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i_1 j_1 : D.J
x : (↑(D.U i_1) : Type u)
y_1 : (↑(D.U j_1) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i_1) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j_1)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j_1) : Type u)) → (↑D.glued : Type u))
        y_1 :
      (↑D.glued : Type u))
i j : D.J
y : (↑(D.diagram.left (i, j)) : Type u)
⊢ D.Rel
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
      ((MultispanShape.prod D.J).fst { as := (i, j) : Discrete (MultispanShape.prod D.J).L }.as)
      ((Hom.hom' (D.diagram.fst { as := (i, j) : Discrete (MultispanShape.prod D.J).L }.as) :
          (a : (↑(D.diagram.left { as := (i, j) }.as) : Type u)) →
            (↑(D.diagram.right ((MultispanShape.prod D.J).fst { as := (i, j) }.as)) : Type u))
        y))
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) ((MultispanShape.prod D.J).snd { as := (i, j) }.as)
      ((Hom.hom' (D.diagram.snd { as := (i, j) }.as) :
          (a : (↑(D.diagram.left { as := (i, j) }.as) : Type u)) →
            (↑(D.diagram.right ((MultispanShape.prod D.J).snd { as := (i, j) }.as)) : Type u))
        y))

Tactic:
⟨y, ⟨rfl, rfl⟩⟩

Premises used: And.intro, TopCat.GlueData.Rel, Exists.intro, rfl
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i_1 j_1 : D.J
x : (↑(D.U i_1) : Type u)
y_1 : (↑(D.U j_1) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U i_1) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right j_1)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j_1) : Type u)) → (↑D.glued : Type u))
        y_1 :
      (↑D.glued : Type u))
i j : D.J
y : (↑(D.diagram.left (i, j)) : Type u)
⊢ D.Rel
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
      ((MultispanShape.prod D.J).fst { as := (i, j) : Discrete (MultispanShape.prod D.J).L }.as)
      ((Hom.hom' (D.diagram.fst { as := (i, j) : Discrete (MultispanShape.prod D.J).L }.as) :
          (a : (↑(D.diagram.left { as := (i, j) }.as) : Type u)) →
            (↑(D.diagram.right ((MultispanShape.prod D.J).fst { as := (i, j) }.as)) : Type u))
        y))
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) ((MultispanShape.prod D.J).snd { as := (i, j) }.as)
      ((Hom.hom' (D.diagram.snd { as := (i, j) }.as) :
          (a : (↑(D.diagram.left { as := (i, j) }.as) : Type u)) →
            (↑(D.diagram.right ((MultispanShape.prod D.J).snd { as := (i, j) }.as)) : Type u))
        y))

Tactic:
exact ⟨y, ⟨rfl, rfl⟩⟩
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
x y : (↑(D.U i) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
w :
  (↑(D.V
        (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x),
          Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
    Type u)
e₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
        (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
      w =
    x
e₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
        (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t i i) :
            (a : (↑(D.V (i, i)) : Type u)) → (↑(D.V (i, i)) : Type u))
          w :
        (↑(D.V (i, i)) : Type u)) =
    y
rw :
  Eq (α := (↑(D.U i) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
          (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
        w :
      (↑(D.U i) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
          (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i i) :
              (a : (↑(D.V (i, i)) : Type u)) → (↑(D.V (i, i)) : Type u))
            w :
          (↑(D.V (i, i)) : Type u)) :
      (↑(D.U i) : Type u))
⊢ x = y

Tactic:
rw [← e₁, ← e₂]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
x y : (↑(D.U i) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
w :
  (↑(D.V
        (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x),
          Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
    Type u)
e₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
        (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
      w =
    x
e₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
        (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t i i) :
            (a : (↑(D.V (i, i)) : Type u)) → (↑(D.V (i, i)) : Type u))
          w :
        (↑(D.V (i, i)) : Type u)) =
    y
⊢ Eq (α := (↑(D.U i) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
          (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
        w :
      (↑(D.U i) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i i) :
          (a : (↑(D.V (i, i)) : Type u)) → (↑(D.U i) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i i) :
              (a : (↑(D.V (i, i)) : Type u)) → (↑(D.V (i, i)) : Type u))
            w :
          (↑(D.V (i, i)) : Type u)) :
      (↑(D.U i) : Type u))

Tactic:
simp
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
⊢ Mono (Y := D.glued) (D.ι i)

Tactic:
(TopCat.mono_iff_injective _).mpr (D.ι_injective _)

Premises used: Iff.mpr, TopCat.mono_iff_injective, TopCat.GlueData.ι_injective
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
h :
  ∀ (x : (↑D.glued : Type u)),
    Membership.mem (γ := Set (↑D.glued : Type u))
        (Set.range (ι := (↑(D.U i) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (Y := D.glued) (D.ι i)) :
              (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ∩
          Set.range (ι := (↑(D.U j) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (Y := D.glued) (D.ι j)) :
              (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u)))
        x ↔
      Membership.mem (γ := Set (↑D.glued : Type u))
        (Set.range (ι := (↑(D.V (i, j)) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued) (D.f i j ≫ D.ι i)) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑D.glued : Type u)))
        x
⊢ Eq (α := Set (↑D.glued : Type u))
    (Set.range (ι := (↑(D.U i) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.ι i)) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ∩
      Set.range (ι := (↑(D.U j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.ι j)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u)))
    (Set.range (ι := (↑(D.V (i, j)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.f i j ≫ D.ι i)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑D.glued : Type u)))

Tactic:
ext x