Theorem: LinearTopology.tendsto_zero_mul (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
⊢ Filter.Tendsto (a * b) f (nhds 0)
Tactic:
intro v hv
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (a * b) f

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (a * b) f
Tactic:
rw [LinearTopology.mem_nhds_zero_iff] at hv
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : ∃ i ∈ toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ v
⊢ v ∈ Filter.map (a * b) f

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : ∃ i ∈ toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ v
⊢ v ∈ Filter.map (a * b) f
Tactic:
obtain ⟨I, _, I_mem, I_le⟩ := hv
State after:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ≤ v
⊢ v ∈ Filter.map (a * b) f

State before:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ≤ v
⊢ v ∈ Filter.map (a * b) f
Tactic:
simp only [Set.le_eq_subset] at I_le
State after:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ v ∈ Filter.map (a * b) f

State before:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ v ∈ Filter.map (a * b) f
Tactic:
apply Filter.sets_of_superset _ _ I_le
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ ↑I ∈ (Filter.map (a * b) f).sets

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ ↑I ∈ (Filter.map (a * b) f).sets
Tactic:
simp only [Filter.mem_sets, Filter.mem_map]
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f
Tactic:
rw [Filter.tendsto_def] at hb
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : ∀ s ∈ nhds 0, b ⁻¹' s ∈ f
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : ∀ s ∈ nhds 0, b ⁻¹' s ∈ f
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f
Tactic:
specialize hb _ I_mem
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ (a * b) ⁻¹' ↑I ∈ f

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ (a * b) ⁻¹' ↑I ∈ f
Tactic:
apply Filter.sets_of_superset _ hb
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ b ⁻¹' ↑I ⊆ (a * b) ⁻¹' ↑I

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ b ⁻¹' ↑I ⊆ (a * b) ⁻¹' ↑I
Tactic:
intro x
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ x ∈ b ⁻¹' ↑I → x ∈ (a * b) ⁻¹' ↑I

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ x ∈ b ⁻¹' ↑I → x ∈ (a * b) ⁻¹' ↑I
Tactic:
simp only [Set.mem_preimage, Pi.mul_apply, SetLike.mem_coe]
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ b x ∈ I → a x * b x ∈ I

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ b x ∈ I → a x * b x ∈ I
Tactic:
intro hx
State after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
hx : b x ∈ I
⊢ a x * b x ∈ I

State before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
hx : b x ∈ I
⊢ a x * b x ∈ I
Tactic:
apply Ideal.mul_mem_left _ _ hx
State after:
no goals