awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
rw : Dense (range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₁ : t ⊆ closure[inst] ↑(range (inclusion (s := s) (t := t) hst)) ↔ t ⊆ closure[inst] s
rw₂ :
  t ⊆ closure[inst] (range (Subtype.val (p := fun (x : X) ↦ x ∈ t) ∘ inclusion (s := s) (t := t) hst)) ↔
    t ⊆ closure[inst] s
rw₃ : t ⊆ closure[inst] (range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ↔ t ⊆ closure[inst] s
rw₄ rw₅ : t ⊆ closure[inst] s ↔ t ⊆ closure[inst] s
⊢ DenseRange (inclusion (s := s) (t := t) hst) ↔ t ⊆ closure[inst] s

Tactic:
rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]

Premises used: Set.range_comp, Set.val_comp_inclusion, Subtype.dense_iff, Subtype.range_coe, DenseRange
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : (↑s : Type u)
rw : 𝓝[range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))] (↑x : X) = 𝓝[s] (↑x : X)
rw₁ rw₂ : 𝓝[s] (↑x : X) = 𝓝[s] (↑x : X)
⊢ map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x) = 𝓝[s] (↑x : X)

Tactic:
rw [IsInducing.subtypeVal.map_nhds_eq, Subtype.range_val]

Premises used: Subtype.range_val, Topology.IsInducing.subtypeVal, Topology.IsInducing.map_nhds_eq
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
rw : p ∈ 𝓝 (↑(Subtype.mk (p := p) x hx) : X)
⊢ range (ι := Subtype p) (Subtype.val (p := p)) ∈ 𝓝 (↑(Subtype.mk (p := p) x hx) : X)

Tactic:
rw [Subtype.range_val]

Premises used: Subtype.range_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 (↑(Subtype.mk (p := p) x hx) : X)

Tactic:
h

Premises used: Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 (↑(Subtype.mk (p := p) x hx) : X)

Tactic:
exact h
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : X
h : p x
⊢ 𝓝 (Subtype.mk (p := p) x h) = comap (Subtype.val (p := p)) (𝓝 x)

Tactic:
nhds_induced _ _

Premises used: nhds_induced
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
rw :
  Tendsto (Subtype.val (p := p) ∘ f) l (𝓝 a) ↔
    Tendsto (fun (x : Y) ↦ (↑(f x) : X)) l (𝓝 (↑(Subtype.mk (p := p) a ha) : X))
⊢ Tendsto f l (𝓝 (Subtype.mk (p := p) a ha)) ↔
    Tendsto (fun (x : Y) ↦ (↑(f x) : X)) l (𝓝 (↑(Subtype.mk (p := p) a ha) : X))

