awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (x : (↑(h.U i) : Type u)) (hx : x ∈ h.V i j) (hx' : x ∈ h.V i k),
    (↑((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))
            (↑(Subtype.mk (p :=
                    fun
                      (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)))
                    (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
                      Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
                    ⋯) :
                (↑((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
⊢ (↑((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

Tactic:
rcases x with ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩

Premises used: rfl
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ (↑((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))
          (↑(Subtype.mk (p :=
                  fun
                    (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)))
                  (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
                    Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
                  ⋯) :
              (↑((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

Tactic:
h.t_inter _ ⟨x, hx⟩ hx'

Premises used: Set.Mem, Subtype.mk, TopCat.GlueData.MkCore.t_inter
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ (↑((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))
          (↑(Subtype.mk (p :=
                  fun
                    (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)))
                  (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
                    Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
                  ⋯) :
              (↑((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

Tactic:
exact h.t_inter _ ⟨x, hx⟩ hx'

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

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

Tactic:
rw [h.t_id]

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

Tactic:
rfl
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t k i) :
            (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
              (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.t i k) :
              (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
                (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
            (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx'))) :
      (↑(h.U i) : Type u)) =
    (↑(Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx') : (↑(h.U i) : Type u))

Tactic:
congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩)

Premises used: TopCat.GlueData.MkCore.t_inv, Subtype.mk, congr_arg, Subtype.val
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
h₁ :
  Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
      (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.t j k) :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
            (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
              (↑((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))
                    (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                (↑(h.U j) : Type u))
              ⋯)) :
        (↑(h.U k) : Type u))
      ⋯ =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t i k) :
        (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
          (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
      (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
⊢ (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t k i) :
            (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
              (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
          (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (h.t j k) :
                    (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                      (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                  (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                    (↑((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))
                          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                      (↑(h.U j) : Type u))
                    ⋯)) :
              (↑(h.U k) : Type u))
            ⋯)) :
      (↑(h.U i) : Type u)) =
    x

Tactic:
convert! congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩) using 3

Premises used: TopCat.GlueData.MkCore.t_inv, Subtype.mk, congr_arg, Subtype.val
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
      (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.t j k) :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
            (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
              (↑((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))
                    (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                (↑(h.U j) : Type u))
              ⋯)) :
        (↑(h.U k) : Type u))
      ⋯ =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t i k) :
        (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
          (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
      (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')

Tactic:
Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
h₁ :
  (↑(Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
          (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.t j k) :
                  (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                    (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                  (↑((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))
                        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                    (↑(h.U j) : Type u))
                  ⋯)) :
            (↑(h.U k) : Type u))
          ⋯) :
      (↑(h.U k) : Type u)) =
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.t i k) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
              (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')) :
      (↑(h.U k) : Type u))
⊢ Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
      (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.t j k) :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
            (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
              (↑((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))
                    (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                (↑(h.U j) : Type u))
              ⋯)) :
        (↑(h.U k) : Type u))
      ⋯ =
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t i k) :
        (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
          (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
      (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ (↑(Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
          (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.t j k) :
                  (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                    (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                  (↑((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))
                        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                    (↑(h.U j) : Type u))
                  ⋯)) :
            (↑(h.U k) : Type u))
          ⋯) :
      (↑(h.U k) : Type u)) =
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.t i k) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
              (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')) :
      (↑(h.U k) : Type u))

Tactic:
h.cocycle i j k ⟨x, hx⟩ hx'

Premises used: Subtype.mk, TopCat.GlueData.MkCore.cocycle
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ (↑(Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
          (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.t j k) :
                  (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                    (↑((Opens.toTopCat (h.U k)).obj (h.V k j)) : Type u))
                (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
                  (↑((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))
                        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                    (↑(h.U j) : Type u))
                  ⋯)) :
            (↑(h.U k) : Type u))
          ⋯) :
      (↑(h.U k) : Type u)) =
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.t i k) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) →
              (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u))
          (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')) :
      (↑(h.U k) : Type u))

Tactic:
exact h.cocycle i j k ⟨x, hx⟩ hx'

Premises used: Subtype.mk, TopCat.GlueData.MkCore.cocycle
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i j : J
⊢ Continuous (Y := ↥(Functor.obj (Opens.map (U j).inclusion') (U i)))
    fun (x : ↥(Functor.obj (Opens.map (U i).inclusion') (U j))) ↦
    Subtype.mk (p := fun (x : (↑(Functor.obj (Opens.toTopCat (of α)) (U j)) : Type u)) ↦
      Membership.mem (γ := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U j)) : Type u))
        (Functor.obj (Opens.map (U j).inclusion') (U i)) x)
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j)
        (↑(↑x : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) : (↑(of α) : Type u)) ⋯)
      ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ Eq.{u + 1} (α := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
    (Functor.obj (Opens.map (U i).inclusion') (U i)) ⊤

Tactic:
simp
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
x :
  (↑(Functor.obj (C := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
        (Opens.toTopCat (Functor.obj (Opens.toTopCat (of α)) (U i))) (Functor.obj (Opens.map (U i).inclusion') (U i))) :
    Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (ofHom
            {
              toFun := fun (x : ↥(Functor.obj (Opens.map (U i).inclusion') (U i))) ↦
                Subtype.mk (p := fun (x : (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u)) ↦
                  Membership.mem (γ := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
                    (Functor.obj (Opens.map (U i).inclusion') (U i)) x)
                  (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i)
                    (↑(↑x : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) : (↑(of α) : Type u)) ⋯)
                  ⋯,
              continuous_toFun := ⋯ :
              C(↥(Functor.obj (Opens.map (U i).inclusion') (U i)),
                ↥(Functor.obj (Opens.map (U i).inclusion') (U i))) }) :
        (a :
            (↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i))) :
              Type u)) →
          (↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i))) :
            Type u))
      x =
    id x

Tactic:
rfl