[GOAL]
G : Type u_1
inst✝ : CommGroup G
sets : Set (Set G)
nonempty : Set.Nonempty sets
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z, z ∈ sets ∧ z ⊆ x ∩ y
one : ∀ (U : Set G), U ∈ sets → 1 ∈ U
mul : ∀ (U : Set G), U ∈ sets → ∃ V, V ∈ sets ∧ V * V ⊆ U
inv : ∀ (U : Set G), U ∈ sets → ∃ V, V ∈ sets ∧ V ⊆ (fun x => x⁻¹) ⁻¹' U
x : G
U : Set G
U_in :
  U ∈
    { sets := sets, nonempty := nonempty,
        inter_sets := (_ : ∀ {x y : Set G}, x ∈ sets → y ∈ sets → ∃ z, z ∈ sets ∧ z ⊆ x ∩ y) }.sets
⊢ U ⊆ (fun x_1 => x * x_1 * x⁻¹) ⁻¹' U
[PROOFSTEP]
simp only [mul_inv_cancel_comm, preimage_id']
[GOAL]
G : Type u_1
inst✝ : CommGroup G
sets : Set (Set G)
nonempty : Set.Nonempty sets
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z, z ∈ sets ∧ z ⊆ x ∩ y
one : ∀ (U : Set G), U ∈ sets → 1 ∈ U
mul : ∀ (U : Set G), U ∈ sets → ∃ V, V ∈ sets ∧ V * V ⊆ U
inv : ∀ (U : Set G), U ∈ sets → ∃ V, V ∈ sets ∧ V ⊆ (fun x => x⁻¹) ⁻¹' U
x : G
U : Set G
U_in :
  U ∈
    { sets := sets, nonempty := nonempty,
        inter_sets := (_ : ∀ {x y : Set G}, x ∈ sets → y ∈ sets → ∃ z, z ∈ sets ∧ z ⊆ x ∩ y) }.sets
⊢ U ⊆ U
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ GroupFilterBasis G
[PROOFSTEP]
refine'
  { sets := {{1}}
    nonempty := singleton_nonempty _ .. }
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y
case refine'_2
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets → 1 ∈ U
case refine'_3
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    U ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets →
      ∃ V, V ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets ∧ V * V ⊆ U
case refine'_4
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    U ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets →
      ∃ V,
        V ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets ∧
          V ⊆ (fun x => x⁻¹) ⁻¹' U
case refine'_5
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G},
    U ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets →
      ∃ V,
        V ∈ { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}), inter_sets := ?refine'_1 }.sets ∧
          V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
