awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DenseEmbedding
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

Tactic:
eventually_comap.2 ((hg.eventually hs).mono ?_)

Premises used: Iff.mpr, Filter.Eventually.mono, Filter.Tendsto.eventually, Filter.eventually_comap
-- Module: Mathlib.Topology.DenseEmbedding
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)
refine : ∀ (x : β), s (g x) → ∀ (a : α), i a = x → g (i a) ∈ s
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s

Tactic:
refine eventually_comap.2 ((hg.eventually hs).mono ?_)

Premises used: Iff.mpr, Filter.Eventually.mono, Filter.Tendsto.eventually, Filter.eventually_comap
-- Module: Mathlib.Topology.DenseEmbedding
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 : α
hxs : s (g (i x))
⊢ g (i x) ∈ s

Tactic:
hxs

Premises used: Set.Mem
-- Module: Mathlib.Topology.DenseEmbedding
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 : α
hxs : s (g (i x))
⊢ g (i x) ∈ s

Tactic:
exact hxs
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T2Space γ
f : α → γ
g : β → γ
di : IsDenseInducing i
hf : ∀ (x : α), g (i x) = f x
hg : Continuous[inst_1, inst_2] g
⊢ di.extend f = g

Tactic:
funext fun _ => extend_unique_at di (Eventually.of_forall hf) hg.continuousAt

Premises used: Filter.Eventually.of_forall, Continuous.continuousAt, funext, IsDenseInducing.extend_unique_at
-- Module: Mathlib.Topology.DenseEmbedding
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)
set :
  let φ := di.extend f;
  ContinuousAt φ b
⊢ ContinuousAt (di.extend f) b

Tactic:
set φ := di.extend f

Premises used: IsDenseInducing.extend
-- Module: Mathlib.Topology.DenseEmbedding
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
⊢ ∀ (b : β), (comap i (𝓝 b)).NeBot

Tactic:
haveI := di.comap_nhds_neBot
-- Module: Mathlib.Topology.DenseEmbedding
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
this : ∀ V' ∈ 𝓝 (φ b), IsClosed[inst_2] V' → φ ⁻¹' V' ∈ 𝓝 b
⊢ ContinuousAt φ b

Tactic:
simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]

Premises used: ContinuousAt, closed_nhds_basis, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.DenseEmbedding
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
suffices : ∀ V' ∈ 𝓝 (φ b), IsClosed[inst_2] V' → φ ⁻¹' V' ∈ 𝓝 b
⊢ ContinuousAt φ b

Tactic:
suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
    simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
-- Module: Mathlib.Topology.DenseEmbedding
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))}
h : ∀ (a : β), (∃ (c : γ), Tendsto f (comap i (𝓝 a)) (𝓝 c)) → a ∈ V₁
⊢ V₁ ∈ 𝓝 b

Tactic:
filter_upwards [hf]
-- Module: Mathlib.Topology.DenseEmbedding
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)
h h₁ h₂ h₃ : ∀ (hc : Tendsto f (comap i (𝓝 x)) (𝓝 (di.extend f x))), x ∈ V₁
⊢ x ∈ V₁

Tactic:
rwa [← di.extend_eq_of_tendsto hc] at hc

Premises used: IsDenseInducing.extend_eq_of_tendsto
-- Module: Mathlib.Topology.DenseEmbedding
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

Tactic:
have V₁_in : V₁ ∈ 𝓝 b := by
    filter_upwards [hf]
    rintro x ⟨c, hc⟩
    rwa [← di.extend_eq_of_tendsto hc] at hc
-- Module: Mathlib.Topology.DenseEmbedding
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, IsOpen[inst_1] V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V'

Tactic:
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

Premises used: mem_of_mem_nhds, Filter.HasBasis.comap, nhds_basis_opens', and_assoc, Iff.mp, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Topology.DenseEmbedding
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
obtain : ∀ (V₂ : Set β) (V₂_in : V₂ ∈ 𝓝 b) (V₂_op : IsOpen[inst_1] V₂) (hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'), φ ⁻¹' V' ∈ 𝓝 b
⊢ φ ⁻¹' 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

Premises used: nhds
-- Module: Mathlib.Topology.DenseEmbedding
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'
⊢ ∀ a ∈ V₁ ∩ V₂, a ∈ φ ⁻¹' V'

Tactic:
this

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.DenseEmbedding
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
h₁ : ∀ a ∈ V₁ ∩ V₂, a ∈ φ ⁻¹' V'
⊢ φ ⁻¹' V' ∈ 𝓝 b

Tactic:
filter_upwards [inter_mem V₁_in V₂_in] using this

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.DenseEmbedding
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'
suffices : ∀ x ∈ V₁ ∩ V₂, φ x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b

Tactic:
suffices ∀ x ∈ V₁ ∩ V₂, φ x ∈ V' by filter_upwards [inter_mem V₁_in V₂_in] using this
-- Module: Mathlib.Topology.DenseEmbedding
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₂
⊢ V₂ ∈ 𝓝 x

Tactic:
have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂
-- Module: Mathlib.Topology.DenseEmbedding
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
apply : ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
⊢ φ x ∈ V'

Tactic:
apply V'_closed.mem_of_tendsto x_in₁

Premises used: IsClosed.mem_of_tendsto
-- Module: Mathlib.Topology.DenseEmbedding
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
h : V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x : α | (fun (x : α) ↦ f x ∈ V') x}
⊢ ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'

Tactic:
use V₂
-- Module: Mathlib.Topology.DenseEmbedding
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
h₁ : i ⁻¹' V₂ ⊆ {x : α | (fun (x : α) ↦ f x ∈ V') x}
⊢ V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x : α | (fun (x : α) ↦ f x ∈ V') x}

Tactic:
tauto
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace γ
inst_3 : T3Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
⊢ Continuous[inst_1, inst_2] (di.extend f)

Tactic:
continuous_iff_continuousAt.mpr fun _ => di.continuousAt_extend <| univ_mem' hf

Premises used: Iff.mpr, IsDenseInducing.continuousAt_extend, Filter.univ_mem', continuous_iff_continuousAt
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
c : Continuous[inst, inst_1] i
dense : ∀ (x : β), x ∈ closure[inst_1] (range i)
H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ (b : α), i b ∈ t → b ∈ s
a : α
⊢ comap i (𝓝 (i a)) ≤ 𝓝 a

Tactic:
simpa [Filter.le_def] using H a

Premises used: Filter.le_def
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T2Space β
hs : Dense s
a : α
b : β
hf : Tendsto f (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)) (𝓝 b)
⊢ hs.extend (s := s) f a = b

Tactic:
hs.isDenseInducing_val.extend_eq_of_tendsto hf

Premises used: Dense.extend, IsDenseInducing.extend_eq_of_tendsto, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
inst_2 : T2Space β
hs : Dense s
f : (↑s : Type u_1) → β
x : (↑s : Type u_1)
hf : ContinuousAt f x
⊢ hs.extend (s := s) f (↑x : α) = f x

Tactic:
hs.isDenseInducing_val.extend_eq_at hf

Premises used: Dense.extend, IsDenseInducing.extend_eq_at, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T2Space β
hs : Dense s
hf : Continuous[instTopologicalSpaceSubtype, inst_1] f
x : (↑s : Type u_1)
⊢ hs.extend (s := s) f (↑x : α) = f x

Tactic:
hs.extend_eq_at hf.continuousAt

Premises used: Dense.extend_eq_at, Continuous.continuousAt
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T2Space β
a : α
g : α → β
hs : Dense s
hf : ∀ᶠ (x : (↑s : Type u_1)) in comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a), g (↑x : α) = f x
hg : ContinuousAt g a
⊢ hs.extend (s := s) f a = g a

Tactic:
hs.isDenseInducing_val.extend_unique_at hf hg

Premises used: Dense.extend, IsDenseInducing.extend_unique_at, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T2Space β
g : α → β
hs : Dense s
hf : ∀ (x : (↑s : Type u_1)), g (↑x : α) = f x
hg : Continuous[inst, inst_1] g
⊢ hs.extend (s := s) f = g

Tactic:
hs.isDenseInducing_val.extend_unique hf hg

Premises used: IsDenseInducing.extend_unique, Dense.extend, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T3Space β
a : α
hs : Dense s
hf : ∀ᶠ (x : α) in 𝓝 a, ∃ (b : β), Tendsto f (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 x)) (𝓝 b)
⊢ ContinuousAt (hs.extend (s := s) f) a

Tactic:
hs.isDenseInducing_val.continuousAt_extend hf

Premises used: IsDenseInducing.continuousAt_extend, Dense.extend, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T3Space β
hs : Dense s
hf : ∀ (a : α), ∃ (b : β), Tendsto f (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)) (𝓝 b)
⊢ Continuous[inst, inst_1] (hs.extend (s := s) f)