Tactic:
rw [nhds_subtype_eq_comap, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, nhds_subtype_eq_comap
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_5
p : X → Prop
l : Filter Y
f : Y → Subtype p
a : X
ha : p a
⊢ Tendsto (Subtype.val (p := p) ∘ f) l (𝓝 a) ↔
    Tendsto (fun (x : Y) ↦ (↑(f x) : X)) l (𝓝 (↑(Subtype.mk (p := p) a ha) : X))

Tactic:
rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
x : { a : X // p a }
s : Set { a : X // p a }
⊢ x ∈ closure[instTopologicalSpaceSubtype] s ↔ (↑x : X) ∈ closure[inst] (Subtype.val (p := fun (a : X) ↦ p a) '' s)

Tactic:
closure_induced

Premises used: Set.Mem, closure_induced
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
t : Set Y
h1 : ∀ (x : X), f x ∈ t
x : X
⊢ ContinuousAt (codRestrict f t h1) x ↔ ContinuousAt f x

Tactic:
IsInducing.subtypeVal.continuousAt_iff

Premises used: Topology.IsInducing.continuousAt_iff, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h1 : MapsTo f s t
x : (↑s : Type u)
h2 : ContinuousAt f (↑x : X)
⊢ ContinuousAt (MapsTo.restrict f s t h1) x

Tactic:
(h2.comp continuousAt_subtype_val).codRestrict _

Premises used: Subtype.map, continuousAt_subtype_val, ContinuousAt.codRestrict, ContinuousAt.comp, Set.codRestrict, Set.MapsTo.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
x : (↑(f ⁻¹' s) : Type u)
h : ContinuousAt f (↑x : X)
⊢ ContinuousAt (s.restrictPreimage f) x

Tactic:
h.restrict _

Premises used: Set.restrictPreimage, ContinuousAt.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst, inst_1] f
hs : ∀ (a : X), f a ∈ s
⊢ Continuous[inst, instTopologicalSpaceSubtype] (Set.codRestrict f s hs)

Tactic:
hf.subtype_mk hs

Premises used: Continuous.subtype_mk, Set.codRestrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ IsOpenMap (Set.codRestrict f s hs)

Tactic:
hf.subtype_mk hs

Premises used: IsOpenMap.subtype_mk, Set.codRestrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedMap f
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ IsClosedMap (Set.codRestrict f s hs)

Tactic:
hf.subtype_mk hs

Premises used: IsClosedMap.subtype_mk, Set.codRestrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h1 : MapsTo f s t
h2 : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (MapsTo.restrict f s t h1)

Tactic:
(h2.comp continuous_subtype_val).codRestrict _

Premises used: Subtype.map, continuous_subtype_val, Continuous.comp, Continuous.codRestrict, Set.codRestrict, Set.MapsTo.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set X
t : Set Y
hs : IsOpen[inst] s
ht : MapsTo f s t
⊢ IsOpenMap (MapsTo.restrict f s t ht)

Tactic:
(hf.restrict hs).codRestrict _

Premises used: Subtype.map, IsOpenMap.codRestrict, IsOpenMap.restrict, Set.codRestrict, Set.restrict, Set.MapsTo.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedMap f
s : Set X
t : Set Y
hs : IsClosed[inst] s
ht : MapsTo f s t
⊢ IsClosedMap (MapsTo.restrict f s t ht)

Tactic:
(hf.restrict hs).codRestrict _

Premises used: Subtype.map, IsClosedMap.codRestrict, Set.codRestrict, IsClosedMap.restrict, Set.restrict, Set.MapsTo.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
h : Continuous[inst, inst_1] f
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (s.restrictPreimage f)

Tactic:
h.restrict _

Premises used: Set.restrictPreimage, Continuous.restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
⊢ IsEmbedding (MapsTo.restrict f s t H)

Tactic:
.of_comp (hf.continuous.restrict H) continuous_subtype_val (hf.comp .subtypeVal)

Premises used: continuous_subtype_val, Continuous.restrict, Topology.IsEmbedding.comp, Topology.IsEmbedding.of_comp, Topology.IsEmbedding.subtypeVal, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
hs : IsOpen[inst] s
rw : IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ t) ⁻¹' f '' s)
⊢ IsOpen[instTopologicalSpaceSubtype] (range (MapsTo.restrict f s t H))

Tactic:
rw [MapsTo.range_restrict]

Premises used: Set.MapsTo.range_restrict
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
hs : IsOpen[inst] s
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ t) ⁻¹' f '' s)

Tactic:
continuous_subtype_val.1 _ (hf.isOpenMap _ hs)

Premises used: Topology.IsOpenEmbedding.isOpenMap, continuous_subtype_val, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
hs : IsOpen[inst] s
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ t) ⁻¹' f '' s)

Tactic:
exact continuous_subtype_val.1 _ (hf.isOpenMap _ hs)

Premises used: Topology.IsOpenEmbedding.isOpenMap, continuous_subtype_val, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsInducing e
s : Set Y
hs : ∀ (x : X), e x ∈ s
⊢ IsInducing (Set.codRestrict e s hs)

Tactic:
he.of_comp (he.continuous.codRestrict hs) continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.codRestrict, Topology.IsInducing.continuous, Topology.IsInducing.of_comp
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X → Y
he : IsEmbedding e
s : Set Y
hs : ∀ (x : X), e x ∈ s
⊢ IsEmbedding (codRestrict e s hs)

Tactic:
he.of_comp (he.continuous.codRestrict hs) continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.codRestrict, Topology.IsEmbedding.of_comp, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : s ⊆ t
⊢ IsEmbedding (inclusion (s := s) (t := t) h)

Tactic:
IsEmbedding.subtypeVal.codRestrict _ _

Premises used: Topology.IsEmbedding.codRestrict, Set.codRestrict, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen[instTopologicalSpaceSubtype] (t ↓∩ s)
rwa rwa₁ rwa₂ rwa₃ : IsOpen[instTopologicalSpaceSubtype] {x : (↑t : Type u) | (↑x : X) ∈ s}
⊢ IsOpen[instTopologicalSpaceSubtype] (range (inclusion (s := s) (t := t) hst))

Tactic:
rwa [range_inclusion]

Premises used: Set.range_inclusion
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
rwa rwa₁ rwa₂ rwa₃ : IsClosed[instTopologicalSpaceSubtype] {x : (↑t : Type u) | (↑x : X) ∈ s}
⊢ IsClosed[instTopologicalSpaceSubtype] (range (inclusion (s := s) (t := t) hst))

Tactic:
rwa [range_inclusion]

Premises used: Set.range_inclusion
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u_5
inst : TopologicalSpace X
s t : Set X
h : DiscreteTopology.{u_5} (↑s : Type u_5)
ts : t ⊆ s
⊢ DiscreteTopology.{u_5} (↑t : Type u_5)

Tactic:
(IsEmbedding.inclusion ts).discreteTopology

Premises used: Topology.IsEmbedding.inclusion, Topology.IsEmbedding.discreteTopology
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
hst : t ⊆ s
⊢ IsDiscrete t

Tactic:
⟨.of_subset hs.to_subtype hst⟩

Premises used: IsDiscrete.to_subtype, IsDiscrete.mk, DiscreteTopology.of_subset
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u_5
Y : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
inst_2 : DiscreteTopology.{u_6} (↑s : Type u_6)
f : X → Y
hc : Continuous[inst, inst_1] f
hinj : Injective f
⊢ MapsTo f (f ⁻¹' s) s

Tactic:
fun _ x ↦ x

Premises used: Set.Mem, setOf, Set.preimage, Set.MapsTo
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u_5
Y : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
inst_2 : DiscreteTopology.{u_6} (↑s : Type u_6)
f : X → Y
hc : Continuous[inst, inst_1] f
hinj : Injective f
⊢ MapsTo f (f ⁻¹' s) s

Tactic:
exact fun _ x ↦ x
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
⊢ IsCoinducing (s.restrictPreimage f)

Tactic:
.of_isOpen_preimage_iff_isOpen fun _ ↦ ?_

Premises used: Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
refine :
  ∀ (x : Set (↑s : Type v)),
    IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x
⊢ IsCoinducing (s.restrictPreimage f)

Tactic:
refine .of_isOpen_preimage_iff_isOpen fun _ ↦ ?_
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst_1] s
x : Set (↑s : Type v)
rw :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst_1] (Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
rw₁ :
  IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
rw₂ :
  IsOpen[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ f ⁻¹' s) '' s.restrictPreimage f ⁻¹' x) ↔
    IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
rw₃ rw₄ :
  IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x) ↔
    IsOpen[inst] (f ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ s) '' x)
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x) ↔ IsOpen[instTopologicalSpaceSubtype] x

