awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : (↑s : Type u_1)
rw : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ t ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)
rw₁ rw₂ : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] (↑a : α)

Tactic:
rw [← map_nhds_subtype_val, mem_map]

Premises used: Filter.mem_map, map_nhds_subtype_val
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : (↑s : Type u_1)
P : α → Prop
⊢ (∀ᶠ (x : (↑s : Type u_1)) in 𝓝 a, P (↑x : α)) ↔ ∀ᶠ (x : α) in 𝓝[s] (↑a : α), P x

Tactic:
preimage_coe_mem_nhds_subtype

Premises used: Set.Mem, preimage_coe_mem_nhds_subtype, Filter.Eventually, setOf, Set.preimage
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : (↑s : Type u_1)
P : α → Prop
⊢ (∃ᶠ (x : (↑s : Type u_1)) in 𝓝 a, P (↑x : α)) ↔ ∃ᶠ (x : α) in 𝓝[s] (↑a : α), P x

Tactic:
eventually_nhds_subtype_iff s a (¬ P ·) |>.not

Premises used: Iff.not, Filter.Frequently, eventually_nhds_subtype_iff, Not
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
rw :
  Tendsto (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l ↔
    Tendsto (s.restrict (π := fun (a : α) ↦ β) f) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict (π := fun (a : α) ↦ β) f) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l

Tactic:
rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]

Premises used: nhdsWithin_eq_map_subtype_coe, Filter.tendsto_map'_iff
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l ↔
    Tendsto (s.restrict (π := fun (a : α) ↦ β) f) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l

Tactic:
rfl
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
rw :
  (∃ᶠ (b : α) in 𝓝 (↑a : α), ∃ (a : (↑s : Type u_1)), (↑a : α) = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in 𝓝 (↑a : α),
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = b ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in 𝓝[t] (↑a : α), ∃ (h : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h ∈ J

Tactic:
rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
    clusterPt_principal_iff_frequently,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Topology.IsInducing.nhds_eq_comap, nhdsWithin_eq_map_subtype_coe, Filter.frequently_comap, Filter.frequently_map, Subtype.prop, clusterPt_principal_iff_frequently, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
h :
  ∀ᶠ (x : α) in 𝓝 (↑a : α),
    (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
⊢ (∃ᶠ (b : α) in 𝓝 (↑a : α), ∃ (a : (↑s : Type u_1)), (↑a : α) = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in 𝓝 (↑a : α),
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = b ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J

Tactic:
apply frequently_congr

Premises used: Filter.frequently_congr
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
h :
  ∀ (x : α),
    (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
⊢ ∀ᶠ (x : α) in 𝓝 (↑a : α),
    (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J

Tactic:
apply Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
x : α
h :
  (∃ (x_1 : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯ ∈ J) ↔
    ∃ (x_1 : x ∈ t) (h : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯ ∈ J
⊢ (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
    ∃ (a : { x : α // x ∈ t }),
      (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J

Tactic:
simp only [SetCoe.exists, exists_and_left, exists_eq_left]

Premises used: exists_and_left, exists_eq_left, SetCoe.exists
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
x : α
⊢ (∃ (x_1 : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯ ∈ J) ↔
    ∃ (x_1 : x ∈ t) (h : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯ ∈ J

Tactic:
⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩

Premises used: Iff.mpr, Iff.of_eq, Membership.mem, Exists, _private.0.clusterPt_principal_subtype_iff_frequently.match_3, _private.0.clusterPt_principal_subtype_iff_frequently.match_4, Subtype.mk, Iff.intro, Exists.intro, Eq.refl
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
x : α
⊢ (∃ (x_1 : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯ ∈ J) ↔
    ∃ (x_1 : x ∈ t) (h : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯ ∈ J

Tactic:
exact ⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
h : s ⊆ s'
⊢ 𝓝ˢ[t] s ≤ 𝓝ˢ[t] s'

Tactic:
inf_le_inf_right _ <| nhdsSet_mono h

Premises used: Set.Mem, nhdsSet_mono, inf_le_inf_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t t' : Set α
h : t ⊆ t'
⊢ 𝓝ˢ[t] s ≤ 𝓝ˢ[t'] s

Tactic:
inf_le_inf_left _ <| principal_mono.2 h

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, inf_le_inf_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_5
p : ι → Prop
s' : ι → Set α
s : Set α
h : (𝓝ˢ s).HasBasis p s'
t : Set α
⊢ (𝓝ˢ[t] s).HasBasis p fun (i : ι) ↦ s' i ∩ t

Tactic:
h.inf_principal t

Premises used: nhdsSetWithin, Filter.HasBasis.inf_principal
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
⊢ (𝓝ˢ[t] s).HasBasis (fun (u : Set α) ↦ IsOpen[inst] u ∧ s ⊆ u) fun (u : Set α) ↦ u ∩ t

Tactic:
nhdsSetWithin_hasBasis (hasBasis_nhdsSet s) t

Premises used: nhdsSetWithin_hasBasis, hasBasis_nhdsSet
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t u : Set α
⊢ u ∈ 𝓝ˢ[t] s ↔ ∃ (v : Set α), IsOpen[inst] v ∧ s ⊆ v ∧ v ∩ t ⊆ u

Tactic:
simpa [and_assoc] using (nhdsSetWithin_basis_open s t).mem_iff

Premises used: Filter.HasBasis.mem_iff, nhdsSetWithin_basis_open, and_assoc
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s : Set α
⊢ 𝓝ˢ[s] {x} = 𝓝[s] x

Tactic:
simp [nhdsSetWithin, nhdsWithin]

Premises used: nhdsWithin, nhdsSetWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[univ] s = 𝓝ˢ s

Tactic:
simp [nhdsSetWithin]

Premises used: nhdsSetWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
⊢ s ∈ 𝓝ˢ t ↔ ∃ u ⊆ s, IsOpen[inst] u ∧ t ⊆ u

Tactic:
simp [← nhdsSetWithin_univ, mem_nhdsSetWithin, and_comm, and_assoc]

Premises used: nhdsSetWithin_univ, and_comm, and_assoc, mem_nhdsSetWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] univ = 𝓟 s

Tactic:
simp [nhdsSetWithin]

Premises used: nhdsSetWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] s = 𝓟 s

Tactic:
simp [nhdsSetWithin, principal_le_nhdsSet]

Premises used: nhdsSetWithin, principal_le_nhdsSet
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : t ⊆ s
⊢ 𝓝ˢ[t] s = 𝓟 t

Tactic:
simp [nhdsSetWithin, (principal_mono.2 h).trans principal_le_nhdsSet]

Premises used: Iff.mpr, Filter.principal_mono, nhdsSetWithin, LE.le.trans, principal_le_nhdsSet
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[∅] s = ⊥

Tactic:
simp [nhdsSetWithin]

Premises used: nhdsSetWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] ∅ = ⊥

Tactic:
simp [nhdsSetWithin]

Premises used: nhdsSetWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
⊢ 𝓟 (s ∩ t) ≤ 𝓝ˢ[t] s

Tactic:
simpa [nhdsSetWithin] using inf_le_of_left_le (b := 𝓟 t) <| principal_le_nhdsSet

Premises used: inf_le_of_left_le, nhdsSetWithin, principal_le_nhdsSet
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s s' : Set α
t t' : Set β
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) ≤ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t

Tactic:
simpa [nhdsSetWithin, ← prod_inf_prod] using inf_le_of_left_le <| nhdsSet_prod_le _ _

Premises used: Filter.prod_inf_prod, inf_le_of_left_le, nhdsSetWithin, nhdsSet_prod_le
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
simp_rw :
  (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u

Tactic:
simp_rw [mem_nhdsSet_iff_exists, isOpen_induced_iff]

Premises used: mem_nhdsSet_iff_exists, isOpen_induced_iff
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
⟨fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_, fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_⟩

Premises used: Exists, HasSubset.Subset, And, Set.preimage, _private.0.mem_nhdsSet_induced.match_3, _private.0.mem_nhdsSet_induced.match_2, Iff.intro, Set.image, IsOpen, Eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
refine_1 :
  (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) →
    ∀ (v : Set α) (v' : Set β) (hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v) (hv : s ⊆ v ∧ v ⊆ u),
      ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
refine_2 :
  (∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u) →
    ∀ (v v' : Set β) (hv' : IsOpen[t] v' ∧ f '' s ⊆ v' ∧ v' ⊆ v) (hv : f ⁻¹' v ⊆ u),
      ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
⊢ (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
refine ⟨fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_, fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
⟨v', ⟨v', hv'.1, ?_, subset_rfl⟩, hv'.2.trans_subset hv.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Eq.trans_subset, subset_rfl
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
refine_1 : f '' s ⊆ v'
⊢ ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u

Tactic:
refine ⟨v', ⟨v', hv'.1, ?_, subset_rfl⟩, hv'.2.trans_subset hv.2⟩
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ f '' v ⊆ v'

Tactic:
simp [hv']
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ f '' s ⊆ v'

Tactic:
exact (image_mono hv.1).trans (by simp [hv'])

Premises used: Set.image_mono, HasSubset.Subset.trans, And.left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
v v' : Set β
hv' : IsOpen[t] v' ∧ f '' s ⊆ v' ∧ v' ⊆ v
hv : f ⁻¹' v ⊆ u
⊢ ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u

Tactic:
⟨f ⁻¹' v', ⟨v', hv'.1, rfl⟩, image_subset_iff.1 hv'.2.1, (preimage_mono hv'.2.2).trans hv⟩

Premises used: HasSubset.Subset.trans, Set.preimage_mono, And.right, Set.preimage, And.left, And.intro, Exists.intro, Iff.mp, Set.image_subset_iff, rfl
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
v v' : Set β
hv' : IsOpen[t] v' ∧ f '' s ⊆ v' ∧ v' ⊆ v
hv : f ⁻¹' v ⊆ u
⊢ ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u

Tactic:
exact ⟨f ⁻¹' v', ⟨v', hv'.1, rfl⟩, image_subset_iff.1 hv'.2.1, (preimage_mono hv'.2.2).trans hv⟩
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (s_1 : Set α), s_1 ∈ 𝓝ˢ s ↔ s_1 ∈ comap f (𝓝ˢ (f '' s))
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Tactic:
ext s
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s_1 s : Set α
h : (∃ v ∈ 𝓝ˢ (f '' s_1), f ⁻¹' v ⊆ s) ↔ s ∈ comap f (𝓝ˢ (f '' s_1))
h₁ h₂ : (∃ v ∈ 𝓝ˢ (f '' s_1), f ⁻¹' v ⊆ s) ↔ ∃ t_1 ∈ 𝓝ˢ (f '' s_1), f ⁻¹' t_1 ⊆ s
⊢ s ∈ 𝓝ˢ s_1 ↔ s ∈ comap f (𝓝ˢ (f '' s_1))

Tactic:
rw [mem_nhdsSet_induced, mem_comap]

Premises used: Filter.mem_comap, mem_nhdsSet_induced
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
rw : map f (comap f (𝓝ˢ (f '' s))) = 𝓝ˢ[range f] (f '' s)
rw₁ : 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ[range f] (f '' s)
rw₂ rw₃ : 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ (f '' s) ⊓ 𝓟 (range f)
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)

Tactic:
rw [nhdsSet_induced, Filter.map_comap, nhdsSetWithin]

Premises used: Filter.map_comap, nhdsSetWithin, nhdsSet_induced
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)

Tactic:
hf.eq_induced ▸ map_nhdsSet_induced_eq s

Premises used: map_nhdsSet_induced_eq, Eq.rec, Eq.symm, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t : Set (↑s : Type u_1)
rw :
  𝓝ˢ[range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))]
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) =
    𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
rw₁ rw₂ : 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) = 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝ˢ t) = 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

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

Premises used: Subtype.range_val, Topology.IsInducing.map_nhdsSet_eq, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t u : Set (↑s : Type u_1)
rw : u ∈ 𝓝ˢ t ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝ˢ t)
rw₁ rw₂ : u ∈ 𝓝ˢ t ↔ u ∈ 𝓝ˢ t
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u ∈ 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
rw [← map_nhdsSet_subtype_val, image_mem_map_iff Subtype.val_injective]

Premises used: Subtype.val_injective, Filter.image_mem_map_iff, map_nhdsSet_subtype_val
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
    CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]

Premises used: CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact, CompleteLattice.isSupFiniteCompact_iff_all_elements_compact, TopologicalSpace.NoetherianSpace
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
forall_congr' Opens.isCompactElement_iff

Premises used: TopologicalSpace.Opens.isCompactElement_iff, forall_congr'
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
exact forall_congr' Opens.isCompactElement_iff

Premises used: TopologicalSpace.Opens.isCompactElement_iff, forall_congr'
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : NoetherianSpace α
⊢ CompactSpace α

Tactic:
⟨(noetherianSpace_iff_opens α).mp h ⊤⟩

Premises used: CompactSpace.mk, TopologicalSpace.noetherianSpace_iff_opens, Iff.mp, Top.top
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
⊢ IsCompact s

Tactic:
isCompact_iff_finite_subcover.2 fun U hUo hs => ?_

Premises used: Iff.mpr, isCompact_iff_finite_subcover
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
refine :
  ∀ {ι : Type u_1} (U : ι → Set α) (hUo : ∀ (i : ι), IsOpen[inst] (U i)) (hs : s ⊆ ⋃ (i : ι), U i),
    ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
⊢ IsCompact s

Tactic:
refine isCompact_iff_finite_subcover.2 fun U hUo hs => ?_

Premises used: Iff.mpr, isCompact_iff_finite_subcover
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
ι : Type u_1
U : ι → Set α
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hs : s ⊆ ⋃ (i : ι), U i
rcases :
  ∀ (t : Finset ι) (ht : (↑{ carrier := ⋃ (i : ι), U i, is_open' := ⋯ : Opens α } : Set α) ⊆ ⋃ i ∈ t, U i),
    ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
rcases ((noetherianSpace_iff_opens α).mp ‹_› ⟨⋃ i, U i, isOpen_iUnion hUo⟩).elim_finite_subcover U
    hUo Set.Subset.rfl with ⟨t, ht⟩

Premises used: TopologicalSpace.noetherianSpace_iff_opens, IsCompact.elim_finite_subcover, Set.Subset.rfl, isOpen_iUnion, TopologicalSpace.Opens.mk, Iff.mp, Set.iUnion
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
ι : Type u_1
U : ι → Set α
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hs : s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : (↑{ carrier := ⋃ (i : ι), U i, is_open' := ⋯ : Opens α } : Set α) ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
⟨t, hs.trans ht⟩

Premises used: HasSubset.Subset.trans, Exists.intro
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
ι : Type u_1
U : ι → Set α
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hs : s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : (↑{ carrier := ⋃ (i : ι), U i, is_open' := ⋯ : Opens α } : Set α) ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, hs.trans ht⟩
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NoetherianSpace α
i : β → α
hi : IsInducing i
⊢ NoetherianSpace β

Tactic:
(noetherianSpace_iff_opens _).2 fun _ => hi.isCompact_iff.2 (NoetherianSpace.isCompact _)

Premises used: Iff.mpr, TopologicalSpace.noetherianSpace_iff_opens, SetLike.coe, Set.image, Topology.IsInducing.isCompact_iff, TopologicalSpace.NoetherianSpace.isCompact
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NoetherianSpace α
s : Set α
⊢ NoetherianSpace.{u_1} (↑s : Type u_1)

Tactic:
IsInducing.subtypeVal.noetherianSpace

Premises used: Topology.IsInducing.noetherianSpace, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace α

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ WellFoundedLT.{u_1} (Closeds α)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw : (WellFounded fun (x1 x2 : Opens α) ↦ x2 < x1) ↔ WellFounded fun (x1 x2 : Closeds α) ↦ x1 < x2
⊢ NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)

Tactic:
simp_rw [isWellFounded_iff]

Premises used: isWellFounded_iff
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (WellFounded fun (x1 x2 : Opens α) ↦ x2 < x1) ↔ WellFounded fun (x1 x2 : Closeds α) ↦ x1 < x2

Tactic:
Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm

Premises used: Function.Surjective.wellFounded_iff, OrderIso.lt_iff_lt, TopologicalSpace.Opens.compl_bijective, And.right, OrderIso.compl, Iff.symm, Set
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (WellFounded fun (x1 x2 : Opens α) ↦ x2 < x1) ↔ WellFounded fun (x1 x2 : Closeds α) ↦ x1 < x2

Tactic:
exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm

Premises used: Function.Surjective.wellFounded_iff, TopologicalSpace.Opens.compl_bijective, And.right
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)

Tactic:
tfae_have 1 ↔ 2 := by
    simp_rw [isWellFounded_iff]
    exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm