awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
⊢ 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)
have 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))
Tactic: rw [←
      show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
⊢ 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))
have 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))
Tactic: change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
have 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
Tactic: refine Relation.EqvGen.mono ?_ (D.eqvGen_of_π_eq h :)
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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
⊢ x = y
have 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))
Tactic: rw [← e₁, ← e₂]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
⊢ 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)))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
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
have h : 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : (↑D.glued : Type u)
h :
  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
⊢ 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
have h₁ : 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 →
  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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : (↑D.glued : Type u)
x₁ : (↑(D.U i) : Type u)
eq₁ :
  (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₁ =
    x
x₂ : (↑(D.U j) : Type u)
eq₂ :
  (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₂ =
    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
have h : ∀
  (y :
    (↑(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)) j x₂))) :
      Type u))
  (e₁ :
    Eq (α :=
      (↑(D.U
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
              (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              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)) j x₂)))
              (D.f
                (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)) j x₂))) :
            (a : (↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst)) : Type u)) → (↑(D.U ⟨i, x₁⟩.fst) : Type u))
          y :
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))) :
          Type u))
      (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁) :
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))) :
          Type u))),
  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
Tactic: obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x_1 : (↑D.glued : Type u)
x : (↑(D.V (i, j)) : Type u)
hx :
  (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 =
    x_1
⊢ 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_1
have h : (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))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            x :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u)) =
  x_1
Tactic: refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