awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V : Opens (↑X : Type u)
f : U ⟶ V
x : (↑X : Type u)
hx : x ∈ U
⊢ (f : (a : ↥U) → ↥V) (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ U) x hx) =
    Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ V) x ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V : Opens (↑X : Type u)
f : U ⟶ V
x : ↥U
⊢ (↑((f : (a : ↥U) → ↥V) x) : (↑X : Type u)) = (↑x : (↑X : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
f : U ⟶ U
⊢ Eq (α := (a : ↥U) → ↥U) (⇑f : (a : ↥U) → ↥U) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
f : U ⟶ U
x : ↥U
⊢ (f : (a : ↥U) → ↥U) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V W : Opens (↑X : Type u)
f : U ⟶ V
g : V ⟶ W
x : ↥U
⊢ Eq (α := ↥W) ((f ≫ g : (a : ↥U) → ↥W) x : ↥W) ((g : (a : ↥V) → ↥W) ((f : (a : ↥U) → ↥V) x) : ↥W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V : Opens (↑X : Type u)
x : ↥(U ⊓ V)
⊢ Eq (α := ↥U) ((U.infLELeft V : (a : ↥(U ⊓ V)) → ↥U) x : ↥U)
    (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ U) (↑x : (↑X : Type u)) ⋯ : ↥U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V : Opens (↑X : Type u)
x : (↑X : Type u)
m : x ∈ U ⊓ V
⊢ Eq (α := ↥U) ((U.infLELeft V : (a : ↥(U ⊓ V)) → ↥U) (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ U ⊓ V) x m) : ↥U)
    (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ U) x ⋯ : ↥U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
ι : Type u_1
U : ι → Opens (↑X : Type u)
i : ι
x : (↑X : Type u)
m : x ∈ U i
⊢ Eq (α := ↥(iSup U))
    ((leSupr U i : (a : ↥(U i)) → ↥(iSup U)) (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ U i) x m) : ↥(iSup U))
    (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ iSup U) x ⋯ : ↥(iSup U))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U V : Opens (↑X : Type u)
