awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Gluing
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)

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
-- Module: Mathlib.Topology.Gluing
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)
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))))
⊢ 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:
rw [← D.preimage_range i j]

Premises used: TopCat.GlueData.preimage_range
-- Module: Mathlib.Topology.Gluing
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.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:
Set.preimage_mono (Set.image_subset_range _ _)

Premises used: Set.image_subset_range, Set.preimage_mono
-- Module: Mathlib.Topology.Gluing
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.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:
exact Set.preimage_mono (Set.image_subset_range _ _)

Premises used: Set.image_subset_range, Set.preimage_mono
-- Module: Mathlib.Topology.Gluing
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))

Tactic:
D.preimage_image_eq_image i j U

Premises used: TopCat.GlueData.preimage_image_eq_image
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
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))
⊢ 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))

Tactic:
convert! D.preimage_image_eq_image i j U using 1

Premises used: TopCat.GlueData.preimage_image_eq_image
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
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))
⊢ 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:
rw [coe_comp, coe_comp, Set.image_comp]

Premises used: Set.image_comp, TopCat.coe_comp
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
h :
  Eq (α := Set (↑(D.V (j, i)) : 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))
    (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)
⊢ 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:
congr! 1
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
h :
  Eq (α := Set (↑(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)) ⁻¹'
      U)
    ((fun (x : (↑(D.V (i, j)) : Type u)) ↦
        Function.comp (α := (↑(D.V (j, i)) : Type u)) (β := (↑(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)) :
            (a : (↑(D.V (j, i)) : Type u)) → (↑(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))
              x :
            (↑(D.V (j, i)) : Type u))) ⁻¹'
      U)
h₁ :
  Function.Bijective (α := (↑(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.t i j)) :
      (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
⊢ Eq (α := Set (↑(D.V (j, i)) : 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))
    (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 [← Set.eq_preimage_iff_image_eq, Set.preimage_preimage]

Premises used: Set.preimage_preimage, Set.eq_preimage_iff_image_eq
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
h :
  Eq (α := Set (↑(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)) ⁻¹'
      U)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t i j ≫ D.t j i ≫ D.f i j)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U)
⊢ Eq (α := Set (↑(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)) ⁻¹'
      U)
    ((fun (x : (↑(D.V (i, j)) : Type u)) ↦
        Function.comp (α := (↑(D.V (j, i)) : Type u)) (β := (↑(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)) :
            (a : (↑(D.V (j, i)) : Type u)) → (↑(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))
              x :
            (↑(D.V (j, i)) : Type u))) ⁻¹'
      U)

Tactic:
change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _

Premises used: CategoryTheory.GlueData.t, TopCat.GlueData.toGlueData, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
h h₁ :
  Eq (α := Set (↑(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)) ⁻¹'
      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)
⊢ Eq (α := Set (↑(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)) ⁻¹'
      U)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t i j ≫ D.t j i ≫ D.f i j)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U)

Tactic:
rw [𝖣.t_inv_assoc]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
h :
  IsIso (X := (↑(D.V (i, j)) : Type u)) (Y := (↑(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 i j)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u)))
⊢ Function.Bijective (α := (↑(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.t i j)) :
      (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))

Tactic:
rw [bijective_iff_isIso_ofHom]

Premises used: CategoryTheory.bijective_iff_isIso_ofHom
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
⊢ IsIso (X := (↑(D.V (i, j)) : Type u)) (Y := (↑(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 i j)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u)))

Tactic:
apply (forget TopCat).map_isIso

Premises used: CategoryTheory.forget, CategoryTheory.Functor.map_isIso, TopCat