case hmul
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto (fun p => p.fst • p.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)

case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ContinuousSMul R M
apply ContinuousSMul.of_nhds_zero
case hmul
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (i : ι), p i → ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.fst • x.snd ∈ b i
case hmul
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto (fun p => p.fst • p.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
rw [h.tendsto_right_iff]
case hmul
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
⊢ ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.fst • x.snd ∈ b i
case hmul
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (i : ι), p i → ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.fst • x.snd ∈ b i
intro i hi
case hmul.intro.intro.intro.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : V ∈ 𝓝 0
j : ι
hj : p j
hVj : V • b j ⊆ b i
⊢ ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.fst • x.snd ∈ b i
case hmul
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
⊢ ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.fst • x.snd ∈ b i
rcases hsmul hi with ⟨V, V_in, j, hj, hVj⟩
case hmul.intro.intro.intro.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : V ∈ 𝓝 0
j : ι
hj : p j
hVj : V • b j ⊆ b i
⊢ V ×ˢ b j ⊆ {x | (fun x => x.fst • x.snd ∈ b i) x}
case hmul.intro.intro.intro.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : V ∈ 𝓝 0
j : ι
hj : p j
hVj : V • b j ⊆ b i
⊢ ∀ᶠ (x : R × M) in 𝓝 0 ×ˢ 𝓝 0, x.fst • x.snd ∈ b i
apply mem_of_superset (prod_mem_prod V_in <| h.mem_of_mem hj)
case hmul.intro.intro.intro.intro.mk.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : V ∈ 𝓝 0
j : ι
hj : p j
hVj : V • b j ⊆ b i
v : R
w : M
v_in : v ∈ V
w_in : w ∈ b j
⊢ (v, w) ∈ {x | (fun x => x.fst • x.snd ∈ b i) x}
case hmul.intro.intro.intro.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : V ∈ 𝓝 0
j : ι
hj : p j
hVj : V • b j ⊆ b i
⊢ V ×ˢ b j ⊆ {x | (fun x => x.fst • x.snd ∈ b i) x}
rintro ⟨v, w⟩ ⟨v_in : v ∈ V, w_in : w ∈ b j⟩
no goals
case hmul.intro.intro.intro.intro.mk.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : V ∈ 𝓝 0
j : ι
hj : p j
hVj : V • b j ⊆ b i
v : R
w : M
v_in : v ∈ V
w_in : w ∈ b j
⊢ (v, w) ∈ {x | (fun x => x.fst • x.snd ∈ b i) x}
exact hVj (Set.smul_mem_smul v_in w_in)
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ Tendsto (fun a => a • m₀) (𝓝 0) (𝓝 0)
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)
intro m₀
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ ∀ (i : ι), p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ Tendsto (fun a => a • m₀) (𝓝 0) (𝓝 0)
rw [h.tendsto_right_iff]
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
i : ι
hi : p i
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ ∀ (i : ι), p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
intro i hi
no goals
case hmulleft
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
i : ι
hi : p i
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
exact hsmul_right m₀ hi
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ Tendsto (fun m => x₀ • m) (𝓝 0) (𝓝 0)
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
intro x₀
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ ∀ (i : ι), p i → ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ Tendsto (fun m => x₀ • m) (𝓝 0) (𝓝 0)
rw [h.tendsto_right_iff]
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ ∀ (i : ι), p i → ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
intro i hi
case hmulright.intro.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
j : ι
hj : p j
hji : b j ⊆ (fun x => x₀ • x) ⁻¹' b i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
case hmulright
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
rcases hsmul_left x₀ hi with ⟨j, hj, hji⟩
no goals
case hmulright.intro.intro
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_1
inst✝² : TopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j x, b j ⊆ (fun x => x₀ • x) ⁻¹' b i
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
j : ι
hj : p j
hji : b j ⊆ (fun x => x₀ • x) ⁻¹' b i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
exact mem_of_superset (h.mem_of_mem hj) hji