f : U ⟶ V
x : (↑X : Type u)
h : x ∈ U
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          ((toTopCat X).map f) :
        (a : (↑((toTopCat X).obj U) : Type u)) → (↑((toTopCat X).obj V) : Type u))
      (Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ U) x h) =
    Subtype.mk (p := fun (x : (↑X : Type u)) ↦ x ∈ V) x ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ Eq (α := (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          U.inclusion') :
      (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u))
    (Subtype.val (p := fun (x : (↑X : Type u)) ↦ x ∈ U))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ IsOpenEmbedding (X := (↑((toTopCat X).obj U) : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          U.inclusion') :
      (a : (↑((toTopCat X).obj U) : Type u)) → (↑X : Type u))

Tactic:
U.2.isOpenEmbedding_subtypeVal

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Set.Mem, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
U : Opens (↑Y : Type u)
⊢ (↑((map f).obj U) : 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)) ⁻¹'
      (↑U : Set (↑Y : Type u))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
U : Opens (↑Y : Type u)
x : (↑X : Type u)
⊢ x ∈ (map f).obj U ↔
    Membership.mem (α := (↑Y : Type u)) U ((TopCat.Hom.hom f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
U : Set (↑Y : Type u)
p : IsOpen U
⊢ (map f).obj { carrier := U, is_open' := p : Opens (↑Y : 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)) ⁻¹'
          U,
      is_open' := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
U V : Opens (↑Y : Type u)
e : U ≤ V
⊢ (map f).map (homOfLE e) = homOfLE ⋯

Tactic:
rfl

Premises used: Set.Mem, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Opens (↑X : Type u)
⊢ (map (𝟙 X)).obj U = U

Tactic:
let ⟨_, _⟩ := U
  rfl

Premises used: CategoryTheory.CategoryStruct.id, _private.0.TopologicalSpace.Opens.map_id_obj.match_1, TopologicalSpace.Opens.map, Eq, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : Set (↑X : Type u)
p : IsOpen U
⊢ (map (𝟙 X)).obj { carrier := U, is_open' := p : Opens (↑X : Type u) } = { carrier := U, is_open' := p }

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : (Opens (↑X : Type u))ᵒᵖ
⊢ (map (𝟙 X)).obj (unop U) = unop U

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
U : (Opens (↑X : Type u))ᵒᵖ
⊢ (map (𝟙 X)).op.obj U = U

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ (map f).obj ⊤ = ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : Opens (↑Z : Type u)
⊢ (map (f ≫ g)).obj U = (map f).obj ((map g).obj U)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : Set (↑Z : Type u)
p : IsOpen U
⊢ (map (f ≫ g)).obj { carrier := U, is_open' := p : Opens (↑Z : Type u) } =
    (map f).obj ((map g).obj { carrier := U, is_open' := p })

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U V : Opens (↑Z : Type u)
i : U ⟶ V
⊢ (map (f ≫ g)).map i = (map f).map ((map g).map i)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens (↑Z : Type u))ᵒᵖ
⊢ (map (f ≫ g)).obj (unop U) = (map f).obj ((map g).obj (unop U))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens (↑Z : Type u))ᵒᵖ
⊢ (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens (↑Y : Type u)
h :
  ∀ (x : (↑X : Type u)),
    x ∈ (↑((map f).obj (iSup U)) : Set (↑X : Type u)) ↔ x ∈ (↑(iSup ((map f).obj ∘ U)) : Set (↑X : Type u))
⊢ (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens (↑Y : Type u)
x : (↑X : Type u)
⊢ x ∈ (↑((map f).obj (iSup U)) : Set (↑X : Type u)) ↔ x ∈ (↑(iSup ((map f).obj ∘ U)) : Set (↑X : Type u))

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens (↑X : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ map (f ≫ g) = map g ⋙ map f

Tactic:
rfl

Premises used: Set.Mem, setOf, CategoryTheory.Functor.comp, Set.preimage, TopologicalSpace.Opens.map, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
U_1 V W : Opens (↑X : Type u)
f g : X ⟶ Y
h : f = g
U : Opens (↑Y : Type u)
rw rw₁ : (map g).obj U = (map g).obj U
⊢ (map f).obj U = (map g).obj U

Tactic:
rw [congr_arg map h]

Premises used: congr_arg, TopologicalSpace.Opens.map
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f g : X ⟶ Y
h : f = g
subst : map f = map f
⊢ map f = map g

Tactic:
subst h
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ map f = map f

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
h : f = f
⊢ mapIso f f h = Iso.refl (map f)

Tactic:
rfl

Premises used: Eq.mpr, TopologicalSpace.Opens.mapIso, CategoryTheory.eqToHom, CategoryTheory.Iso.refl, CategoryTheory.NatTrans.id, rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
U_1 V W : Opens (↑X : Type u)
f g : X ⟶ Y
h : f = g
U : Opens (↑Y : Type u)
rw rw₁ : (map g).obj U = (map g).obj U
⊢ (map f).obj U = (map g).obj U

Tactic:
rw [h]
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f g : X ⟶ Y
h : f = g
U : Opens (↑Y : Type u)
⊢ (mapIso f g h).hom.app U = eqToHom ⋯

Tactic:
rfl

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y Z : TopCat
U_1 V W : Opens (↑X : Type u)
f g : X ⟶ Y
h : f = g
U : Opens (↑Y : Type u)
rw rw₁ : (map g).obj U = (map g).obj U
⊢ (map g).obj U = (map f).obj U

Tactic:
rw [h]
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f g : X ⟶ Y
h : f = g
U : Opens (↑Y : Type u)
⊢ (mapIso f g h).inv.app U = eqToHom ⋯

Tactic:
rfl

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
H : X ≅ Y
⊢ (mapMapIso H).functor = map H.hom

Tactic:
rfl

Premises used: Set.Mem, Monotone.functor, CategoryTheory.homOfLE, TopologicalSpace.Opens.map, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
H : X ≅ Y
⊢ (mapMapIso H).inverse = map H.inv

Tactic:
rfl

Premises used: Set.Mem, Monotone.functor, CategoryTheory.homOfLE, TopologicalSpace.Opens.map, rfl
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X_1 Y_1 Z : TopCat
U V W : Opens (↑X_1 : Type u)
X Y : TopCat
H : X ≅ Y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X_2 Y_2 : Opens (↑Y : Type u)} (f : X_2 ⟶ Y_2),
    Eq (α := Functor.obj (𝟭 (Opens (↑Y : Type u))) X_2 ⟶ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj Y_2)
      (CategoryTheory.Functor.map (𝟭 (Opens (↑Y : Type u))) f ≫
        Iso.hom
          ((fun (U : Opens (↑Y : Type u)) ↦
              (eqToIso ⋯ :
                Functor.obj (𝟭 (Opens (↑Y : Type u))) U ≅ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj U))
            Y_2))
      (Iso.hom
          ((fun (U : Opens (↑Y : Type u)) ↦
              (eqToIso ⋯ :
                Functor.obj (𝟭 (Opens (↑Y : Type u))) U ≅ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj U))
            X_2) ≫
        ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).map f)
⊢ ∀ {X_2 Y_2 : Opens (↑Y : Type u)} (f : X_2 ⟶ Y_2),
    Eq (α := Functor.obj (𝟭 (Opens (↑Y : Type u))) X_2 ⟶ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj Y_2)
      (CategoryTheory.Functor.map (𝟭 (Opens (↑Y : Type u))) f ≫
        Iso.hom
          ((fun (U : Opens (↑Y : Type u)) ↦
              (eqToIso ⋯ :
                Functor.obj (𝟭 (Opens (↑Y : Type u))) U ≅ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj U))
            Y_2))
      (Iso.hom
          ((fun (U : Opens (↑Y : Type u)) ↦
              (eqToIso ⋯ :
                Functor.obj (𝟭 (Opens (↑Y : Type u))) U ≅ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj U))
            X_2) ≫
        ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).map f)

Tactic:
cat_disch
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
H : X ≅ Y
⊢ (mapMapIso H).unitIso = NatIso.ofComponents (fun (U : Opens (↑Y : Type u)) ↦ eqToIso ⋯) ⋯

Tactic:
rfl

Premises used: Monotone.functor, CategoryTheory.Iso.symm, rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X_1 Y_1 Z : TopCat
U V W : Opens (↑X_1 : Type u)
X Y : TopCat
H : X ≅ Y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X_2 Y_2 : Opens (↑X : Type u)} (f : X_2 ⟶ Y_2),
    Eq (α := ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj X_2 ⟶ Functor.obj (𝟭 (Opens (↑X : Type u))) Y_2)
      (((mapMapIso H).inverse ⋙ (mapMapIso H).functor).map f ≫
        Iso.hom
          ((fun (U : Opens (↑X : Type u)) ↦
              (eqToIso ⋯ :
                ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj U ≅ Functor.obj (𝟭 (Opens (↑X : Type u))) U))
            Y_2))
      (Iso.hom
          ((fun (U : Opens (↑X : Type u)) ↦
              (eqToIso ⋯ :
                ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj U ≅ Functor.obj (𝟭 (Opens (↑X : Type u))) U))
            X_2) ≫
        CategoryTheory.Functor.map (𝟭 (Opens (↑X : Type u))) f)
⊢ ∀ {X_2 Y_2 : Opens (↑X : Type u)} (f : X_2 ⟶ Y_2),
    Eq (α := ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj X_2 ⟶ Functor.obj (𝟭 (Opens (↑X : Type u))) Y_2)
      (((mapMapIso H).inverse ⋙ (mapMapIso H).functor).map f ≫
        Iso.hom
          ((fun (U : Opens (↑X : Type u)) ↦
              (eqToIso ⋯ :
                ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj U ≅ Functor.obj (𝟭 (Opens (↑X : Type u))) U))
            Y_2))
      (Iso.hom
          ((fun (U : Opens (↑X : Type u)) ↦
              (eqToIso ⋯ :
                ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj U ≅ Functor.obj (𝟭 (Opens (↑X : Type u))) U))
            X_2) ≫
        CategoryTheory.Functor.map (𝟭 (Opens (↑X : Type u))) f)

Tactic:
cat_disch
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
H : X ≅ Y
⊢ (mapMapIso H).counitIso = NatIso.ofComponents (fun (U : Opens (↑X : Type u)) ↦ eqToIso ⋯) ⋯

Tactic:
rfl

Premises used: Monotone.functor, CategoryTheory.Iso.symm, rfl, CategoryTheory.NatIso.ofComponents
-- 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))
H : Mono f
X_1 Y_1 : Opens (↑X : Type u)
i : hf.functor.obj X_1 ⟶ hf.functor.obj Y_1
x : (↑X : Type u)
hx : x ∈ X_1
obtain :
  ∀ (y : (↑X : Type u)) (hy : y ∈ (↑Y_1 : Set (↑X : Type u)))
    (eq :
      Eq (α := (↑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))
            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 :
          (↑Y : Type u))),
    x ∈ Y_1
⊢ x ∈ Y_1

Tactic:
obtain ⟨y, hy, eq⟩ := i.le ⟨x, hx, rfl⟩

Premises used: Quiver.Hom.le, And.intro, Exists.intro, rfl
-- 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))
H : Mono f
X_1 Y_1 : Opens (↑X : Type u)
i : hf.functor.obj X_1 ⟶ hf.functor.obj Y_1
x : (↑X : Type u)
hx : x ∈ X_1
y : (↑X : Type u)
hy : y ∈ (↑Y_1 : Set (↑X : Type u))
eq :
  Eq (α := (↑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))
        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 :
      (↑Y : Type u))