Tactic:
rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Topology.IsCoinducing.isOpen_preimage, Topology.IsCoinducing.continuous, IsOpen.preimage, Set.image_val_preimage_restrictPreimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap f
s : Set Y
hs : IsOpen[inst_1] s
⊢ IsQuotientMap (s.restrictPreimage f)

Tactic:
(isQuotientMap_iff _).2
    ⟨.restrictPreimage_of_isOpen hf.isCoinducing hs, hf.surjective.restrictPreimage _⟩

Premises used: Iff.mpr, Topology.IsCoinducing.restrictPreimage_of_isOpen, Topology.IsQuotientMap.surjective, Topology.isQuotientMap_iff, Function.Surjective.restrictPreimage, And.intro, Topology.IsQuotientMap.isCoinducing
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
rw : s ∩ closure[inst] (s ∩ t) ⊆ s
rw₁ : s ∩ t ⊆ s ∩ closure[inst] (s ∩ t)
⊢ IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t) ↔ s ∩ closure[inst] (s ∩ t) ⊆ t

Tactic:
rw [← closure_eq_iff_isClosed, IsEmbedding.subtypeVal.closure_eq_preimage_closure_image,
    ← Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe,
    Subtype.image_preimage_coe, subset_antisymm_iff, and_iff_left, Set.subset_inter_iff,
    and_iff_right]

Premises used: Subtype.val_injective, Set.subset_inter_iff, Subtype.image_preimage_coe, closure_eq_iff_isClosed, and_iff_left, Function.Injective.eq_iff, and_iff_right, subset_antisymm_iff, Topology.IsEmbedding.subtypeVal, Function.Injective.image_injective, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst] (s ∩ t) ⊆ s