[PROOFSTEP]
all_goals simp only [exists_prop, mem_singleton_iff]
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y
[PROOFSTEP]
simp only [exists_prop, mem_singleton_iff]
[GOAL]
case refine'_2
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    U ∈
        { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
            inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets →
      1 ∈ U
[PROOFSTEP]
simp only [exists_prop, mem_singleton_iff]
[GOAL]
case refine'_3
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    U ∈
        { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
            inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
                inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets ∧
          V * V ⊆ U
[PROOFSTEP]
simp only [exists_prop, mem_singleton_iff]
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    U ∈
        { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
            inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
                inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => x⁻¹) ⁻¹' U
[PROOFSTEP]
simp only [exists_prop, mem_singleton_iff]
[GOAL]
case refine'_5
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G},
    U ∈
        { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
            inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {{1}}, nonempty := (_ : Set.Nonempty {{1}}),
                inter_sets := (_ : ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z, z ∈ {{1}} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
[PROOFSTEP]
simp only [exists_prop, mem_singleton_iff]
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G}, x = {1} → y = {1} → ∃ z, z = {1} ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro - - rfl rfl
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∃ z, z = {1} ∧ z ⊆ {1} ∩ {1}
[PROOFSTEP]
use{1}
[GOAL]
case h
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ {1} = {1} ∧ {1} ⊆ {1} ∩ {1}
[PROOFSTEP]
simp
[GOAL]
case refine'_2
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U = {1} → 1 ∈ U
[PROOFSTEP]
simp
[GOAL]
case refine'_3
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U = {1} → ∃ V, V = {1} ∧ V * V ⊆ U
[PROOFSTEP]
rintro - rfl
[GOAL]
case refine'_3
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∃ V, V = {1} ∧ V * V ⊆ {1}
[PROOFSTEP]
use{1}
[GOAL]
case h
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ {1} = {1} ∧ {1} * {1} ⊆ {1}
[PROOFSTEP]
simp
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U = {1} → ∃ V, V = {1} ∧ V ⊆ (fun x => x⁻¹) ⁻¹' U
[PROOFSTEP]
rintro - rfl
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∃ V, V = {1} ∧ V ⊆ (fun x => x⁻¹) ⁻¹' {1}
[PROOFSTEP]
use{1}
[GOAL]
case h
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ {1} = {1} ∧ {1} ⊆ (fun x => x⁻¹) ⁻¹' {1}
[PROOFSTEP]
simp
[GOAL]
case refine'_5
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G}, U = {1} → ∃ V, V = {1} ∧ V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
[PROOFSTEP]
rintro x₀ - rfl
[GOAL]
case refine'_5
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∃ V, V = {1} ∧ V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' {1}
[PROOFSTEP]
use{1}
[GOAL]
case h
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ {1} = {1} ∧ {1} ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' {1}
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ N B 1 = FilterBasis.filter toFilterBasis
[PROOFSTEP]
simp only [N, one_mul, map_id']
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ 𝓝 x₀ = N B x₀
[PROOFSTEP]
rw [TopologicalSpace.nhds_mkOfNhds]
[GOAL]
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ pure ≤ N B
[PROOFSTEP]
intro x U U_in
[GOAL]
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : U ∈ N B x
⊢ U ∈ pure x
[PROOFSTEP]
rw [(B.hasBasis x).mem_iff] at U_in 
[GOAL]
case h₀
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : ∃ i, i ∈ B ∧ (fun y => x * y) '' i ⊆ U
⊢ U ∈ pure x
[PROOFSTEP]
rcases U_in with ⟨V, V_in, H⟩
[GOAL]
case h₀.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
⊢ U ∈ pure x
[PROOFSTEP]
simpa [mem_pure] using H (mem_image_of_mem _ (GroupFilterBasis.one V_in))
[GOAL]
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G) (s : Set G), s ∈ N B a → ∃ t, t ∈ N B a ∧ t ⊆ s ∧ ∀ (a' : G), a' ∈ t → s ∈ N B a'
[PROOFSTEP]
intro x U U_in
[GOAL]
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : U ∈ N B x
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
[PROOFSTEP]
rw [(B.hasBasis x).mem_iff] at U_in 
[GOAL]
case h₁
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U : Set G
U_in : ∃ i, i ∈ B ∧ (fun y => x * y) '' i ⊆ U
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
[PROOFSTEP]
rcases U_in with ⟨V, V_in, H⟩
[GOAL]
case h₁.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
[PROOFSTEP]
rcases GroupFilterBasis.mul V_in with ⟨W, W_in, hW⟩
[GOAL]
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ ∃ t, t ∈ N B x ∧ t ⊆ U ∧ ∀ (a' : G), a' ∈ t → U ∈ N B a'
[PROOFSTEP]
use(fun y ↦ x * y) '' W, image_mem_map (FilterBasis.mem_filter_of_mem _ W_in)
[GOAL]
case right
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ (fun y => x * y) '' W ⊆ U ∧ ∀ (a' : G), a' ∈ (fun y => x * y) '' W → U ∈ N B a'
[PROOFSTEP]
constructor
[GOAL]
case right.left
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ (fun y => x * y) '' W ⊆ U
[PROOFSTEP]
rw [image_subset_iff] at H ⊢
[GOAL]
case right.left
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : V ⊆ (fun y => x * y) ⁻¹' U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ W ⊆ (fun y => x * y) ⁻¹' U
[PROOFSTEP]
exact ((B.prod_subset_self W_in).trans hW).trans H
[GOAL]
case right.right
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
⊢ ∀ (a' : G), a' ∈ (fun y => x * y) '' W → U ∈ N B a'
[PROOFSTEP]
rintro y ⟨t, tW, rfl⟩
[GOAL]
case right.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ U ∈ N B ((fun y => x * y) t)
[PROOFSTEP]
rw [(B.hasBasis _).mem_iff]
[GOAL]
case right.right.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ ∃ i, i ∈ B ∧ (fun y => (fun y => x * y) t * y) '' i ⊆ U
[PROOFSTEP]
use W, W_in
[GOAL]
case right
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ U
[PROOFSTEP]
apply Subset.trans _ H
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
H : (fun y => x * y) '' V ⊆ U
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ (fun y => x * y) '' V
[PROOFSTEP]
clear H
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
⊢ (fun y => (fun y => x * y) t * y) '' W ⊆ (fun y => x * y) '' V
[PROOFSTEP]
rintro z ⟨w, wW, rfl⟩
[GOAL]
case intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
w : G
wW : w ∈ W
⊢ (fun y => (fun y => x * y) t * y) w ∈ (fun y => x * y) '' V
[PROOFSTEP]
exact ⟨t * w, hW (mul_mem_mul tW wW), by simp [mul_assoc]⟩
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ x : G
U V : Set G
V_in : V ∈ B
W : Set G
W_in : W ∈ B
hW : W * W ⊆ V
t : G
tW : t ∈ W
w : G
wW : w ∈ W
⊢ (fun y => x * y) (t * w) = (fun y => (fun y => x * y) t * y) w
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ 𝓝 1 = FilterBasis.filter toFilterBasis
[PROOFSTEP]
rw [B.nhds_eq]
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ N B 1 = FilterBasis.filter toFilterBasis
[PROOFSTEP]
simp only [N, one_mul]
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ map (fun y => y) (FilterBasis.filter toFilterBasis) = FilterBasis.filter toFilterBasis
[PROOFSTEP]
exact map_id
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ HasBasis (𝓝 x₀) (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
[PROOFSTEP]
rw [B.nhds_eq]
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
x₀ : G
⊢ HasBasis (N B x₀) (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
[PROOFSTEP]
apply B.hasBasis
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ HasBasis (𝓝 1) (fun V => V ∈ B) id
[PROOFSTEP]
rw [B.nhds_one_eq]
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ HasBasis (FilterBasis.filter toFilterBasis) (fun V => V ∈ B) id
[PROOFSTEP]
exact B.toFilterBasis.hasBasis
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ U ∈ 𝓝 1
[PROOFSTEP]
rw [B.nhds_one_hasBasis.mem_iff]
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i, i ∈ B ∧ id i ⊆ U
[PROOFSTEP]
exact ⟨U, hU, rfl.subset⟩
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ TopologicalGroup G
[PROOFSTEP]
letI := B.topology
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
⊢ TopologicalGroup G
[PROOFSTEP]
have basis := B.nhds_one_hasBasis
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
⊢ TopologicalGroup G
[PROOFSTEP]
have basis' := basis.prod basis
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ TopologicalGroup G
[PROOFSTEP]
refine' TopologicalGroup.of_nhds_one _ _ _ _
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
[PROOFSTEP]
rw [basis'.tendsto_iff basis]
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ ∀ (ib : Set G),
    ib ∈ B →
      ∃ ia,
        (ia.fst ∈ B ∧ ia.snd ∈ B) ∧ ∀ (x : G × G), x ∈ id ia.fst ×ˢ id ia.snd → uncurry (fun x x_1 => x * x_1) x ∈ id ib
[PROOFSTEP]
suffices ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
[GOAL]
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this✝ : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
this : ∀ (U : Set G), U ∈ B → ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ (ib : Set G),
    ib ∈ B →
      ∃ ia,
        (ia.fst ∈ B ∧ ia.snd ∈ B) ∧ ∀ (x : G × G), x ∈ id ia.fst ×ˢ id ia.snd → uncurry (fun x x_1 => x * x_1) x ∈ id ib
[PROOFSTEP]
simpa
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ ∀ (U : Set G), U ∈ B → ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
[PROOFSTEP]
intro U U_in
[GOAL]
case refine'_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
U : Set G
U_in : U ∈ B
⊢ ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
[PROOFSTEP]
rcases mul U_in with ⟨V, V_in, hV⟩
[GOAL]
case refine'_1.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
[PROOFSTEP]
refine' ⟨V, V, ⟨V_in, V_in⟩, _⟩
[GOAL]
case refine'_1.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∀ (a b : G), a ∈ V → b ∈ V → a * b ∈ U
[PROOFSTEP]
intro a b a_in b_in
[GOAL]
case refine'_1.intro.intro
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
a b : G
a_in : a ∈ V
b_in : b ∈ V
⊢ a * b ∈ U
[PROOFSTEP]
exact hV ⟨a, b, a_in, b_in, rfl⟩
[GOAL]
case refine'_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
[PROOFSTEP]
rw [basis.tendsto_iff basis]
[GOAL]
case refine'_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ ∀ (ib : Set G), ib ∈ B → ∃ ia, ia ∈ B ∧ ∀ (x : G), x ∈ id ia → x⁻¹ ∈ id ib
[PROOFSTEP]
intro U U_in
[GOAL]
case refine'_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
U : Set G
U_in : U ∈ B
⊢ ∃ ia, ia ∈ B ∧ ∀ (x : G), x ∈ id ia → x⁻¹ ∈ id U
[PROOFSTEP]
simpa using inv U_in
[GOAL]
case refine'_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
[PROOFSTEP]
intro x₀
[GOAL]
case refine'_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
x₀ : G
⊢ 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
[PROOFSTEP]
rw [nhds_eq, nhds_one_eq]
[GOAL]
case refine'_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
x₀ : G
⊢ N B x₀ = map (fun x => x₀ * x) (FilterBasis.filter toFilterBasis)
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
⊢ ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
[PROOFSTEP]
intro x₀
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
x₀ : G
⊢ Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
[PROOFSTEP]
rw [basis.tendsto_iff basis]
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
x₀ : G
⊢ ∀ (ib : Set G), ib ∈ B → ∃ ia, ia ∈ B ∧ ∀ (x : G), x ∈ id ia → x₀ * x * x₀⁻¹ ∈ id ib
[PROOFSTEP]
intro U U_in
[GOAL]
case refine'_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := topology B
basis : HasBasis (𝓝 1) (fun V => V ∈ B) id
basis' : HasBasis (𝓝 1 ×ˢ 𝓝 1) (fun i => i.fst ∈ B ∧ i.snd ∈ B) fun i => id i.fst ×ˢ id i.snd
x₀ : G
U : Set G
U_in : U ∈ B
⊢ ∃ ia, ia ∈ B ∧ ∀ (x : G), x ∈ id ia → x₀ * x * x₀⁻¹ ∈ id U
[PROOFSTEP]
exact conj x₀ U_in
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
⊢ TopologicalRing R
[PROOFSTEP]
let B' := B.toAddGroupFilterBasis
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
⊢ TopologicalRing R
[PROOFSTEP]
letI := B'.topology
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this : TopologicalSpace R := AddGroupFilterBasis.topology B'
⊢ TopologicalRing R
[PROOFSTEP]
have basis := B'.nhds_zero_hasBasis
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
⊢ TopologicalRing R
[PROOFSTEP]
have basis' := basis.prod basis
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
⊢ TopologicalRing R
[PROOFSTEP]
haveI := B'.isTopologicalAddGroup
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
⊢ TopologicalRing R
[PROOFSTEP]
apply TopologicalRing.of_addGroup_of_nhds_zero
[GOAL]
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
⊢ Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
[PROOFSTEP]
rw [basis'.tendsto_iff basis]
[GOAL]
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
⊢ ∀ (ib : Set R),
    ib ∈ B' →
      ∃ ia,
        (ia.fst ∈ B' ∧ ia.snd ∈ B') ∧
          ∀ (x : R × R), x ∈ id ia.fst ×ˢ id ia.snd → uncurry (fun x x_1 => x * x_1) x ∈ id ib
[PROOFSTEP]
suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
[GOAL]
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝¹ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this✝ : TopologicalAddGroup R
this : ∀ (U : Set R), U ∈ B' → ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ (ib : Set R),
    ib ∈ B' →
      ∃ ia,
        (ia.fst ∈ B' ∧ ia.snd ∈ B') ∧
          ∀ (x : R × R), x ∈ id ia.fst ×ˢ id ia.snd → uncurry (fun x x_1 => x * x_1) x ∈ id ib
[PROOFSTEP]
simpa
[GOAL]
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
⊢ ∀ (U : Set R), U ∈ B' → ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
[PROOFSTEP]
intro U U_in
[GOAL]
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
U : Set R
U_in : U ∈ B'
⊢ ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
[PROOFSTEP]
rcases B.mul U_in with ⟨V, V_in, hV⟩
[GOAL]
case hmul.intro.intro
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
U : Set R
U_in : U ∈ B'
V : Set R
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
[PROOFSTEP]
refine' ⟨V, V, ⟨V_in, V_in⟩, _⟩
[GOAL]
case hmul.intro.intro
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
U : Set R
U_in : U ∈ B'
V : Set R
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∀ (a b : R), a ∈ V → b ∈ V → a * b ∈ U
[PROOFSTEP]
intro a b a_in b_in
[GOAL]
case hmul.intro.intro
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
U : Set R
U_in : U ∈ B'
V : Set R
V_in : V ∈ B
hV : V * V ⊆ U
a b : R
a_in : a ∈ V
b_in : b ∈ V
⊢ a * b ∈ U
[PROOFSTEP]
exact hV ⟨a, b, a_in, b_in, rfl⟩
[GOAL]
case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
intro x₀
[GOAL]
case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
x₀ : R
⊢ Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
rw [basis.tendsto_iff basis]
[GOAL]
case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
x₀ : R
⊢ ∀ (ib : Set R), ib ∈ B' → ∃ ia, ia ∈ B' ∧ ∀ (x : R), x ∈ id ia → x₀ * x ∈ id ib
[PROOFSTEP]
intro U
[GOAL]
case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
x₀ : R
U : Set R
⊢ U ∈ B' → ∃ ia, ia ∈ B' ∧ ∀ (x : R), x ∈ id ia → x₀ * x ∈ id U
[PROOFSTEP]
simpa using B.mul_left x₀
[GOAL]
case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
intro x₀
[GOAL]
case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
x₀ : R
⊢ Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
rw [basis.tendsto_iff basis]
[GOAL]
case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
x₀ : R
⊢ ∀ (ib : Set R), ib ∈ B' → ∃ ia, ia ∈ B' ∧ ∀ (x : R), x ∈ id ia → x * x₀ ∈ id ib
[PROOFSTEP]
intro U
[GOAL]
case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this✝ : TopologicalSpace R := AddGroupFilterBasis.topology B'
basis : HasBasis (𝓝 0) (fun V => V ∈ B') id
basis' : HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => i.fst ∈ B' ∧ i.snd ∈ B') fun i => id i.fst ×ˢ id i.snd
this : TopologicalAddGroup R
x₀ : R
U : Set R
⊢ U ∈ B' → ∃ ia, ia ∈ B' ∧ ∀ (x : R), x ∈ id ia → x * x₀ ∈ id U
[PROOFSTEP]
simpa using B.mul_right x₀
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
⊢ ∀ {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
[PROOFSTEP]
rintro U (rfl : U ∈ {{(0 : M)}})
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ {0}
[PROOFSTEP]
use univ, univ_mem, {0}, rfl
[GOAL]
case right
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
⊢ univ • {0} ⊆ {0}
[PROOFSTEP]
rintro a ⟨x, m, -, rfl, rfl⟩
[GOAL]
case right.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
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
x : R
⊢ (fun x x_1 => x • x_1) x 0 ∈ {0}
[PROOFSTEP]
simp only [smul_zero, mem_singleton_iff]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
⊢ ∀ (x₀ : R) {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
[PROOFSTEP]
rintro x₀ U (h : U ∈ {{(0 : M)}})
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
x₀ : R
U : Set M
h : U ∈ {{0}}
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
[PROOFSTEP]
rw [mem_singleton_iff] at h 
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
x₀ : R
U : Set M
h : U = {0}
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
[PROOFSTEP]
use{0}, rfl
[GOAL]
case right
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
x₀ : R
U : Set M
h : U = {0}
⊢ {0} ⊆ (fun x => x₀ • x) ⁻¹' U
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
⊢ ∀ (m₀ : M) {U : Set M}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
rintro m₀ U (h : U ∈ (0 : Set (Set M)))
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
m₀ : M
U : Set M
h : U ∈ 0
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
rw [Set.mem_zero] at h 
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
src✝ : AddGroupFilterBasis M :=
  let_fun this := default;
  this
m₀ : M
U : Set M
h : U = 0
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
simp [h, nhds_discrete]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
apply ContinuousSMul.of_nhds_zero
[GOAL]
case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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)
[PROOFSTEP]
rw [h.tendsto_right_iff]
[GOAL]
case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
intro i hi
[GOAL]
case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
rcases hsmul hi with ⟨V, V_in, j, hj, hVj⟩
[GOAL]
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
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
apply mem_of_superset (prod_mem_prod V_in <| h.mem_of_mem hj)
[GOAL]
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
B : ModuleFilterBasis R M
ι : Type u_3
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}
[PROOFSTEP]
rintro ⟨v, w⟩ ⟨v_in : v ∈ V, w_in : w ∈ b j⟩
[GOAL]
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
B : ModuleFilterBasis R M
ι : Type u_3
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}
[PROOFSTEP]
exact hVj (Set.smul_mem_smul v_in w_in)
[GOAL]
case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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)
[PROOFSTEP]
intro m₀
[GOAL]
case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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)
[PROOFSTEP]
rw [h.tendsto_right_iff]
[GOAL]
case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
intro i hi
[GOAL]
case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
exact hsmul_right m₀ hi
[GOAL]
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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)
[PROOFSTEP]
intro x₀
[GOAL]
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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)
[PROOFSTEP]
rw [h.tendsto_right_iff]
[GOAL]
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
intro i hi
[GOAL]
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
rcases hsmul_left x₀ hi with ⟨j, hj, hji⟩
[GOAL]
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
B : ModuleFilterBasis R M
ι : Type u_3
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
[PROOFSTEP]
exact mem_of_superset (h.mem_of_mem hj) hji
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : TopologicalRing R
⊢ ContinuousSMul R M
[PROOFSTEP]
let B' := B.toAddGroupFilterBasis
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : TopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
⊢ ContinuousSMul R M
[PROOFSTEP]
let _ := B'.topology
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : TopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝ : TopologicalSpace M := AddGroupFilterBasis.topology B'
⊢ ContinuousSMul R M
[PROOFSTEP]
have _ := B'.isTopologicalAddGroup
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : TopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝¹ : TopologicalSpace M := AddGroupFilterBasis.topology B'
x✝ : TopologicalAddGroup M
⊢ ContinuousSMul R M
[PROOFSTEP]
exact
  ContinuousSMul.of_basis_zero B'.nhds_zero_hasBasis (fun {_} => by simpa using B.smul) (by simpa using B.smul_left)
    B.smul_right
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : TopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝² : TopologicalSpace M := AddGroupFilterBasis.topology B'
x✝¹ : TopologicalAddGroup M
x✝ : Set M
⊢ x✝ ∈ B' → ∃ V, V ∈ 𝓝 0 ∧ ∃ j x, V • id j ⊆ id x✝
[PROOFSTEP]
simpa using B.smul
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : TopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝¹ : TopologicalSpace M := AddGroupFilterBasis.topology B'
x✝ : TopologicalAddGroup M
⊢ ∀ (x₀ : R) {i : Set M}, i ∈ B' → ∃ j x, id j ⊆ (fun x => x₀ • x) ⁻¹' id i
[PROOFSTEP]
simpa using B.smul_left
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : TopologicalSpace R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
B : ModuleFilterBasis R✝ M✝
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := RingFilterBasis.topology BR
⊢ ∀ {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
[PROOFSTEP]
intro U U_in
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : TopologicalSpace R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
B : ModuleFilterBasis R✝ M✝
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := RingFilterBasis.topology BR
U : Set M
U_in : U ∈ AddGroupFilterBasis.toFilterBasis.sets
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
[PROOFSTEP]
rcases smul U_in with ⟨V, V_in, W, W_in, H⟩
[GOAL]
case 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✝
B : ModuleFilterBasis R✝ M✝
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := RingFilterBasis.topology BR
U : Set M
U_in : U ∈ AddGroupFilterBasis.toFilterBasis.sets
V : Set R
V_in : V ∈ BR
W : Set M
W_in : W ∈ BM
H : V • W ⊆ U
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
[PROOFSTEP]
exact ⟨V, BR.toAddGroupFilterBasis.mem_nhds_zero V_in, W, W_in, H⟩
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : TopologicalSpace R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
B : ModuleFilterBasis R✝ M✝
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := RingFilterBasis.topology BR
⊢ ∀ (m₀ : M) {U : Set M}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
intro m₀ U U_in
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : TopologicalSpace R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
B : ModuleFilterBasis R✝ M✝
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := RingFilterBasis.topology BR
m₀ : M
U : Set M
U_in : U ∈ AddGroupFilterBasis.toFilterBasis.sets
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
rcases smul_right m₀ U_in with ⟨V, V_in, H⟩
[GOAL]
case intro.intro
R✝ : Type u_1
M✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : TopologicalSpace R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
B : ModuleFilterBasis R✝ M✝
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ ∃ W, W ∈ BM ∧ V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V, V ∈ BM ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V, V ∈ BR ∧ V ⊆ (fun x => x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := RingFilterBasis.topology BR
m₀ : M
U : Set M
U_in : U ∈ AddGroupFilterBasis.toFilterBasis.sets
V : Set R
V_in : V ∈ BR
H : V ⊆ (fun x => x • m₀) ⁻¹' U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H
