awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
refine : f ⁻¹' ⋃₀ (g '' S) = ⋃₀ S
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S

Tactic:
refine ⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
rw : Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ S, f ⁻¹' g y) (⋃ i ∈ S, i)
⊢ f ⁻¹' ⋃₀ (g '' S) = ⋃₀ S

Tactic:
rw [preimage_sUnion, biUnion_image, sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion, Set.preimage_sUnion, Set.biUnion_image
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ S, f ⁻¹' g y) (⋃ i ∈ S, i)

Tactic:
iUnion₂_congr hfg

Premises used: Set.iUnion₂_congr
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ S, f ⁻¹' g y) (⋃ i ∈ S, i)

Tactic:
exact iUnion₂_congr hfg

Premises used: Set.iUnion₂_congr
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace X
s : Set (Set Y)
h : ∀ t_1 ∈ s, IsOpen[t] (f ⁻¹' t_1)
⊢ IsOpen[t] (f ⁻¹' ⋃₀ s)

Tactic:
simpa only [preimage_sUnion] using isOpen_biUnion h

Premises used: Set.preimage_sUnion, isOpen_biUnion
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
t : TopologicalSpace X
⊢ instTopologicalSpace X t = TopologicalSpace.coinduced (toTopology t) t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Defs.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SequentialSpace X
s : Set X
hs : IsSeqClosed s
⊢ IsClosed[inst] s

Tactic:
SequentialSpace.isClosed_of_seq s hs

Premises used: SequentialSpace.isClosed_of_seq
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsDenseInducing.{u_1, u_1} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
⟨IsInducing.subtypeVal, hs.denseRange_val⟩

Premises used: IsDenseInducing.mk, Dense.denseRange_val, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
⊢ IsInducing i

Tactic:
di.toIsInducing

Premises used: IsDenseInducing.toIsInducing
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
⊢ ∀ (a : α), 𝓝 a = comap i (𝓝 (i a))

Tactic:
di.isInducing.nhds_eq_comap

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 β
i : α → β
di : IsDenseInducing i
⊢ Continuous[inst, inst_1] i

Tactic:
di.isInducing.continuous

Premises used: IsDenseInducing.isInducing, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
⊢ closure[inst_1] (range i) = univ

Tactic:
di.dense.closure_range

Premises used: DenseRange.closure_range, IsDenseInducing.dense
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : PreconnectedSpace α
di : IsDenseInducing i
⊢ PreconnectedSpace β

Tactic:
di.dense.preconnectedSpace di.continuous

Premises used: DenseRange.preconnectedSpace, IsDenseInducing.dense, IsDenseInducing.continuous
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : s ∈ 𝓝 a
⊢ ∃ (i_1 : Set β), (i a ∈ i_1 ∧ IsOpen[inst_1] i_1) ∧ i ⁻¹' i_1 ⊆ s

Tactic:
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs

Premises used: IsDenseInducing.nhds_eq_comap, Filter.HasBasis.mem_iff, Filter.HasBasis.comap, nhds_basis_opens
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : ∃ (i_1 : Set β), (i a ∈ i_1 ∧ IsOpen[inst_1] i_1) ∧ i ⁻¹' i_1 ⊆ s
rcases : ∀ (U : Set β) (sub : i ⁻¹' U ⊆ s) (haU : i a ∈ U) (hUo : IsOpen[inst_1] U), closure[inst_1] (i '' s) ∈ 𝓝 (i a)
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i a)

Tactic:
rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst_1] U
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i a)

Tactic:
mem_of_superset (hUo.mem_nhds haU) ?_

Premises used: IsOpen.mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst_1] U
refine : U ⊆ closure[inst_1] (i '' s)
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i a)

Tactic:
refine mem_of_superset (hUo.mem_nhds haU) ?_

Premises used: IsOpen.mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst_1] U
⊢ U ⊆ closure[inst_1] (i '' i ⁻¹' U)

Tactic:
di.dense.subset_closure_image_preimage_of_isOpen hUo

Premises used: DenseRange.subset_closure_image_preimage_of_isOpen, IsDenseInducing.dense
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst_1] U
⊢ closure[inst_1] (i '' i ⁻¹' U) ⊆ closure[inst_1] (i '' s)

Tactic:
closure_mono (image_mono sub)

Premises used: Set.image_mono, closure_mono
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst_1] U
⊢ U ⊆ closure[inst_1] (i '' s)