Tactic:
Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure[inst] (s ∩ t)

Tactic:
Set.subset_inter Set.inter_subset_left subset_closure

Premises used: subset_closure, Set.inter_subset_left, Set.subset_inter
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ s ∩ closure[inst] (s ∩ t) ⊆ s

Tactic:
exacts [Set.inter_subset_left, Set.subset_inter Set.inter_subset_left subset_closure]

Premises used: subset_closure, Set.inter_subset_left, Set.subset_inter
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
ht : IsOpen[inst] t
⊢ frontier (s ∩ t) ∩ t = frontier s ∩ t

Tactic:
simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff,
    ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
    Subtype.preimage_coe_self_inter]

Premises used: continuous_subtype_val, Subtype.preimage_coe_self_inter, Set.inter_comm, IsOpen.isOpenMap_subtype_val, Subtype.preimage_coe_eq_preimage_coe_iff, IsOpenMap.preimage_frontier_eq_frontier_preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
ht : IsOpen[inst] t
⊢ IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)

Tactic:
ht.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
ht : IsOpen[instTopologicalSpaceSubtype] t
⊢ ∃ (c : Set X), IsOpen[inst] c ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t = c ∩ s

Tactic:
simpa using IsInducing.subtypeVal.image_eq_isOpen_inter_range ht

Premises used: Topology.IsInducing.image_eq_isOpen_inter_range, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
huo : IsOpen[instTopologicalSpaceSubtype] u
hud : Dense u
choose :
  ∀ (v : Set X) (hv1 : IsOpen[inst] v) (hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u),
    ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u

Tactic:
choose v hv1 hv2 using huo
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
hud : Dense u
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u

Tactic:
⟨v, hv1, ?_, hv2⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
hud : Dense u
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
refine : Dense v
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ Dense v ∧ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u

Tactic:
refine ⟨v, hv1, ?_, hv2⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
u : Set (↑s : Type u)
hud : Dense u
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
rw :
  ∀ (hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty) {u : Set (↑s : Type u)}
    (hud : ∀ (U : Set (↑s : Type u)), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty) (v : Set X)
    (hv1 : IsOpen[inst] v) (hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u) (U : Set X),
    IsOpen[inst] U → U.Nonempty → (U ∩ v).Nonempty
⊢ Dense v

Tactic:
rw [dense_iff_inter_open] at *

Premises used: dense_iff_inter_open
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
u : Set (↑s : Type u)
hud : ∀ (U : Set (↑s : Type u)), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty
v : Set X
hv1 : IsOpen[inst] v
hv2 : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v = u
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
⊢ ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty

Tactic:
subst hv2
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
⊢ (t ∩ v).Nonempty

Tactic:
nonempty_of_nonempty_preimage (f := (Subtype.val : s → X)) (hud (Subtype.val ⁻¹' t) ?_ ?_)

Premises used: Set.nonempty_of_nonempty_preimage, Set.preimage, Subtype.val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
refine_1 : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)
refine_2 : Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)
⊢ (t ∩ v).Nonempty

Tactic:
refine nonempty_of_nonempty_preimage (f := (Subtype.val : s → X)) (hud (Subtype.val ⁻¹' t) ?_ ?_)
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
⊢ IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)

Tactic:
IsOpen.preimage_val ht

Premises used: IsOpen.preimage_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
⊢ IsOpen[instTopologicalSpaceSubtype] (s ↓∩ t)

Tactic:
exact IsOpen.preimage_val ht

Premises used: IsOpen.preimage_val
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
refine_2 : ∀ (x : X) (hx : x ∈ t ∩ s), Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)
⊢ Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)

Tactic:
obtain ⟨x, hx⟩ := hs t ht ht'
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst] v
t : Set X
ht : IsOpen[inst] t
ht' : t.Nonempty
hud :
  ∀ (U : Set (↑s : Type u)),
    IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' v).Nonempty
x : X
hx : x ∈ t ∩ s
⊢ Set.Nonempty (α := (↑s : Type u)) (s ↓∩ t)

Tactic:
simpa using ⟨⟨x, hx.2⟩, hx.1⟩
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
ht : IsClosed[inst] t
⊢ IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t)

Tactic:
ht.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage