awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i j : h.J
⊢ h.t i j ≫ h.t j i = 𝟙 (Functor.obj (Opens.toTopCat (h.U i)) (h.V i j))
have 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))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i j : h.J
⊢ h.t j i ≫ h.t i j = 𝟙 (Functor.obj (Opens.toTopCat (h.U j)) (h.V j i))
have 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))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i j k : h.J
⊢ pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion'
have refine_1 : { 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)) } →
  { 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 (pullbackIsoProdSubtype _ _).hom ≫ ofHom ⟨?_, ?_⟩ ≫ (pullbackIsoProdSubtype _ _).inv
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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)) }
⊢ { 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)) }
have 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
Tactic: refine ⟨⟨⟨(h.t i j x.1.1).1, ?_⟩, h.t i j x.1.1⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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)) }
⊢ (↑((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
have 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')
                  sorry) :
              (↑((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'⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i : h.J
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i : h.J
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))
have 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
Tactic: rw [h.t_id]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
          (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
have 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))
            sorry)) :
      (↑(h.U k) : Type u))
    sorry =
  (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: convert! congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩) using 3
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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')
have 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))
                sorry)) :
          (↑(h.U k) : Type u))
        sorry) :
    (↑(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: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
⊢ Eq (α := (ofOpenSubsets U).diagram.left (i, j) ⟶ of α)
    ((ofOpenSubsets U).diagram.fst (i, j) ≫
      (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
          ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
        ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j)))
    ((ofOpenSubsets U).diagram.snd (i, j) ≫
      (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
          ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
        ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j)))
have w : ∀ (x : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)),
  Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).diagram.left (i, j)) (Y := of α)
            ((ofOpenSubsets U).diagram.fst (i, j) ≫
              (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
                  ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
                ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))) :
          (a : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).diagram.left (i, j)) (Y := of α)
            ((ofOpenSubsets U).diagram.snd (i, j) ≫
              (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
                  ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
                ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))) :
          (a : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x y : (↑(ofOpenSubsets U).glued : Type u)
e :
  Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        y :
      (↑(of α) : Type u))
⊢ x = y
have obtain : ∀ (i : (ofOpenSubsets U).J) (x : (↑(of α) : Type u)) (hx : x ∈ U i)
  (e :
    Eq (α := (↑(of α) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                  (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
                (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
              (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
            (↑(ofOpenSubsets U).glued : Type u)) :
        (↑(of α) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
          y :
        (↑(of α) : Type u))),
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
          (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
        (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) =
    y
Tactic: obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
Cleared hypotheses: x, e