Tactic:
calc
    U ⊆ closure (i '' i ⁻¹' U) := di.dense.subset_closure_image_preimage_of_isOpen hUo
    _ ⊆ closure (i '' s) := closure_mono (image_mono sub)

Premises used: Set.image_mono, closure_mono, DenseRange.subset_closure_image_preimage_of_isOpen, IsDenseInducing.dense, closure, Set.preimage, Set.image
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s

Tactic:
⟨fun H x => ?_, di.dense.dense_image di.continuous⟩

Premises used: IsDenseInducing.dense, IsDenseInducing.continuous, Iff.intro, DenseRange.dense_image
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
refine : ∀ (H : Dense (i '' s)) (x : α), x ∈ closure[inst] s
⊢ Dense (i '' s) ↔ Dense s

Tactic:
refine ⟨fun H x => ?_, di.dense.dense_image di.continuous⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
rw : Membership.mem (γ := Set α) univ x
⊢ x ∈ closure[inst] s

Tactic:
rw [di.isInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]

Premises used: IsDenseInducing.isInducing, Dense.closure_eq, Set.preimage_univ, Topology.IsInducing.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
trivial
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
⊢ interior s = ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun x hx => ?_

Premises used: Iff.mpr, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
refine : ∀ (x : α) (hx : x ∈ interior s), False
⊢ interior s = ∅

Tactic:
refine eq_empty_iff_forall_notMem.2 fun x hx => ?_

Premises used: Iff.mpr, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : x ∈ interior s
⊢ s ∈ 𝓝 x

Tactic:
rw [mem_interior_iff_mem_nhds] at hx

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i x)

Tactic:
have := di.closure_image_mem_nhds hx
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : closure[inst_1] (i '' s) ∈ 𝓝 (i x)
⊢ i '' s ∈ 𝓝 (i x)

Tactic:
rw [(hs.image di.continuous).isClosed.closure_eq] at this

Premises used: IsClosed.closure_eq, IsDenseInducing.continuous, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
rcases : ∀ (y : β) (hyi : y ∈ (range i)ᶜ) (hys : y ∈ i '' s), False
⊢ False

Tactic:
rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩

Premises used: Dense.inter_nhds_nonempty
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
y : β
hyi : y ∈ (range i)ᶜ
hys : y ∈ i '' s
⊢ False

Tactic:
hyi (image_subset_range _ _ hys)

Premises used: Set.image_subset_range
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
y : β
hyi : y ∈ (range i)ᶜ
hys : y ∈ i '' s
⊢ False

Tactic:
exact hyi (image_subset_range _ _ hys)

Premises used: Set.image_subset_range
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : SeparableSpace α
di : IsDenseInducing i
⊢ SeparableSpace β

Tactic:
di.dense.separableSpace di.continuous

Premises used: DenseRange.separableSpace, IsDenseInducing.dense, IsDenseInducing.continuous
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
⊢ map g (comap g (𝓝 d)) ≤ 𝓝 d

Tactic:
have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d
⊢ map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)

Tactic:
replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))

Tactic:
rw [Filter.map_map, comm, ← Filter.map_map, map_le_iff_le_comap] at lim1

Premises used: Filter.map_map, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
⊢ comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))

Tactic:
have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a)) := comap_mono H
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
⊢ comap i (map h (𝓝 d)) ≤ 𝓝 a

Tactic:
rw [← di.nhds_eq_comap] at lim2

Premises used: IsDenseInducing.nhds_eq_comap
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
le_trans lim1 lim2

Premises used: Filter.Tendsto, le_trans
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
exact le_trans lim1 lim2

Premises used: le_trans
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
⊢ (𝓝[range i] b).NeBot

Tactic:
di.dense.nhdsWithin_neBot b

Premises used: DenseRange.nhdsWithin_neBot, IsDenseInducing.dense
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
rcases : ∀ (a : α) (ha : i a ∈ s), ∃ (a : α), i a ∈ s
⊢ ∃ (a : α), i a ∈ s

Tactic:
rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩

Premises used: mem_closure_iff_nhds, IsDenseInducing.dense, Iff.mp, rfl
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ (a : α), i a ∈ s

Tactic:
⟨a, ha⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ (a : α), i a ∈ s

Tactic:
exact ⟨a, ha⟩
-- Module: Mathlib.Topology.DenseEmbedding
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : Dense s
a : α
⊢ NeBot (α := { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a))

