awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
⊢ ∃ (a : α), i a ∈ s
have rcases : ∀ (a : α) (ha : i a ∈ s), ∃ (a : α), i a ∈ s
Tactic: rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 (di.extend f (i a)))
have rw : Tendsto f (𝓝 a) (𝓝 ((𝓝 a).limUnder f))
Tactic: rw [IsDenseInducing.extend, ← di.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
⊢ di.extend f (i a) = f a
have rcases : ∀ (b : γ) (hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)), di.extend f (i a) = f a
Tactic: rcases hf (i a) with ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ di.extend f (i a) = f a
have refine : Tendsto f (𝓝 a) (𝓝 b)
Tactic: refine di.extend_eq_at' b ?_
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)
have rwa : ∀ (hb : Tendsto f (𝓝 a) (𝓝 b)), Tendsto f (𝓝 a) (𝓝 b)
Tactic: rwa [← di.isInducing.nhds_eq_comap] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
b : β
f : α → γ
g : β → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
⊢ di.extend f b = g b
have refine : ∀ (s : Set γ) (hs : s ∈ 𝓝 (g b)), f ⁻¹' s ∈ comap i (𝓝 b)
Tactic: refine di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
b : β
f : α → γ
g : β → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ f ⁻¹' s ∈ comap i (𝓝 b)
have suffices : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
Tactic: suffices ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s from
    hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
b : β
g : β → γ
di : IsDenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
have refine : ∀ (x : β), s (g x) → ∀ (a : α), i a = x → g (i a) ∈ s
Tactic: refine eventually_comap.2 ((hg.eventually hs).mono ?_)
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
⊢ ContinuousAt φ b
have this : ∀ (b : β), (comap i (𝓝 b)).NeBot
Tactic: haveI := di.comap_nhds_neBot
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
⊢ ContinuousAt φ b
have suffices : ∀ V' ∈ 𝓝 (φ b), IsClosed[inst_2] V' → φ ⁻¹' V' ∈ 𝓝 b
Tactic: suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
    simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ V₁ ∈ 𝓝 b
have h : ∀ (a : β), (∃ (c : γ), Tendsto f (comap i (𝓝 a)) (𝓝 c)) → a ∈ V₁
Tactic: filter_upwards [hf]
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
x : β
c : γ
hc : Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ x ∈ V₁
have h : ∀ (hc : Tendsto f (comap i (𝓝 x)) (𝓝 (di.extend f x))), x ∈ V₁
Tactic: rwa [← di.extend_eq_of_tendsto hc] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ φ ⁻¹' V' ∈ 𝓝 b
have V₁_in : V₁ ∈ 𝓝 b
Tactic: have V₁_in : V₁ ∈ 𝓝 b := by
    filter_upwards [hf]
    rintro x ⟨c, hc⟩
    rwa [← di.extend_eq_of_tendsto hc] at hc
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
⊢ φ ⁻¹' V' ∈ 𝓝 b
have obtain : ∀ (V₂ : Set β) (V₂_in : V₂ ∈ 𝓝 b) (V₂_op : IsOpen[inst_1] V₂) (hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'), φ ⁻¹' V' ∈ 𝓝 b
Tactic: obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by
    simpa [and_assoc] using
      ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this_1 : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
this : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
have h : ∀ (a : β), Membership.mem (γ := Set β) {x : β | x ∈ V₁ ∩ V₂ → x ∈ φ ⁻¹' V'} a
Tactic: filter_upwards [inter_mem V₁_in V₂_in] using this
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this_1 : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
this : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
h : ∀ (a : β), Membership.mem (γ := Set β) {x : β | x ∈ V₁ ∩ V₂ → x ∈ φ ⁻¹' V'} a
⊢ φ ⁻¹' V' ∈ 𝓝 b
have h₁ : ∀ a ∈ V₁ ∩ V₂, a ∈ φ ⁻¹' V'
Tactic: filter_upwards [inter_mem V₁_in V₂_in] using this
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
have suffices : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
Tactic: suffices ∀ x ∈ V₁ ∩ V₂, φ x ∈ V' by filter_upwards [inter_mem V₁_in V₂_in] using this
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
⊢ φ x ∈ V'
have hV₂x : V₂ ∈ 𝓝 x
Tactic: have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ φ x ∈ V'
have apply : ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
Tactic: apply V'_closed.mem_of_tendsto x_in₁
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
have h : V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x : α | (fun (x : α) ↦ f x ∈ V') x}
Tactic: use V₂
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ (c : γ), Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : (b : β) → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst_2] V'
V₁ : Set β := {x : β | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst_1] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x h : V₂ ∈ 𝓝 x
⊢ V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x : α | (fun (x : α) ↦ f x ∈ V') x}
have h₁ : i ⁻¹' V₂ ⊆ {x : α | (fun (x : α) ↦ f x ∈ V') x}
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
⊢ Eq (α := Set { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) })
    (closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e))) univ
have h : ∀ (x : β) (hx : x ∈ closure[inst_1] (e '' {x : α | p x})),
  Membership.mem (γ := Set { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) })
      (closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1] (e '' {x : α | p x})) x hx) ↔
    Membership.mem (γ := Set { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) }) univ
      (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1] (e '' {x : α | p x})) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure[inst_1] (e '' {x : α | p x})
⊢ Membership.mem (γ := Set { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) })
      (closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1] (e '' {x : α | p x})) x hx) ↔
    Membership.mem (γ := Set { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) }) univ
      (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1] (e '' {x : α | p x})) x hx)
have hx₁ : Membership.mem (γ := Set β) (closure[inst_1] (range fun (x : (↑{x : α | p x} : Type u_1)) ↦ e (↑x : α))) x
Tactic: rw [image_eq_range] at hx
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
e : α → β
p : β → Prop
he : DenseRange e
hp : IsClosed[inst] {x : β | p x}
h : ∀ (a : α), p (e a)
⊢ ∀ (b : β), p b
have this : Subset.{u_2} (α := Set β) univ {b : β | p b}
Tactic: have : univ ⊆ { b | p b } :=
    calc
      univ = closure (range e) := he.closure_range.symm
      _ ⊆ closure { b | p b } := closure_mono <| range_subset_iff.mpr h
      _ = _ := hp.closure_eq
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
⊢ (𝓝 (f x)).HasBasis p fun (i : ι) ↦ closure[inst_1] (f '' s i)
have 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
Tactic: rw [Filter.hasBasis_iff] at h ⊢
Cleared hypotheses: h, f, hf
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
have refine_1 : ∀ (hT : T ∈ 𝓝 (f x)), ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
Tactic: refine ⟨fun hT => ?_, fun hT => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
⊢ T ∈ 𝓝 (f x) ↔ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
have refine_2 : ∀ (hT : ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T), T ∈ 𝓝 (f x)
Tactic: refine ⟨fun hT => ?_, fun hT => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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)
⊢ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
have 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
Tactic: obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
have rw : f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
Tactic: rw [hf.isInducing.nhds_eq_comap x]
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
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
⊢ ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
have hT₄ : f ⁻¹' T' ∈ 𝓝 x
Tactic: have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
      rw [hf.isInducing.nhds_eq_comap x]
      exact ⟨T', hT₁, Subset.rfl⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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 : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
have refine_1 : ∀ (i : ι) (hi : p i) (hi' : s i ⊆ f ⁻¹' T'), ∃ (i : ι), p i ∧ closure[inst_1] (f '' s i) ⊆ T
Tactic: obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
⊢ T ∈ 𝓝 (f x)
have refine_2 : ∀ (i : ι) (hi : p i) (hi' : closure[inst_1] (f '' s i) ⊆ T), T ∈ 𝓝 (f x)
Tactic: obtain ⟨i, hi, hi'⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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)
⊢ T ∈ 𝓝 (f x)
have h₁ : ∀ (a : β), Membership.mem (γ := Set β) {x : β | x ∈ closure[inst_1] (f '' s i) → x ∈ T} a
Tactic: filter_upwards [this] using hi'
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
⊢ T ∈ 𝓝 (f x)
have h₂ : ∀ a ∈ closure[inst_1] (f '' s i), a ∈ T
Tactic: filter_upwards [this] using hi'
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
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
⊢ T ∈ 𝓝 (f x)
have refine_2 : closure[inst_1] (f '' s i) ∈ 𝓝 (f x)
Tactic: suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
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
⊢ closure[inst_1] (f '' s i) ∈ 𝓝 (f x)
have h₁ : s i ∈ 𝓝 x
Tactic: replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ AccPt (f x) (Filter.map f F)
have apply : Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F
Tactic: apply map_neBot (m := f) (hf := h) |>.mono
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F
have rw : Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F
Tactic: rw [Filter.map_inf hf2]
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F
have h₁ : Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
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
⊢ Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x
have h₁ : ∀ᶠ (x_1 : X) in 𝓝[≠] x, Membership.mem (γ := Set β) {f x}ᶜ (f x_1)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf1.continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.DerivedSet (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
A B : Set X
⊢ derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B
have h : ∀ (x : X), x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B
Tactic: ext x