awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
      (a : (↑Y : Type u)) → (↑c.pt : Type u))

Tactic:
simpa only [← epi_iff_surjective] using epi_of_isColimit_cofork hc

Premises used: TopCat.epi_iff_surjective, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
U : Set (↑(coequalizer f g) : Type u)
⊢ IsOpen U ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              coequalizer f g) (coequalizer.π f g)) :
          (a : (↑Y : Type u)) → (↑(coequalizer f g) : Type u)) ⁻¹'
        U)

Tactic:
isOpen_iff_of_isColimit_cofork _ (coequalizerIsCoequalizer f g) _

Premises used: CategoryTheory.Limits.coequalizerIsCoequalizer, TopCat.isOpen_iff_of_isColimit_cofork
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
p : (↑(tensorObj (𝒞 := instCategory) W Y) : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) X Z) : Type u))
    ((Hom.hom (f ⊗ₘ g) : (a : (↑(W ⊗ Y) : Type u)) → (↑(X ⊗ Z) : Type u)) p :
      (↑(tensorObj (𝒞 := instCategory) X Z) : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑W : Type u)) → (↑X : Type u))
          p.1,
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          p.2) :
      (↑X : Type u) × (↑Z : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
f : Y ⟶ Z
p : (↑(tensorObj (𝒞 := instCategory) X Y) : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) X Z) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            tensorObj (𝒞 := instCategory) X Y) (X ◁ f) :
          (a : (↑(X ⊗ Y) : Type u)) → (↑(X ⊗ Z) : Type u))
        p :
      (↑(tensorObj (𝒞 := instCategory) X Z) : Type u))
    ((p.1,
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          p.2) :
      (↑X : Type u) × (↑Z : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
Y Z : TopCat
f : Y ⟶ Z
X : TopCat
p : (↑(tensorObj (𝒞 := instCategory) Y X) : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) Z X) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            tensorObj (𝒞 := instCategory) Y X) (f ▷ X) :
          (a : (↑(Y ⊗ X) : Type u)) → (↑(Z ⊗ X) : Type u))
        p :
      (↑(tensorObj (𝒞 := instCategory) Z X) : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          p.1,
        p.2) :
      (↑Z : Type u) × (↑X : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
x : (↑X : Type u)
p : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          tensorObj (𝒞 := instCategory) ((𝟙_ TopCat) (𝒞 := instCategory)) X) (Iso.hom (λ_ X)) :
        (a : (↑(𝟙_ TopCat ⊗ X) : Type u)) → (↑X : Type u))
      (p, x) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
x : (↑X : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
          tensorObj (𝒞 := instCategory) ((𝟙_ TopCat) (𝒞 := instCategory)) X) (Iso.inv (λ_ X)) :
        (a : (↑X : Type u)) → (↑(𝟙_ TopCat ⊗ X) : Type u))
      x =
    (PUnit.unit, x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
x : (↑X : Type u)
p : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          tensorObj (𝒞 := instCategory) X ((𝟙_ TopCat) (𝒞 := instCategory))) (Iso.hom (ρ_ X)) :
        (a : (↑(X ⊗ 𝟙_ TopCat) : Type u)) → (↑X : Type u))
      (x, p) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
x : (↑X : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
          tensorObj (𝒞 := instCategory) X ((𝟙_ TopCat) (𝒞 := instCategory))) (Iso.inv (ρ_ X)) :
        (a : (↑X : Type u)) → (↑(X ⊗ 𝟙_ TopCat) : Type u))
      x =
    (x, PUnit.unit)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑X : Type u)
y : (↑Y : Type u)
z : (↑Z : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) (Iso.hom (α_ X Y Z)) :
        (a : (↑((X ⊗ Y) ⊗ Z) : Type u)) → (↑(X ⊗ Y ⊗ Z) : Type u))
      ((x, y), z) =
    (x, y, z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑X : Type u)
y : (↑Y : Type u)
z : (↑Z : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) (Iso.inv (α_ X Y Z)) :
        (a : (↑(X ⊗ Y ⊗ Z) : Type u)) → (↑((X ⊗ Y) ⊗ Z) : Type u))
      (x, y, z) =
    ((x, y), z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑(tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) : Type u)
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) (Iso.hom (α_ X Y Z)) :
          (a : (↑((X ⊗ Y) ⊗ Z) : Type u)) → (↑(X ⊗ Y ⊗ Z) : Type u))
        x).1 =
    x.1.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑(tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) : Type u)
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) (Iso.hom (α_ X Y Z)) :
            (a : (↑((X ⊗ Y) ⊗ Z) : Type u)) → (↑(X ⊗ Y ⊗ Z) : Type u))
          x).2.1 =
    x.1.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑(tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) : Type u)
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z) (Iso.hom (α_ X Y Z)) :
            (a : (↑((X ⊗ Y) ⊗ Z) : Type u)) → (↑(X ⊗ Y ⊗ Z) : Type u))
          x).2.2 =
    x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑(tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) : Type u)
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) (Iso.inv (α_ X Y Z)) :
            (a : (↑(X ⊗ Y ⊗ Z) : Type u)) → (↑((X ⊗ Y) ⊗ Z) : Type u))
          x).1.1 =
    x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑(tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) : Type u)
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) (Iso.inv (α_ X Y Z)) :
            (a : (↑(X ⊗ Y ⊗ Z) : Type u)) → (↑((X ⊗ Y) ⊗ Z) : Type u))
          x).1.2 =
    x.2.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
x : (↑(tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) : Type u)
⊢ ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)) (Iso.inv (α_ X Y Z)) :
          (a : (↑(X ⊗ Y ⊗ Z) : Type u)) → (↑((X ⊗ Y) ⊗ Z) : Type u))
        x).2 =
    x.2.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y : TopCat
x : (↑X : Type u)
y : (↑Y : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          tensorObj (𝒞 := instCategory) X Y) (Iso.hom (β_ X Y)) :
        (a : (↑(X ⊗ Y) : Type u)) → (↑(Y ⊗ X) : Type u))
      (x, y) =
    (y, x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y : TopCat
x : (↑X : Type u)
y : (↑Y : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          tensorObj (𝒞 := instCategory) Y X) (Iso.inv (β_ X Y)) :
        (a : (↑(Y ⊗ X) : Type u)) → (↑(X ⊗ Y) : Type u))
      (y, x) =
    (x, y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : X ⟶ Z
x : (↑X : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) Y Z) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            tensorObj (𝒞 := instCategory) Y Z) (CartesianMonoidalCategory.lift f g) :
          (a : (↑X : Type u)) → (↑(Y ⊗ Z) : Type u))
        x :
      (↑(tensorObj (𝒞 := instCategory) Y Z) : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
            (a : (↑X : Type u)) → (↑Z : Type u))
          x) :
      (↑Y : Type u) × (↑Z : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
⊢ LocallyCompactSpace.{u_1} (↑I : Type u_1)

Tactic:
inferInstanceAs (LocallyCompactSpace (ULift unitInterval))

Premises used: _private.0.TopCat.instLocallyCompactSpaceCarrierI._proof_1
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
x y : (↑I : Type u)
h :
  Eq (α := (↑unitInterval : Type))
    ((homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) x : (↑unitInterval : Type))
    ((homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) y : (↑unitInterval : Type))
⊢ x = y

Tactic:
homeomorph.injective h

Premises used: TopCat.I.homeomorph, Homeomorph.injective
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
⊢ Continuous (X := ULift.{u, 0} (↑unitInterval : Type)) (Y := ULift.{u, 0} (↑unitInterval : Type))
    ((⇑homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) ∘
      unitInterval.symm ∘ (⇑homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
x : (↑I : Type u_1)
⊢ (homeomorph : (a : (↑I : Type u_1)) → (↑unitInterval : Type))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            symm :
          (a : (↑I : Type u_1)) → (↑I : Type u_1))
        x) =
    unitInterval.symm ((homeomorph : (a : (↑I : Type u_1)) → (↑unitInterval : Type)) x)

Tactic:
rfl

Premises used: unitInterval.symm, rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
⊢ Eq (α := (↑unitInterval : Type))
    ((homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) 0 : (↑unitInterval : Type))
    (0 : (↑unitInterval : Type))

Tactic:
simp [OfNat.ofNat]

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
⊢ Eq (α := (↑unitInterval : Type))
    ((homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type)) 1 : (↑unitInterval : Type))
    (1 : (↑unitInterval : Type))

