awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
e : α → β
p : β → β → β → Prop
he : DenseRange e
hp : IsClosed[instTopologicalSpaceProd] {q : β × β × β | p q.1 q.2.1 q.2.2}
h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)
⊢ ∀ (b₁ b₂ b₃ : β), p b₁ b₂ b₃

Tactic:
have : ∀ q : β × β × β, p q.1 q.2.1 q.2.2 :=
    isClosed_property (he.prodMap <| he.prodMap he) hp fun _ => h _ _ _
  fun b₁ b₂ b₃ => this ⟨b₁, b₂, b₃⟩

Premises used: DenseRange.prodMap, Prod.mk, Prod.fst, isClosed_property, Prod.snd
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
e : α → β
he : DenseRange e
p : β → Prop
b₀ : β
hp : IsClosed[inst] {b : β | p b}
ih : ∀ (a : α), p (e a)
⊢ p b₀

Tactic:
isClosed_property he hp ih b₀

Premises used: isClosed_property
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
e : α → β
p : β → β → Prop
he : DenseRange e
hp : IsClosed[instTopologicalSpaceProd] {q : β × β | p q.1 q.2}
h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂)
b₁ b₂ : β
⊢ p b₁ b₂

Tactic:
isClosed_property2 he hp h _ _

Premises used: isClosed_property2
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
e : α → β
p : β → β → β → Prop
he : DenseRange e
hp : IsClosed[instTopologicalSpaceProd] {q : β × β × β | p q.1 q.2.1 q.2.2}
h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)
b₁ b₂ b₃ : β
⊢ p b₁ b₂ b₃

Tactic:
isClosed_property3 he hp h _ _ _

Premises used: isClosed_property3
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
inst_2 : T2Space γ
f : α → β
hfd : DenseRange f
g h : β → γ
hg : Continuous[inst, inst_1] g
hh : Continuous[inst, inst_1] h
H : g ∘ f = h ∘ f
⊢ g = h

Tactic:
funext fun y => hfd.induction_on y (isClosed_eq hg hh) <| congr_fun H

Premises used: funext, DenseRange.induction_on
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : (𝓝 x).HasBasis p s
f : α → β
hf : IsDenseInducing f
rw :
  ∀ (h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t) {f : α → β} (hf : IsDenseInducing f) (t : Set β),
    t ∈ 𝓝 (f x) ↔ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ t
⊢ (𝓝 (f x)).HasBasis p fun (i : ι) ↦ closure[inst_1] (f '' s i)

Tactic:
rw [Filter.hasBasis_iff] at h ⊢

Premises used: Filter.hasBasis_iff
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
⊢ T ∈ 𝓝 (f x) ↔ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T

Tactic:
⟨fun hT => ?_, fun hT => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
refine_1 : ∀ (hT : T ∈ 𝓝 (f x)), ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
refine_2 : ∀ (hT : ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T), T ∈ 𝓝 (f x)
⊢ T ∈ 𝓝 (f x) ↔ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T

Tactic:
refine ⟨fun hT => ?_, fun hT => ?_⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
refine_1 :
  ∀ (T' : Set β) (hT₁ : T' ∈ 𝓝 (f x)) (hT₂ : IsClosed[inst_1] T') (hT₃ : T' ⊆ T),
    ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
⊢ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T

Tactic:
obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT

Premises used: exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
rw : f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
⊢ f ⁻¹' T' ∈ 𝓝 x

Tactic:
rw [hf.isInducing.nhds_eq_comap x]

Premises used: Topology.IsInducing.nhds_eq_comap, IsDenseInducing.isInducing
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))

Tactic:
⟨T', hT₁, Subset.rfl⟩

Premises used: Set.Mem, setOf, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))

Tactic:
exact ⟨T', hT₁, Subset.rfl⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ 𝓝 x

Tactic:
have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
      rw [hf.isInducing.nhds_eq_comap x]
      exact ⟨T', hT₁, Subset.rfl⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