Tactic:
hs.isDenseInducing_val.continuous_extend hf

Premises used: Dense.extend, IsDenseInducing.continuous_extend, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
c : Continuous[inst, inst_1] e
dense : DenseRange e
injective : Function.Injective e
H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ (b : α), e b ∈ t → b ∈ s
⊢ IsDenseEmbedding e

Tactic:
{ IsDenseInducing.mk' e c dense H with injective }

Premises used: IsDenseEmbedding.mk, IsDenseInducing.mk'
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
⊢ IsDenseInducing e

Tactic:
de.toIsDenseInducing

Premises used: IsDenseEmbedding.toIsDenseInducing
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
x y : α
⊢ e x = e y ↔ x = y

Tactic:
de.injective.eq_iff

Premises used: Function.Injective.eq_iff, IsDenseEmbedding.injective
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
inst_2 : SeparableSpace α
de : IsDenseEmbedding e
⊢ SeparableSpace β

Tactic:
de.isDenseInducing.separableSpace

Premises used: IsDenseEmbedding.isDenseInducing, IsDenseInducing.separableSpace
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x_1 : { x : α // p x }
x : α
hx : p x
⊢ 𝓝 (Subtype.mk (p := fun (x : α) ↦ p x) x hx) =
    comap (β := { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) }) (subtypeEmb p e)
      (𝓝 (subtypeEmb p e (Subtype.mk (p := fun (x : α) ↦ p x) x hx)))

Tactic:
simp [subtypeEmb, nhds_subtype_eq_comap, de.isInducing.nhds_eq_comap, comap_comap,
        Function.comp_def]

Premises used: IsDenseEmbedding.toIsDenseInducing, Topology.IsInducing.nhds_eq_comap, IsDenseInducing.isInducing, nhds_subtype_eq_comap, Function.comp_def, Filter.comap_comap, IsDenseEmbedding.subtypeEmb
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
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)
⊢ Eq (α := Set { x : β // x ∈ closure[inst_1] (e '' {x : α | p x}) })
    (closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e))) univ

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Topology.DenseEmbedding
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 β) (closure[inst_1] (range fun (x : (↑{x : α | p x} : Type u_1)) ↦ e (↑x : α))) x

Tactic:
rw [image_eq_range] at hx

Premises used: Set.image_eq_range
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx_1 : x ∈ closure[inst_1] (e '' {x : α | p x})
hx : Membership.mem (γ := Set β) (closure[inst_1] (range fun (x : (↑{x : α | p x} : Type u_1)) ↦ e (↑x : α))) 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_1) ↔
    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_1)

Tactic:
simpa [closure_subtype, ← range_comp, (· ∘ ·)]

Premises used: Set.range_comp, Function.comp, closure_subtype
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
s : Set α
⊢ Dense (e '' s) ↔ Dense s

Tactic:
de.isDenseInducing.dense_image

Premises used: IsDenseEmbedding.isDenseInducing, IsDenseInducing.dense_image
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_5
inst : TopologicalSpace α
⊢ IsDenseEmbedding.{u_5, u_5} (α := α) id

Tactic:
{ IsEmbedding.id with dense := denseRange_id }

Premises used: IsDenseEmbedding.mk, IsDenseInducing.mk, Topology.IsEmbedding.id, Topology.IsEmbedding.injective, Topology.IsEmbedding.toIsInducing, denseRange_id
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsDenseEmbedding.{u_1, u_1} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
{ IsEmbedding.subtypeVal with dense := hs.denseRange_val }

Premises used: IsDenseEmbedding.mk, IsDenseInducing.mk, Topology.IsEmbedding.injective, Dense.denseRange_val, Topology.IsEmbedding.toIsInducing, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.DenseEmbedding
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)
⊢ 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
-- Module: Mathlib.Topology.DenseEmbedding
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)
this : Subset.{u_2} (α := Set β) univ {b : β | p b}
⊢ ∀ (b : β), p b

Tactic:
simpa only [univ_subset_iff, eq_univ_iff_forall, mem_setOf]

Premises used: Set.univ_subset_iff, Set.eq_univ_iff_forall, Set.mem_setOf
-- 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:
have : ∀ q : β × β, p q.1 q.2 := isClosed_property (he.prodMap he) hp fun _ => h _ _
  fun b₁ b₂ => this ⟨b₁, b₂⟩

Premises used: DenseRange.prodMap, Prod.mk, Prod.fst, isClosed_property, Prod.snd