Tactic:
simp [OfNat.ofNat]

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
⊢ Eq (α := (↑I : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) symm :
          (a : (↑I : Type u_1)) → (↑I : Type u_1))
        1 :
      (↑I : Type u_1))
    (0 : (↑I : Type u_1))

Tactic:
aesop
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
⊢ Eq (α := (↑I : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) symm :
          (a : (↑I : Type u_1)) → (↑I : Type u_1))
        0 :
      (↑I : Type u_1))
    (1 : (↑I : Type u_1))

Tactic:
aesop
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ ι₀ ≫ f ▷ I = f ≫ ι₀

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
⊢ ι₀ ≫ fst X I = 𝟙 X

Tactic:
rfl

Premises used: ContinuousMap.id, rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
⊢ ι₀ ≫ snd X I = const 0

Tactic:
rfl

Premises used: ContinuousMap.comp, TopCat.I, rfl, TopCat.const
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
x : (↑X : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) X I) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := X)
            ι₀ :
          (a : (↑X : Type u)) → (↑(X ⊗ I) : Type u))
        x :
      (↑(tensorObj (𝒞 := instCategory) X I) : Type u))
    ((x, 0) : (↑X : Type u) × (↑I : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ ι₁ ≫ f ▷ I = f ≫ ι₁

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
⊢ ι₁ ≫ fst X I = 𝟙 X

Tactic:
rfl

Premises used: ContinuousMap.id, rfl
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
⊢ ι₁ ≫ snd X I = const 1

Tactic:
rfl

Premises used: ContinuousMap.comp, TopCat.I, rfl, TopCat.const
-- Module: Mathlib.Topology.Category.TopCat.Monoidal
Goal:
X : TopCat
x : (↑X : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := instCategory) X I) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := X)
            ι₁ :
          (a : (↑X : Type u)) → (↑(X ⊗ I) : Type u))
        x :
      (↑(tensorObj (𝒞 := instCategory) X I) : Type u))
    ((x, 1) : (↑X : Type u) × (↑I : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X : TopCat
x : (↑X : Type u)
U V : OpenNhds x
⊢ U ≤ V ↔ (↑U : Opens (↑X : Type u)) ≤ (↑V : Opens (↑X : Type u))

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X Y : TopCat
f : X ⟶ Y
x_1 : (↑X : Type u)
U V W : OpenNhds x_1
x_2 : (↑X : Type u)
x : OpenNhds x_2
mk :
  ∀ (val : Opens (↑X : Type u)) (property : x_2 ∈ val),
    LE.le (α := OpenNhds x_2) (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x_2 ∈ U) val property)
      (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x_2 ∈ U) ⊤ trivial)
⊢ x ≤ Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x_2 ∈ U) ⊤ trivial

Tactic:
cases x
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X Y : TopCat
f : X ⟶ Y
x_1 : (↑X : Type u)
U V W : OpenNhds x_1
x : (↑X : Type u)
val : Opens (↑X : Type u)
property : x ∈ val
⊢ LE.le (α := OpenNhds x) (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x ∈ U) val property)
    (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x ∈ U) ⊤ trivial)

Tactic:
simp [le_def]

Premises used: TopologicalSpace.OpenNhds.le_def
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X Y : TopCat
f : X ⟶ Y
x : (↑X : Type u)
U V W : OpenNhds x
down : U ≤ V
a₂ : U ⟶ V
h :
  Eq.{u + 1} (α := (a : ↥(↑U : Opens (↑X : Type u))) → ↥(↑V : Opens (↑X : Type u)))
    ((fun (f : U ⟶ V) ↦
        Set.inclusion (s := (↑(↑U : Opens (↑X : Type u)) : Set (↑X : Type u))) (t :=
          (↑(↑V : Opens (↑X : Type u)) : Set (↑X : Type u))) ⋯)
      { down := { down := down } })
    ((fun (f : U ⟶ V) ↦
        Set.inclusion (s := (↑(↑U : Opens (↑X : Type u)) : Set (↑X : Type u))) (t :=
          (↑(↑V : Opens (↑X : Type u)) : Set (↑X : Type u))) ⋯)
      a₂)