refine_1 : ∀ (i : ι) (hi : p i) (hi' : s i ⊆ f ⁻¹' T'), ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
⊢ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T

Tactic:
obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄

Premises used: Iff.mp
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T

Tactic:
⟨i, hi,
        (closure_mono (image_mono hi')).trans
          (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩

Premises used: Set.Subset.trans, closure_minimal, Set.image_mono, HasSubset.Subset.trans, closure_mono, And.intro, Set.image_preimage_subset, Exists.intro
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst_1] T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T

Tactic:
exact
      ⟨i, hi,
        (closure_mono (image_mono hi')).trans
          (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
refine_2 : ∀ (i : ι) (hi : p i) (hi' : closure[inst_1] (f '' s i) ⊆ T), T ∈ 𝓝 (f x)
⊢ T ∈ 𝓝 (f x)

Tactic:
obtain ⟨i, hi, hi'⟩ := hT
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst_1] (f '' s i) ⊆ T
this : closure[inst_1] (f '' s i) ∈ 𝓝 (f x)
⊢ ∀ a ∈ closure[inst_1] (f '' s i), a ∈ T

Tactic:
hi'

Premises used: Set.Subset
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst_1] (f '' s i) ⊆ T
this : closure[inst_1] (f '' s i) ∈ 𝓝 (f x)
h₁ : ∀ (a : β), Membership.mem (γ := Set β) {x : β | x ∈ closure[inst_1] (f '' s i) → x ∈ T} a
h₂ : ∀ a ∈ closure[inst_1] (f '' s i), a ∈ T
⊢ T ∈ 𝓝 (f x)

Tactic:
filter_upwards [this] using hi'
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst_1] (f '' s i) ⊆ T
refine_2 : closure[inst_1] (f '' s i) ∈ 𝓝 (f x)
⊢ T ∈ 𝓝 (f x)

Tactic:
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ (i : ι), p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst_1] (f '' s i) ⊆ T
⊢ s i ∈ 𝓝 x

Tactic:
replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst_1] (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure[inst_1] (f '' s i) ∈ 𝓝 (f x)

Tactic:
hf.closure_image_mem_nhds h

Premises used: IsDenseInducing.closure_image_mem_nhds
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst_1] (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure[inst_1] (f '' s i) ∈ 𝓝 (f x)

Tactic:
exact hf.closure_image_mem_nhds h

Premises used: IsDenseInducing.closure_image_mem_nhds
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
apply : Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F
⊢ AccPt (f x) (Filter.map f F)

Tactic:
apply map_neBot (m := f) (hf := h) |>.mono

Premises used: Filter.NeBot.mono, Filter.map_neBot
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
rw : Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F
⊢ Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F

Tactic:
rw [Filter.map_inf hf2]

Premises used: Filter.map_inf
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
h₁ : Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x
⊢ Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F

Tactic:
gcongr
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
h₁ : ∀ᶠ (x_1 : X) in 𝓝[≠] x, Membership.mem (γ := Set β) {f x}ᶜ (f x_1)
⊢ Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf1.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, Membership.mem (γ := Set β) {f x}ᶜ (f x_1)

Tactic:
simpa [hf2.eq_iff] using eventually_mem_nhdsWithin

Premises used: eventually_mem_nhdsWithin, Function.Injective.eq_iff
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
x : X
⊢ x ∈ derivedSet A ↔ AccPt x (𝓟 A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, derivedSet, AccPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A B : Set X
h : ∀ (x : X), x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B
⊢ derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

Tactic:
ext x
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A B : Set X
x : X
⊢ x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B

Tactic:
simp [derivedSet, ← sup_principal, accPt_sup]

Premises used: Filter.sup_principal, accPt_sup, derivedSet
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A B : Set X
h : A ⊆ B
⊢ derivedSet A ⊆ derivedSet B

Tactic:
fun _ hx ↦ hx.mono <| le_principal_iff.mpr <| mem_principal.mpr h

Premises used: Iff.mpr, AccPt.mono, Filter.le_principal_iff, Set.Mem, setOf, Set.Subset, derivedSet, Filter.mem_principal, AccPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
x : β
hx : x ∈ f '' derivedSet A
⊢ ∃ (x_1 : X), AccPt x_1 (𝓟 A) ∧ f x_1 = x

Tactic:
simp only [Set.mem_image, mem_derivedSet] at hx

Premises used: mem_derivedSet, Set.mem_image
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
x : β
hx : ∃ (x_1 : X), AccPt x_1 (𝓟 A) ∧ f x_1 = x
obtain : ∀ (y : X) (hy1 : AccPt y (𝓟 A)), f y ∈ derivedSet (f '' A)
⊢ x ∈ derivedSet (f '' A)

Tactic:
obtain ⟨y, hy1, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ AccPt (f y) (map f (𝓟 A))

Tactic:
hy1.map hf1.continuousAt hf2

Premises used: Continuous.continuousAt, AccPt.map
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
a : f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))
⊢ f y ∈ derivedSet (f '' A)

Tactic:
convert! hy1.map hf1.continuousAt hf2

Premises used: Continuous.continuousAt, AccPt.map
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
β : Type u_2
inst_1 : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst, inst_1] f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))

Tactic:
simp
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
⊢ derivedSet A ⊆ closure[inst] A

Tactic:
fun _ hx ↦ mem_closure_iff_clusterPt.mpr hx.clusterPt

Premises used: Iff.mpr, mem_closure_iff_clusterPt, Set.Subset, AccPt.clusterPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
rw : ∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A
⊢ IsClosed[inst] A

Tactic:
rw [isClosed_iff_clusterPt]

Premises used: isClosed_iff_clusterPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
by_contra! : ∀ (nh : a ∉ A), False
⊢ a ∈ A

Tactic:
by_contra! nh
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ A = A \ {a}

Tactic:
simp [nh]
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ A = A \ {a}

Tactic:
have : A = A \ {a} := by simp [nh]
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ AccPt a (𝓟 A)

