awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
x : (↑X : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
hx :
  x ∈
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f) :
            (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
          t,
      is_open' := hU : Opens (↑X : Type u) }
⊢ x ∈
    (Opens.map f).obj
      (hf.functorObj
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU : Opens (↑X : Type u) })

Tactic:
exact Opens.mem_sSup.mpr ⟨⟨_, ht⟩, rfl, hx⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_sSup, TopologicalSpace.Opens.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑X : Type u)
x : (↑X : Type u)
rw : x ∈ (Opens.map f).obj (hf.functorObj U)
| x ∈ U

Tactic:
rw [← hf.map_functorObj U]

Premises used: Topology.IsInducing.map_functorObj
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑X : Type u)
x : (↑X : Type u)
conv_rhs :
  Membership.mem (α := (↑Y : Type u)) (hf.functorObj U)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u)) ↔
    x ∈ (Opens.map f).obj (hf.functorObj U)
⊢ Membership.mem (α := (↑Y : Type u)) (hf.functorObj U)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u)) ↔
    x ∈ U

Tactic:
conv_rhs => rw [← hf.map_functorObj U]

Premises used: Topology.IsInducing.map_functorObj
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑X : Type u)
x : (↑X : Type u)
⊢ Membership.mem (α := (↑Y : Type u)) (hf.functorObj U)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u)) ↔
    x ∈ (Opens.map f).obj (hf.functorObj U)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑X : Type u)
V : Opens (↑Y : Type u)
obtain :
  ∀ (U : Set (↑X : Type u)) (hU : IsOpen U),
    V ≤ hf.functorObj { carrier := U, is_open' := hU } ↔ (Opens.map f).obj V ≤ { carrier := U, is_open' := hU }
⊢ V ≤ hf.functorObj U ↔ (Opens.map f).obj V ≤ U

Tactic:
obtain ⟨U, hU⟩ := U
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
U : Set (↑X : Type u)
hU : IsOpen U
obtain :
  ∀ (t : Set (↑Y : Type u)) (ht : IsOpen t)
    (hU :
      IsOpen (X := (↑X : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f) :
            (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
          t)),
    V ≤
        hf.functorObj
          {
            carrier :=
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f) :
                  (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
                t,
            is_open' := hU } ↔
      (Opens.map f).obj V ≤
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU }
⊢ V ≤ hf.functorObj { carrier := U, is_open' := hU } ↔ (Opens.map f).obj V ≤ { carrier := U, is_open' := hU }

Tactic:
obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
mp :
  V ≤
      hf.functorObj
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU } →
    (Opens.map f).obj V ≤
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU }
mpr :
  (Opens.map f).obj V ≤
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU } →
    V ≤
      hf.functorObj
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU }
⊢ V ≤
      hf.functorObj
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU } ↔
    (Opens.map f).obj V ≤
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU }

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
⊢ V ≤
      hf.functorObj
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU } →
    (Opens.map f).obj V ≤
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU }

Tactic:
fun i x hx ↦ (hf.mem_functorObj_iff ((Opens.map f).obj ⟨t, ht⟩)).mp (i hx)

Premises used: Set.Mem, Topology.IsInducing.mem_functorObj_iff, TopologicalSpace.Opens.mk, Iff.mp, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
⊢ V ≤
      hf.functorObj
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU } →
    (Opens.map f).obj V ≤
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU }

Tactic:
exact fun i x hx ↦ (hf.mem_functorObj_iff ((Opens.map f).obj ⟨t, ht⟩)).mp (i hx)

Premises used: Topology.IsInducing.mem_functorObj_iff, TopologicalSpace.Opens.mk, Iff.mp, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
h :
  (Opens.map f).obj V ≤
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f) :
            (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
          t,
      is_open' := hU }
x : (↑Y : Type u)
hx : x ∈ V
⊢ x ∈
    hf.functorObj
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU : Opens (↑X : Type u) }

Tactic:
Opens.mem_sSup.mpr ⟨⟨_, V.2.union ht⟩, Opens.ext ?_, Set.mem_union_left t hx⟩