⊢ { down := { down := down : PLift (U ≤ V) } : ULift.{u, 0} (PLift (U ≤ V)) } = a₂

Tactic:
congr!
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X : TopCat
x : (↑X : Type u)
U V : OpenNhds x
f : U ⟶ V
y : (↑X : Type u)
hy : y ∈ (↑U : Opens (↑X : Type u))
⊢ (f : (a : ↥(↑U : Opens (↑X : Type u))) → ↥(↑V : Opens (↑X : Type u)))
      (Subtype.mk (p := fun (x_1 : (↑X : Type u)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u))) y hy) =
    Subtype.mk (p := fun (x_1 : (↑X : Type u)) ↦ x_1 ∈ (↑V : Opens (↑X : Type u))) y ⋯

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X : TopCat
x : (↑X : Type u)
U : Opens (↑X : Type u)
p : x ∈ U
⊢ (inclusion x).obj (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x ∈ U) U p) = U

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X : TopCat
x : (↑X : Type u)
U : OpenNhds x
⊢ IsOpenEmbedding (X := (↑((Opens.toTopCat X).obj (↑U : Opens (↑X : Type 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 : Opens (↑X : Type u)).inclusion') :
      (a : (↑((Opens.toTopCat X).obj (↑U : Opens (↑X : Type u))) : Type u)) → (↑X : Type u))

Tactic:
U.1.isOpenEmbedding

Premises used: TopologicalSpace.Opens.isOpenEmbedding, Subtype.val
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X Y : TopCat
f : X ⟶ Y
x : (↑X : Type u)
U : Opens (↑Y : Type u)
q :
  Membership.mem (α := (↑Y : Type u)) 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))
⊢ (map f x).obj
      (Subtype.mk (p := fun (U : Opens (↑Y : Type u)) ↦
        Membership.mem (α := (↑Y : Type u)) 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)))
        U q) =
    Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x ∈ U) ((Opens.map f).obj U) q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X : TopCat
x : (↑X : Type u)
U :
  OpenNhds (X := X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (𝟙 X) :
        (a : (↑X : Type u)) → (↑X : Type u))
      x)
⊢ (map (𝟙 X) x).obj U = U

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, TopologicalSpace.OpenNhds, rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X : TopCat
x : (↑X : Type u)
U : Set (↑X : Type u)
p : IsOpen U
q :
  Membership.mem (α := (↑X : Type u)) { carrier := U, is_open' := p : Opens (↑X : Type u) }
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (𝟙 X) :
          (a : (↑X : Type u)) → (↑X : Type u))
        x :
      (↑X : Type u))
⊢ (map (𝟙 X) x).obj
      (Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦
        Membership.mem (α := (↑X : Type u)) U
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  (𝟙 X) :
                (a : (↑X : Type u)) → (↑X : Type u))
              x :
            (↑X : Type u)))
        { carrier := U, is_open' := p : Opens (↑X : Type u) } q) =
    Subtype.mk (p := fun (U : Opens (↑X : Type u)) ↦ x ∈ U) { carrier := U, is_open' := p } q

Tactic:
rfl

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

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

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X Y : TopCat
f : X ⟶ Y
x : (↑X : Type u)
⊢ (inclusionMapIso f x).hom =
    𝟙
      (inclusion
          ((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) ⋙
        Opens.map f)

Tactic:
rfl

Premises used: Set.Mem, CategoryTheory.Functor.comp, TopologicalSpace.OpenNhds.map, Monotone.functor, CategoryTheory.homOfLE, TopologicalSpace.OpenNhds, CategoryTheory.NatTrans.id, TopologicalSpace.OpenNhds.inclusion, rfl
-- Module: Mathlib.Topology.Category.TopCat.OpenNhds
Goal:
X Y : TopCat
f : X ⟶ Y
x : (↑X : Type u)
⊢ (inclusionMapIso f x).inv = 𝟙 (map f x ⋙ inclusion x)

Tactic:
rfl

Premises used: Set.Mem, CategoryTheory.Functor.comp, TopologicalSpace.OpenNhds.map, Monotone.functor, CategoryTheory.homOfLE, TopologicalSpace.OpenNhds, CategoryTheory.NatTrans.id, TopologicalSpace.OpenNhds.inclusion, rfl