-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem _root_.ContinuousSMul.of_basis_zero {ι : Type*} [IsTopologicalRing R] [TopologicalSpace M]
    [IsTopologicalAddGroup M] {p : ι → Prop} {b : ι → Set M} (h : HasBasis (𝓝 0) p b)
    (hsmul : ∀ {i}, p i → ∃ V ∈ 𝓝 (0 : R), ∃ j, p j ∧ V • b j ⊆ b i)
    (hsmul_left : ∀ (x₀ : R) {i}, p i → ∃ j, p j ∧ MapsTo (x₀ • ·) (b j) (b i))
    (hsmul_right : ∀ (m₀ : M) {i}, p i → ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ b i) : ContinuousSMul R M

Proof state:
case hmul.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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.1 • x.2 ∈ b i

Tactic:
apply mem_of_superset (prod_mem_prod V_in <| h.mem_of_mem hj)

Result:
case hmul.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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.1 • x.2 ∈ b i) x}

Proof state:
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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

Tactic:
intro i hi

Result:
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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

Proof state:
case hmulright.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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 : MapsTo (fun x => x₀ • x) (b j) (b i)
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i

Tactic:
exact mem_of_superset (h.mem_of_mem hj) hji

Result:
no goals

Proof state:
case hmul.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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.1 • x.2 ∈ b i) x}

Tactic:
rintro ⟨v, w⟩ ⟨v_in : v ∈ V, w_in : w ∈ b j⟩

Result:
case hmul.intro.intro.intro.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (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.1 • x.2 ∈ b i) x}