Premises used: Iff.mpr, Set.Mem, TopologicalSpace.Opens.ext, IsOpen.union, TopologicalSpace.Opens.mem_sSup, TopologicalSpace.Opens.mk, And.intro, Exists.intro, Set.mem_union_left, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
h :
  (Opens.map f).obj V ≤
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f) :
            (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
          t,
      is_open' := hU }
x : (↑Y : Type u)
hx : x ∈ V
mpr :
  (↑((Opens.map f).obj { carrier := V.carrier ∪ t, is_open' := ⋯ : Opens (↑Y : Type u) }) : Set (↑X : Type u)) =
    (↑{
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU : Opens (↑X : Type u) } :
      Set (↑X : Type u))
⊢ x ∈
    hf.functorObj
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f) :
              (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
            t,
        is_open' := hU : Opens (↑X : Type u) }

Tactic:
refine Opens.mem_sSup.mpr ⟨⟨_, V.2.union ht⟩, Opens.ext ?_, Set.mem_union_left t hx⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.ext, IsOpen.union, TopologicalSpace.Opens.mem_sSup, TopologicalSpace.Opens.mk, And.intro, Exists.intro, Set.mem_union_left, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
h :
  (Opens.map f).obj V ≤
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f) :
            (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
          t,
      is_open' := hU }
x : (↑Y : Type u)
hx : x ∈ V
mpr :
  Eq (α := Set (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f) :
          (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
        (↑V : Set (↑Y : Type u)) ∪
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f) :
          (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
        t)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
⊢ (↑((Opens.map f).obj { carrier := V.carrier ∪ t, is_open' := ⋯ : Opens (↑Y : Type u) }) : Set (↑X : Type u)) =
    (↑{
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f) :
                (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
              t,
          is_open' := hU : Opens (↑X : Type u) } :
      Set (↑X : Type u))

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsInducing (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
V : Opens (↑Y : Type u)
t : Set (↑Y : Type u)
ht : IsOpen t
hU :
  IsOpen (X := (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
h :
  (Opens.map f).obj V ≤
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f) :
            (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
          t,
      is_open' := hU }
x : (↑Y : Type u)
hx : x ∈ V
mpr mpr₁ mpr₂ mpr₃ :
  Subset (α := Set (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      (↑V : Set (↑Y : Type u)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)
⊢ Eq (α := Set (↑X : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f) :
          (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
        (↑V : Set (↑Y : Type u)) ∪
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f) :
          (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
        t)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ⁻¹'
      t)

Tactic:
rwa [Set.union_eq_right]

Premises used: Set.union_eq_right
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
h : (↑(⋯.functor.obj ⊤) : Set (↑X : Type u)) = (↑U : Set (↑X : Type u))
⊢ ⋯.functor.obj ⊤ = U

Tactic:
ext1
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (↑(⋯.functor.obj ⊤) : Set (↑X : Type u)) = (↑U : Set (↑X : Type u))

Tactic:
Set.image_univ.trans Subtype.range_coe

Premises used: Set.image_univ, Set.Mem, Set.univ, setOf, Subtype.range_coe, Set.image, Eq.trans
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (↑(⋯.functor.obj ⊤) : Set (↑X : Type u)) = (↑U : Set (↑X : Type u))

Tactic:
exact Set.image_univ.trans Subtype.range_coe

Premises used: Set.image_univ, Subtype.range_coe, Eq.trans
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
h : (↑((map U.inclusion').obj U) : Set (↑((toTopCat X).obj U) : Type u)) = (↑⊤ : Set (↑((toTopCat X).obj U) : Type u))
⊢ (map U.inclusion').obj U = ⊤

Tactic:
ext1
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (↑((map U.inclusion').obj U) : Set (↑((toTopCat X).obj U) : Type u)) = (↑⊤ : Set (↑((toTopCat X).obj U) : Type u))

Tactic:
Subtype.coe_preimage_self _

Premises used: Set.Mem, Set.univ, Subtype.coe_preimage_self, setOf, Set.preimage
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (↑((map U.inclusion').obj U) : Set (↑((toTopCat X).obj U) : Type u)) = (↑⊤ : Set (↑((toTopCat X).obj U) : Type u))

Tactic:
exact Subtype.coe_preimage_self _

Premises used: Subtype.coe_preimage_self
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (map U.inclusion' ⋙ ⋯.functor).obj U = Functor.obj (𝟭 (Opens (↑X : Type u))) U

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ ⋯.adjunction.counit.app U = eqToHom ⋯

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
⊢ IsOpenEmbedding.functor ⋯ = map (inclusionTopIso X).inv

Tactic:
CategoryTheory.Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
refine_1 :
  ∀ (X_1 : Opens (↑((toTopCat X).obj ⊤) : Type u_1)),
    Functor.obj (IsOpenEmbedding.functor ⋯) X_1 = (map (inclusionTopIso X).inv).obj X_1
refine_2 :
  ∀ (X_1 Y : Opens (↑((toTopCat X).obj ⊤) : Type u_1)) (f : X_1 ⟶ Y),
    Eq (α := Functor.obj (IsOpenEmbedding.functor ⋯) X_1 ⟶ Functor.obj (IsOpenEmbedding.functor ⋯) Y)
      (CategoryTheory.Functor.map (IsOpenEmbedding.functor ⋯) f)
      (eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯)
⊢ IsOpenEmbedding.functor ⋯ = map (inclusionTopIso X).inv

Tactic:
refine CategoryTheory.Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑((toTopCat X).obj ⊤) : Type u_1)
refine_1 :
  ∀ (x : (↑X : Type u_1)),
    x ∈ (↑(Functor.obj (IsOpenEmbedding.functor ⋯) U) : Set (↑X : Type u_1)) ↔
      x ∈ (↑((map (inclusionTopIso X).inv).obj U) : Set (↑X : Type u_1))
⊢ Functor.obj (IsOpenEmbedding.functor ⋯) U = (map (inclusionTopIso X).inv).obj U

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑((toTopCat X).obj ⊤) : Type u_1)
x : (↑X : Type u_1)
⊢ x ∈ (↑(Functor.obj (IsOpenEmbedding.functor ⋯) U) : Set (↑X : Type u_1)) ↔
    x ∈ (↑((map (inclusionTopIso X).inv).obj U) : Set (↑X : Type u_1))

Tactic:
⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩

Premises used: trivial, Membership.mem, _private.0.TopologicalSpace.Opens.inclusion'_top_functor.match_1, Subtype.mk, SetLike.coe, And.intro, Iff.intro, Exists.intro, TopologicalSpace.Opens.map, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, TopologicalSpace.Opens.inclusionTopIso, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑((toTopCat X).obj ⊤) : Type u_1)
x : (↑X : Type u_1)
⊢ x ∈ (↑(Functor.obj (IsOpenEmbedding.functor ⋯) U) : Set (↑X : Type u_1)) ↔
    x ∈ (↑((map (inclusionTopIso X).inv).obj U) : Set (↑X : Type u_1))

Tactic:
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
⊢ ∀ (X_1 Y : Opens (↑((toTopCat X).obj ⊤) : Type u_1)) (f : X_1 ⟶ Y),
    Eq (α := Functor.obj (IsOpenEmbedding.functor ⋯) X_1 ⟶ Functor.obj (IsOpenEmbedding.functor ⋯) Y)
      (CategoryTheory.Functor.map (IsOpenEmbedding.functor ⋯) f)
      (eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯)

Tactic:
subsingleton
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type u)) → (↑Y : Type u))
U : Opens (↑Y : Type u)
h :
  ∀ (x : (↑Y : Type u)),
    x ∈ (↑(hf.functor.obj ((map f).obj U)) : Set (↑Y : Type u)) ↔ x ∈ (↑(hf.functor.obj ⊤ ⊓ U) : Set (↑Y : Type u))
⊢ hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U

Tactic:
ext