⊢ x ∈ Y_1

Tactic:
(TopCat.mono_iff_injective f).mp H eq ▸ hy

Premises used: Eq.rec, Iff.mp, TopCat.mono_iff_injective
-- 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))
H : Mono f
X_1 Y_1 : Opens (↑X : Type u)
i : hf.functor.obj X_1 ⟶ hf.functor.obj Y_1
x : (↑X : Type u)
hx : x ∈ X_1
y : (↑X : Type u)
hy : y ∈ (↑Y_1 : Set (↑X : Type u))
eq :
  Eq (α := (↑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))
        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 :
      (↑Y : Type u))
⊢ x ∈ Y_1

Tactic:
exact (TopCat.mono_iff_injective f).mp H eq ▸ hy
-- Module: Mathlib.Topology.Category.TopCat.Opens
Goal:
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenEmbedding (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))
⊢ Function.Injective hf.functor.obj

Tactic:
fun _ _ e ↦ Opens.ext (Set.image_injective.mpr hf.injective (congr_arg (↑· : Opens Y → Set Y) e))

Premises used: Iff.mpr, Set.image_injective, Topology.IsOpenEmbedding.toIsEmbedding, TopologicalSpace.Opens.ext, congr_arg, SetLike.coe, Topology.IsEmbedding.injective, Function.Injective
-- 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)
a : (Opens.map f).obj (hf.functorObj U) ≤ U
a₁ : U ≤ (Opens.map f).obj (hf.functorObj U)
⊢ (Opens.map f).obj (hf.functorObj U) = U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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)
s : Opens (↑Y : Type u)
hx :
  Membership.mem (α := (↑Y : Type u)) s
    ((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 s

Tactic:
hx

Premises used: Set.Mem, setOf, Set.preimage
-- 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)
s : Opens (↑Y : Type u)
hx :
  Membership.mem (α := (↑Y : Type u)) s
    ((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 s

Tactic:
exact hx
-- 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)
hx : x ∈ U
a :
  ∀ (U : Set (↑X : Type u)) (hU : IsOpen U) (hx : x ∈ { carrier := U, is_open' := hU : Opens (↑X : Type u) }),
    x ∈ (Opens.map f).obj (hf.functorObj { carrier := U, is_open' := hU : Opens (↑X : Type u) })
⊢ x ∈ (Opens.map f).obj (hf.functorObj 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))
x : (↑X : Type u)
U : Set (↑X : Type u)
hU : IsOpen U
hx : x ∈ { carrier := U, is_open' := hU : Opens (↑X : Type u) }
a :
  ∀ (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) })
⊢ x ∈ (Opens.map f).obj (hf.functorObj { carrier := U, is_open' := hU : Opens (↑X : Type u) })

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))
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:
Opens.mem_sSup.mpr ⟨⟨_, ht⟩, rfl, hx⟩

Premises used: Iff.mpr, Set.Mem, iSup, setOf, TopologicalSpace.Opens.mem_sSup, TopologicalSpace.Opens.mk, Set.preimage, And.intro, Exists.intro, Set.iUnion, rfl