awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Gluing
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
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
⊢ 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
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x₁ : (↑(D.U i) : Type u)
x₂ : (↑(D.U j) : Type u)
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))
eq₂ :
  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.ι j) :
          (a : (↑(D.U j) : 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))
        x₁ :
      (↑D.glued : Type u))
⊢ 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.f i j ≫ D.ι i) :
          (a : (↑(D.V (i, j)) : Type u)) → (↑D.glued : Type u))
        y :
      (↑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))

Tactic:
simp [e₁]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x₁ : (↑(D.U i) : Type u)
x₂ : (↑(D.U j) : Type u)
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))
eq₂ :
  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.ι j) :
          (a : (↑(D.U j) : 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))
        x₁ :
      (↑D.glued : Type u))
⊢ Membership.mem (α := (↑D.glued : Type u)) (γ := 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)))
    ((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))

Tactic:
exact ⟨y, by simp [e₁]⟩
-- Module: Mathlib.Topology.Gluing
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

Tactic:
⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩

Premises used: CategoryTheory.GlueData.t, CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, TopCat.GlueData.toGlueData, CategoryTheory.GlueData.f, Set.inter, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.Gluing
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
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
⊢ 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

Tactic:
refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
-- Module: Mathlib.Topology.Gluing
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
h :
  (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))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f i j) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
          x :
        (↑(D.U i) : Type u)) =
    x_1
⊢ (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:
rw [D.glue_condition_apply]

Premises used: TopCat.GlueData.toGlueData, CategoryTheory.GlueData.glue_condition_apply
-- Module: Mathlib.Topology.Gluing
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
⊢ (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))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f i j) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
          x :
        (↑(D.U i) : Type u)) =
    x_1

Tactic:
hx
-- Module: Mathlib.Topology.Gluing
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
⊢ (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))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f i j) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
          x :
        (↑(D.U i) : Type u)) =
    x_1

Tactic:
exact hx
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
h :
  ∀ (x : (↑(D.V (j, i)) : Type u)),
    Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
        (Set.preimage (β := (↑(D.U j) : 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))
          (Set.preimage (β := (↑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.ι 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)
                    (Y := D.glued) (D.ι i)) :
                (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ''
              U)))
        x ↔
      Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t j i ≫ D.f i j)) :
            (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
          U)
        x
⊢ Eq (α := Set (↑(D.V (j, i)) : Type u))
    (Set.preimage (β := (↑(D.U j) : 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))
      (Set.preimage (β := (↑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.ι 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) (Y :=
                D.glued) (D.ι i)) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ''
          U)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t j i ≫ D.f i j)) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U)

Tactic:
ext x
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
x : (↑(D.V (j, i)) : Type u)
rw :
  Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
    (Set.preimage (β := (↑(D.U i) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t j i ≫ D.f i j)) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U)))
    x
| Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t j i ≫ D.f i j)) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U)
    x

Tactic:
rw [← Set.preimage_image_eq U (D.ι_injective _)]

Premises used: Set.preimage_image_eq, TopCat.GlueData.ι_injective
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
x : (↑(D.V (j, i)) : Type u)
h :
  Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
      (Set.preimage (β := (↑(D.U j) : 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))
        (Set.preimage (β := (↑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.ι 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)
                  (Y := D.glued) (D.ι i)) :
              (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ''
            U)))
      x ↔
    Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
      (Set.preimage (β := (↑(D.U i) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t j i ≫ D.f i j)) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u))
        (Set.preimage (β := (↑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))
          ((⇑(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)) ''
            U)))
      x
⊢ Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
      (Set.preimage (β := (↑(D.U j) : 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))
        (Set.preimage (β := (↑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.ι 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)
                  (Y := D.glued) (D.ι i)) :
              (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ''
            U)))
      x ↔
    Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t j i ≫ D.f i j)) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
        U)
      x

Tactic:
conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]

Premises used: Set.preimage_image_eq, TopCat.GlueData.ι_injective
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
x : (↑(D.V (j, i)) : Type u)
⊢ Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
      (Set.preimage (β := (↑(D.U j) : 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))
        (Set.preimage (β := (↑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.ι 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)
                  (Y := D.glued) (D.ι i)) :
              (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ''
            U)))
      x ↔
    Membership.mem (γ := Set (↑(D.V (j, i)) : Type u))
      (Set.preimage (β := (↑(D.U i) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t j i ≫ D.f i j)) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u))
        (Set.preimage (β := (↑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))
          ((⇑(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)) ''
            U)))
      x

Tactic:
simp