awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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
have 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
Tactic: rw [D.glue_condition_apply]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
⊢ Eq (α := Set (↑(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))
      (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.V (j, i)) : 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)))
have rw : Eq (α := Set (↑(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))
    (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.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))
    (Set.image (α := (↑(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 (j, i)) : 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)))))
Tactic: rw [← Set.preimage_image_eq (Set.range (D.f j i)) (D.ι_injective j), ← Set.image_univ, ←
    Set.image_univ, ← Set.image_comp, ← coe_comp, Set.image_univ, Set.image_univ, ← image_inter,
    Set.preimage_range_inter]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
⊢ 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)
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
    ((⇑(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
have 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
Tactic: rw [← Set.preimage_image_eq U (D.ι_injective _)]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
      ((⇑(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
have 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
Tactic: conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]
-- Lean 4 proof step from Mathlib.Topology.Gluing (hypothesis)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
⊢ Eq (α := Set (↑(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))
    (Set.image (α := (↑(D.V (j, i)) : 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 j i ≫ D.f i j)) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
        U))
have this : 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: have : D.f _ _ ⁻¹' 𝖣.ι j ⁻¹' 𝖣.ι i '' U = (D.t j i ≫ D.f _ _) ⁻¹' U := by
    ext x
    conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]
    simp
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
this :
  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)
⊢ Eq (α := Set (↑(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) ∩
      Set.range (ι := (↑(D.V (j, i)) : 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))
have a : Subset (α := Set (↑(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))
  (Set.range (ι := (↑(D.V (j, i)) : 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)))
Tactic: apply Set.inter_eq_self_of_subset_left
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
this :
  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)
⊢ Subset (α := Set (↑(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))
    (Set.range (ι := (↑(D.V (j, i)) : 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)))
have a : Subset (α := Set (↑(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))
  (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))
    (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))))
Tactic: rw [← D.preimage_range i j]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
⊢ Eq (α := Set (↑(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))
    (Set.image (α := (↑(D.V (i, j)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t i j ≫ D.f j i)) :
        (a : (↑(D.V (i, j)) : 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.f i j)) :
          (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
        U))
have h : Eq (α := Set (↑(D.U j) : Type u))
  (Set.image (α := (↑(D.V (i, j)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (D.t i j ≫ D.f j i)) :
      (a : (↑(D.V (i, j)) : 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.f i j)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U))
  (Set.image (α := (↑(D.V (j, i)) : 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 j i ≫ D.f i j)) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U))
Tactic: convert! D.preimage_image_eq_image i j U using 1
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
⊢ Eq (α := Set (↑(D.U j) : Type u))
    (Set.image (α := (↑(D.V (i, j)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t i j ≫ D.f j i)) :
        (a : (↑(D.V (i, j)) : 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.f i j)) :
          (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
        U))
    (Set.image (α := (↑(D.V (j, i)) : 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 j i ≫ D.f i j)) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
        U))
have h : Eq (α := Set (↑(D.U j) : Type u))
  (Set.image (α := (↑(D.V (j, i)) : 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.image (α := (↑(D.V (i, 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))
      ((⇑(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)) ⁻¹'
        U)))
  (Set.image (α := (↑(D.V (j, i)) : 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))
    (Function.comp (β := (↑(D.V (i, j)) : 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))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t j i)) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u)) ⁻¹'
      U))
Tactic: rw [coe_comp, coe_comp, Set.image_comp]