Tactic:
rw [this, ← accPt_principal_iff_clusterPt] at ha

Premises used: accPt_principal_iff_clusterPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
ha₁ : AccPt a (𝓟 A)
⊢ a ∉ A

Tactic:
rw [this, ← accPt_principal_iff_clusterPt] at ha

Premises used: accPt_principal_iff_clusterPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
ha₁ : AccPt a (𝓟 A)
nh₁ : a ∉ A
⊢ A = A \ {a}

Tactic:
rw [this, ← accPt_principal_iff_clusterPt] at ha

Premises used: accPt_principal_iff_clusterPt
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : AccPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False

Tactic:
nh (h ha)
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : AccPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False

Tactic:
exact nh (h ha)
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
h : ∀ (x : X), x ∈ closure[inst] A ↔ x ∈ A ∪ derivedSet A
⊢ closure[inst] A = A ∪ derivedSet A

Tactic:
ext
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Set X
x : X
⊢ x ∈ closure[inst] A ↔ x ∈ A ∪ derivedSet A

Tactic:
simp [closure_eq_cluster_pts, clusterPt_principal]

Premises used: closure_eq_cluster_pts, clusterPt_principal
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
⊢ derivedSet (closure[inst] A) = derivedSet A

Tactic:
le_antisymm (fun x hx => ?_) (derivedSet_mono _ _ subset_closure)

Premises used: subset_closure, le_antisymm, derivedSet_mono
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
refine : ∀ (x : X) (hx : x ∈ derivedSet (closure[inst] A)), x ∈ derivedSet A
⊢ derivedSet (closure[inst] A) = derivedSet A

Tactic:
refine le_antisymm (fun x hx => ?_) (derivedSet_mono _ _ subset_closure)

Premises used: subset_closure, le_antisymm, derivedSet_mono
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : x ∈ derivedSet (closure[inst] A)
rw :
  ∀ (hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty) ⦃i : Set X⦄,
    x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ A).Nonempty
⊢ x ∈ derivedSet A

Tactic:
rw [mem_derivedSet, AccPt, (nhdsWithin_basis_open x {x}ᶜ).inf_principal_neBot_iff] at hx ⊢

Premises used: nhdsWithin_basis_open, Compl.compl, mem_derivedSet, AccPt, Filter.HasBasis.inf_principal_neBot_iff, Singleton.singleton
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
h : ∀ (u : Set X) (hu : x ∈ u ∧ IsOpen[inst] u) (this : (u ∩ {x}ᶜ ∩ closure[inst] A).Nonempty), (u ∩ {x}ᶜ ∩ A).Nonempty
⊢ ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ A).Nonempty

Tactic:
peel hx with u hu _
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
u : Set X
hu : x ∈ u ∧ IsOpen[inst] u
this : (u ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
⊢ IsOpen[inst] u

Tactic:
obtain ⟨-, hu_open⟩ := hu
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
u : Set X
this : (u ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
hu_open : IsOpen[inst] u
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty

Tactic:
mem_closure_iff.mp this.some_mem.2 (u ∩ {x}ᶜ) (hu_open.inter isOpen_compl_singleton)
    this.some_mem.1

Premises used: mem_closure_iff, Compl.compl, isOpen_compl_singleton, Set.Nonempty.some_mem, Inter.inter, And.right, And.left, IsOpen.inter, Iff.mp, Singleton.singleton
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → (i ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
u : Set X
this : (u ∩ {x}ᶜ ∩ closure[inst] A).Nonempty
hu_open : IsOpen[inst] u
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty

Tactic:
exact mem_closure_iff.mp this.some_mem.2 (u ∩ {x}ᶜ) (hu_open.inter isOpen_compl_singleton)
    this.some_mem.1

Premises used: mem_closure_iff, Compl.compl, isOpen_compl_singleton, Set.Nonempty.some_mem, Inter.inter, And.right, And.left, IsOpen.inter, Iff.mp, Singleton.singleton
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
rw : derivedSet (derivedSet (closure[inst] A)) ⊆ derivedSet (closure[inst] A)
⊢ IsClosed[inst] (derivedSet A)

Tactic:
rw [← derivedSet_closure, isClosed_iff_derivedSet_subset]

Premises used: isClosed_iff_derivedSet_subset, derivedSet_closure
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
h : derivedSet (closure[inst] A) ⊆ closure[inst] A
⊢ derivedSet (derivedSet (closure[inst] A)) ⊆ derivedSet (closure[inst] A)

Tactic:
apply derivedSet_mono

Premises used: derivedSet_mono
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
⊢ derivedSet (closure[inst] A) ⊆ closure[inst] A

Tactic:
simp [← isClosed_iff_derivedSet_subset]

Premises used: isClosed_iff_derivedSet_subset
-- Module: Mathlib.Topology.DerivedSet
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
⊢ Preperfect U ↔ U ⊆ derivedSet U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Preperfect, setOf, Set.Subset, derivedSet, AccPt