awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
U : Opens (↑(D.U i) : Type u)
rw :
  ∀ (i_1 : D.J),
    IsOpen (X := (↑(D.U i_1) : 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_1)) :
          (a : (↑(D.U i_1) : 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 (↑(D.U i) : Type u))))
⊢ IsOpen (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)) ''
      (↑U : Set (↑(D.U i) : Type u)))

Tactic:
rw [isOpen_iff]

Premises used: TopCat.GlueData.isOpen_iff
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
U : Opens (↑(D.U i) : Type u)
j : D.J
rw :
  IsOpen (X := (↑(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))
      ((⇑(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 : Set (↑(D.U i) : Type u))))
⊢ IsOpen (X := (↑(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 (↑(D.U i) : Type u))))

Tactic:
rw [preimage_image_eq_image]

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

Tactic:
apply (D.f_open _ _).isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, TopCat.GlueData.f_open
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
U : Opens (↑(D.U i) : Type u)
j : D.J
a : IsOpen (↑U : Set (↑(D.U i) : Type u))
⊢ IsOpen (X := (↑(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 : Set (↑(D.U i) : Type u)))

Tactic:
apply (D.t j i ≫ D.f i j).hom.continuous_toFun.isOpen_preimage

Premises used: CategoryTheory.GlueData.t, TopCat.GlueData.toGlueData, CategoryTheory.GlueData.f, ContinuousMap.continuous_toFun, TopCat.Hom.hom, CategoryTheory.CategoryStruct.comp, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
U : Opens (↑(D.U i) : Type u)
j : D.J
⊢ IsOpen (↑U : Set (↑(D.U i) : Type u))

Tactic:
U.isOpen

Premises used: TopologicalSpace.Opens.isOpen
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
U : Opens (↑(D.U i) : Type u)
j : D.J
⊢ IsOpen (↑U : Set (↑(D.U i) : Type u))

Tactic:
exact U.isOpen

Premises used: TopologicalSpace.Opens.isOpen
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
⊢ IsOpenEmbedding (X := (↑(D.U i) : 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))

Tactic:
.of_continuous_injective_isOpenMap (𝖣.ι i).hom.continuous_toFun (D.ι_injective i) fun U h =>
    D.open_image_open i ⟨U, h⟩

Premises used: TopCat.GlueData.open_image_open, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, TopCat.GlueData.toGlueData, CategoryTheory.GlueData.ι, TopologicalSpace.Opens.mk, ContinuousMap.continuous_toFun, TopCat.Hom.hom, TopCat.GlueData.ι_injective
-- Module: Mathlib.Topology.Gluing
Goal:
h : MkCore
i j : h.J
x : ↥(h.V j i)
refine_2 :
  ∀
    (this :
      Eq.{u_1 + 1} (α := (↑(h.U j) : Type u_1))
        (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                  (h.t i j) :
                (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
                  (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
              (Subtype.mk (p := fun (x : (↑(h.U i) : Type u_1)) ↦ x ∈ h.V i j)
                (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          carrier) (h.t j i) :
                        (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
                          (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
                      x) :
                  (↑(h.U i) : Type u_1))
                ⋯)) :
          (↑(h.U j) : Type u_1))
        (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                  (h.t j j) :
                (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j j)) : Type u_1)) →
                  (↑((Opens.toTopCat (h.U j)).obj (h.V j j)) : Type u_1))
              (Subtype.mk (p := fun (x : (↑(h.U j) : Type u_1)) ↦ x ∈ h.V j j) (↑x : (↑(h.U j) : Type u_1)) ⋯)) :
          (↑(h.U j) : Type u_1))),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (h.t i j) :
          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
            (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (h.t j i) :
            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
              (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
          x) =
      x
refine_1 : (↑x : (↑(h.U j) : Type u_1)) ∈ h.V j j
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
          (h.t i j) :
        (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
          (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (h.t j i) :
          (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
        x) =
    x

Tactic:
have := h.cocycle j i j x ?_
-- Module: Mathlib.Topology.Gluing
Goal:
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  Eq.{u_1 + 1} (α := (↑(h.U j) : Type u_1))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (h.t i j) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u_1)) ↦ x ∈ h.V i j)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (h.t j i) :
                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
                  x) :
              (↑(h.U i) : Type u_1))
            ⋯)) :
      (↑(h.U j) : Type u_1))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (h.t j j) :
            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j j)) : Type u_1)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j j)) : Type u_1))
          (Subtype.mk (p := fun (x : (↑(h.U j) : Type u_1)) ↦ x ∈ h.V j j) (↑x : (↑(h.U j) : Type u_1)) ⋯)) :
      (↑(h.U j) : Type u_1))
⊢ (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (h.t i j) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u_1)) ↦ x ∈ h.V i j)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (h.t j i) :
                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
                  x) :
              (↑(h.U i) : Type u_1))
            ⋯)) :
      (↑(h.U j) : Type u_1)) =
    (↑(id (Subtype.mk (p := fun (x : (↑(h.U j) : Type u_1)) ↦ x ∈ h.V j j) (↑x : (↑(h.U j) : Type u_1)) ⋯)) :
      (↑(h.U j) : Type u_1))

Tactic:
rw [h.t_id] at this

Premises used: TopCat.GlueData.MkCore.t_id
-- Module: Mathlib.Topology.Gluing
Goal:
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (h.t i j) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u_1)) ↦ x ∈ h.V i j)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (h.t j i) :
                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
                  x) :
              (↑(h.U i) : Type u_1))
            ⋯)) :
      (↑(h.U j) : Type u_1)) =
    (↑(id (Subtype.mk (p := fun (x : (↑(h.U j) : Type u_1)) ↦ x ∈ h.V j j) (↑x : (↑(h.U j) : Type u_1)) ⋯)) :
      (↑(h.U j) : Type u_1))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
          (h.t i j) :
        (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
          (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
      (Subtype.mk (p := fun (x : (↑(h.U i) : Type u_1)) ↦ x ∈ h.V i j)
        (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                  (h.t j i) :
                (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
                  (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
              x) :
          (↑(h.U i) : Type u_1))
        ⋯) =
    x

Tactic:
Subtype.ext this

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Gluing
Goal:
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (h.t i j) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u_1)) ↦ x ∈ h.V i j)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (h.t j i) :
                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
                  x) :
              (↑(h.U i) : Type u_1))
            ⋯)) :
      (↑(h.U j) : Type u_1)) =
    (↑(id (Subtype.mk (p := fun (x : (↑(h.U j) : Type u_1)) ↦ x ∈ h.V j j) (↑x : (↑(h.U j) : Type u_1)) ⋯)) :
      (↑(h.U j) : Type u_1))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
          (h.t i j) :
        (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1)) →
          (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (h.t j i) :
          (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u_1)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u_1))
        x) =
    x

Tactic:
convert! Subtype.ext this

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Gluing
Goal:
h : MkCore
i j : h.J
x : ↥(h.V j i)
refine_1 : Membership.mem (γ := Opens (↑(h.U j) : Type u_1)) ⊤ (↑x : (↑(h.U j) : Type u_1))
⊢ (↑x : (↑(h.U j) : Type u_1)) ∈ h.V j j

Tactic:
rw [h.V_id]

Premises used: TopCat.GlueData.MkCore.V_id
-- Module: Mathlib.Topology.Gluing
Goal:
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ Membership.mem (γ := Opens (↑(h.U j) : Type u_1)) ⊤ (↑x : (↑(h.U j) : Type u_1))

Tactic:
trivial
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
h₁ :
  h.t i j ≫ h.t j i = 𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) ∧
    h.t j i ≫ h.t i j = 𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))
⊢ IsIso (h.t i j)

Tactic:
use h.t j i

Premises used: TopCat.GlueData.MkCore.t
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
h₁ : h.t i j ≫ h.t j i = 𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j))
h₂ : h.t j i ≫ h.t i j = 𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))
⊢ h.t i j ≫ h.t j i = 𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) ∧
    h.t j i ≫ h.t i j = 𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))

Tactic:
constructor
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
h₁ :
  ∀ (x : (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u)),
    Eq (α := (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.t i j ≫ h.t j i) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
              (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u))
          x :
        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j))) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
              (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u))
          x :
        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
⊢ h.t i j ≫ h.t j i = 𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j))

Tactic:
ext1
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
h₁ :
  ∀ (x : (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u)),
    Eq (α := (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.t j i ≫ h.t i j) :
            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
          x :
        (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))) :
            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
          x :
        (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u))
⊢ h.t j i ≫ h.t i j = 𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))

Tactic:
ext1
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
x : (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u)
⊢ Eq (α := (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (h.t i j ≫ h.t j i) :
          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u))
        x :
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j))) :
          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u))
        x :
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))

Tactic:
h.t_inv _ _ _

Premises used: TopCat.GlueData.MkCore.t_inv
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
x : (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u)
⊢ Eq (α := (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (h.t j i ≫ h.t i j) :
          (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) →
            (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
        x :
      (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))) :
          (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) →
            (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
        x :
      (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u))

Tactic:
h.t_inv _ _ _

Premises used: TopCat.GlueData.MkCore.t_inv
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j : h.J
x : (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u)
⊢ Eq (α := (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (h.t i j ≫ h.t j i) :
          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u))
        x :
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j))) :
          (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u))
        x :
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u))

Tactic:
exacts [h.t_inv _ _ _, h.t_inv _ _ _]

Premises used: TopCat.GlueData.MkCore.t_inv
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x :
  { p :
    (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
    Eq (α := (↑(h.U i) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.V i j).inclusion' :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
          p.1 :
        (↑(h.U i) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.V i k).inclusion' :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
          p.2 :
        (↑(h.U i) : Type u)) }
refine_1 :
  (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t i j) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
          (↑x :
              (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)).1) :
      (↑(h.U j) : Type u)) ∈
    h.V j k
⊢ { p :
    (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
      (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u) //
    Eq (α := (↑(h.U j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.V j k).inclusion' :
            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
          p.1 :
        (↑(h.U j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.V j i).inclusion' :
            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
          p.2 :
        (↑(h.U j) : Type u)) }

Tactic:
refine ⟨⟨⟨(h.t i j x.1.1).1, ?_⟩, h.t i j x.1.1⟩, rfl⟩