Tactic:
hs.isDenseInducing_val.comap_nhds_neBot _

Premises used: IsDenseInducing.comap_nhds_neBot, Dense.isDenseInducing_val
-- Module: Mathlib.Topology.DenseEmbedding
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
rw : Tendsto f (𝓝 a) (𝓝 ((𝓝 a).limUnder f))
⊢ Tendsto f (𝓝 a) (𝓝 (di.extend f (i a)))

Tactic:
rw [IsDenseInducing.extend, ← di.nhds_eq_comap]

Premises used: IsDenseInducing.nhds_eq_comap, 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 γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 ((𝓝 a).limUnder f))

Tactic:
tendsto_nhds_limUnder ⟨_, hf⟩

Premises used: tendsto_nhds_limUnder, Exists.intro
-- Module: Mathlib.Topology.DenseEmbedding
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) (𝓝 ((𝓝 a).limUnder f))

Tactic:
exact tendsto_nhds_limUnder ⟨_, hf⟩

Premises used: tendsto_nhds_limUnder, Exists.intro
-- 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 : R1Space γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Inseparable (di.extend f (i a)) (f a)

Tactic:
tendsto_nhds_unique_inseparable (di.tendsto_extend hf) hf

Premises used: tendsto_nhds_unique_inseparable, IsDenseInducing.tendsto_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 : T2Space γ
di : IsDenseInducing i
b : β
c : γ
f : α → γ
hf : Tendsto f (comap i (𝓝 b)) (𝓝 c)
⊢ di.extend f b = c

Tactic:
haveI := di.comap_nhds_neBot
  hf.limUnder_eq

Premises used: Filter.Tendsto.limUnder_eq, 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 : T2Space γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ di.extend f (i a) = f a

Tactic:
extend_eq_of_tendsto _ <| di.nhds_eq_comap a ▸ hf

Premises used: IsDenseInducing.nhds_eq_comap, Eq.rec, 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 : T2Space γ
di : IsDenseInducing i
f : α → γ
a : α
c : γ
hf : Tendsto f (𝓝 a) (𝓝 c)
⊢ di.extend f (i a) = f a

Tactic:
di.extend_eq_at (continuousAt_of_tendsto_nhds hf)

Premises used: IsDenseInducing.extend_eq_at, continuousAt_of_tendsto_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 : T2Space γ
di : IsDenseInducing i
f : α → γ
hf : Continuous[inst, inst_2] f
a : α
⊢ di.extend f (i a) = f a

Tactic:
di.extend_eq_at hf.continuousAt

Premises used: Continuous.continuousAt, IsDenseInducing.extend_eq_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 : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
rcases : ∀ (b : γ) (hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)), di.extend f (i a) = f a
⊢ di.extend f (i a) = f a

Tactic:
rcases hf (i a) with ⟨b, hb⟩
-- 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 : α → γ
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

Tactic:
di.extend_eq_at' b ?_

Premises used: IsDenseInducing.extend_eq_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 : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
refine : Tendsto f (𝓝 a) (𝓝 b)
⊢ di.extend f (i a) = f a

Tactic:
refine di.extend_eq_at' b ?_

Premises used: IsDenseInducing.extend_eq_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 : T2Space γ
f : α → γ
di : IsDenseInducing i
hf : ∀ (b : β), ∃ (c : γ), Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb : Tendsto f (𝓝 a) (𝓝 b)), Tendsto f (𝓝 a) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)

Tactic:
rwa [← di.isInducing.nhds_eq_comap] at hb

Premises used: Topology.IsInducing.nhds_eq_comap, IsDenseInducing.isInducing
-- 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 : β
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

Tactic:
di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_

Premises used: Iff.mpr, IsDenseInducing.extend_eq_of_tendsto, Filter.mem_map
-- 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 : β
f : α → γ
g : β → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
refine : ∀ (s : Set γ) (hs : s ∈ 𝓝 (g b)), f ⁻¹' s ∈ comap i (𝓝 b)
⊢ di.extend f b = g b

Tactic:
refine di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_

Premises used: Iff.mpr, IsDenseInducing.extend_eq_of_tendsto, Filter.mem_map
-- 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 : β
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)
suffices : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
⊢ f ⁻¹' s ∈ comap i (𝓝 b)

Tactic:
suffices ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s from
    hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)