[GOAL]
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
[PROOFSTEP]
have := h.comap fun p : G × G => p.2 / p.1
[GOAL]
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (comap (fun p => p.snd / p.fst) (𝓝 1)) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
[PROOFSTEP]
rw [← uniformity_eq_comap_nhds_one] at this
[GOAL]
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
[PROOFSTEP]
convert UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) this
[GOAL]
case h.e'_5.h.h.e'_2.h.a
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G ((fun p => p.snd / p.fst) ⁻¹' b x✝¹)
[PROOFSTEP]
simp [UniformFun.gen]
[GOAL]
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖✝ : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
⊢ HasBasis (𝓝 1) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd}
[PROOFSTEP]
have := h.comap fun p : G × G => p.1 / p.2
[GOAL]
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖✝ : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (comap (fun p => p.fst / p.snd) (𝓝 1)) p fun i => (fun p => p.fst / p.snd) ⁻¹' b i
⊢ HasBasis (𝓝 1) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd}
[PROOFSTEP]
rw [← uniformity_eq_comap_nhds_one_swapped] at this
[GOAL]
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖✝ : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.fst / p.snd) ⁻¹' b i
⊢ HasBasis (𝓝 1) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd}
[PROOFSTEP]
convert UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ this
[GOAL]
case h.e'_5.h.h.e'_2.h.a
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
𝔖✝ : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.fst / p.snd) ⁻¹' b i
x✝¹ : Set α × ι
x✝ : α →ᵤ[𝔖] G
⊢ (∀ (x : α), x ∈ x✝¹.fst → x✝ x ∈ b x✝¹.snd) ↔
    (x✝, 1) ∈ UniformOnFun.gen 𝔖 x✝¹.fst ((fun p => p.fst / p.snd) ⁻¹' b x✝¹.snd)
[PROOFSTEP]
simp [UniformOnFun.gen]
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
⊢ ContinuousSMul 𝕜 H
[PROOFSTEP]
have : TopologicalAddGroup H := by
  rw [hφ.induced]
  exact topologicalAddGroup_induced φ
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
⊢ TopologicalAddGroup H
[PROOFSTEP]
rw [hφ.induced]
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
⊢ TopologicalAddGroup H
[PROOFSTEP]
exact topologicalAddGroup_induced φ
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ContinuousSMul 𝕜 H
[PROOFSTEP]
have : (𝓝 0 : Filter H).HasBasis _ _ := by
  rw [hφ.induced, nhds_induced, map_zero]
  exact (UniformOnFun.hasBasis_nhds_zero 𝔖 h𝔖₁ h𝔖₂).comap φ
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ HasBasis (𝓝 0) ?m.88528 ?m.88529
[PROOFSTEP]
rw [hφ.induced, nhds_induced, map_zero]
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ HasBasis (comap (↑φ) (𝓝 0)) ?m.88528 ?m.88529
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ Sort ?u.88519
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ?m.88527 → Prop
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ?m.88527 → Set H
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ Sort ?u.88519
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ?m.88527 → Prop
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ?m.88527 → Set H
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ Sort ?u.88519
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ?m.88527 → Prop
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this : TopologicalAddGroup H
⊢ ?m.88527 → Set H
[PROOFSTEP]
exact (UniformOnFun.hasBasis_nhds_zero 𝔖 h𝔖₁ h𝔖₂).comap φ
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
⊢ ContinuousSMul 𝕜 H
[PROOFSTEP]
refine' ContinuousSMul.of_basis_zero this _ _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
⊢ ∀ {i : Set α × Set E},
    i.fst ∈ 𝔖 ∧ i.snd ∈ 𝓝 0 →
      ∃ V,
        V ∈ 𝓝 0 ∧
          ∃ j x, V • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
[PROOFSTEP]
rintro ⟨S, V⟩ ⟨hS, hV⟩
[GOAL]
case refine'_1.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
⊢ ∃ V_1,
    V_1 ∈ 𝓝 0 ∧
      ∃ j x,
        V_1 • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
have : Tendsto (fun kx : 𝕜 × E => kx.1 • kx.2) (𝓝 (0, 0)) (𝓝 <| (0 : 𝕜) • (0 : E)) :=
  continuous_smul.tendsto (0 : 𝕜 × E)
[GOAL]
case refine'_1.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 (0, 0)) (𝓝 (0 • 0))
⊢ ∃ V_1,
    V_1 ∈ 𝓝 0 ∧
      ∃ j x,
        V_1 • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
rw [zero_smul, nhds_prod_eq] at this
[GOAL]
case refine'_1.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
⊢ ∃ V_1,
    V_1 ∈ 𝓝 0 ∧
      ∃ j x,
        V_1 • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
have := this hV
[GOAL]
case refine'_1.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝² : TopologicalAddGroup H
this✝¹ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this✝ : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
this : (S, V).snd ∈ map (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0)
⊢ ∃ V_1,
    V_1 ∈ 𝓝 0 ∧
      ∃ j x,
        V_1 • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
rw [mem_map, mem_prod_iff] at this
[GOAL]
case refine'_1.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝² : TopologicalAddGroup H
this✝¹ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this✝ : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
this : ∃ t₁, t₁ ∈ 𝓝 0 ∧ ∃ t₂, t₂ ∈ 𝓝 0 ∧ t₁ ×ˢ t₂ ⊆ (fun kx => kx.fst • kx.snd) ⁻¹' (S, V).snd
⊢ ∃ V_1,
    V_1 ∈ 𝓝 0 ∧
      ∃ j x,
        V_1 • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
rcases this with ⟨U, hU, W, hW, hUW⟩
[GOAL]
case refine'_1.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
U : Set 𝕜
hU : U ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hUW : U ×ˢ W ⊆ (fun kx => kx.fst • kx.snd) ⁻¹' (S, V).snd
⊢ ∃ V_1,
    V_1 ∈ 𝓝 0 ∧
      ∃ j x,
        V_1 • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
refine' ⟨U, hU, ⟨S, W⟩, ⟨hS, hW⟩, _⟩
[GOAL]
case refine'_1.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
U : Set 𝕜
hU : U ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hUW : U ×ˢ W ⊆ (fun kx => kx.fst • kx.snd) ⁻¹' (S, V).snd
⊢ U • ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, W).fst → f x ∈ (S, W).snd} ⊆
    ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
rw [Set.smul_subset_iff]
[GOAL]
case refine'_1.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
U : Set 𝕜
hU : U ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hUW : U ×ˢ W ⊆ (fun kx => kx.fst • kx.snd) ⁻¹' (S, V).snd
⊢ ∀ (a : 𝕜),
    a ∈ U →
      ∀ (b : H),
        b ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, W).fst → f x ∈ (S, W).snd} →
          a • b ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
intro a ha u hu x hx
[GOAL]
case refine'_1.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
U : Set 𝕜
hU : U ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hUW : U ×ˢ W ⊆ (fun kx => kx.fst • kx.snd) ⁻¹' (S, V).snd
a : 𝕜
ha : a ∈ U
u : H
hu : u ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, W).fst → f x ∈ (S, W).snd}
x : α
hx : x ∈ (S, V).fst
⊢ ↑φ (a • u) x ∈ (S, V).snd
[PROOFSTEP]
rw [SMulHomClass.map_smul]
[GOAL]
case refine'_1.mk.intro.intro.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun kx => kx.fst • kx.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
U : Set 𝕜
hU : U ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hUW : U ×ˢ W ⊆ (fun kx => kx.fst • kx.snd) ⁻¹' (S, V).snd
a : 𝕜
ha : a ∈ U
u : H
hu : u ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, W).fst → f x ∈ (S, W).snd}
x : α
hx : x ∈ (S, V).fst
⊢ (a • ↑φ u) x ∈ (S, V).snd
[PROOFSTEP]
exact hUW (⟨ha, hu x hx⟩ : (a, φ u x) ∈ U ×ˢ W)
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
⊢ ∀ (x₀ : 𝕜) {i : Set α × Set E},
    i.fst ∈ 𝔖 ∧ i.snd ∈ 𝓝 0 →
      ∃ j x,
        ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
          (fun x => x₀ • x) ⁻¹' (↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd})
[PROOFSTEP]
rintro a ⟨S, V⟩ ⟨hS, hV⟩
[GOAL]
case refine'_2.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
a : 𝕜
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
⊢ ∃ j x,
    ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
      (fun x => a • x) ⁻¹' (↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd})
[PROOFSTEP]
have : Tendsto (fun x : E => a • x) (𝓝 0) (𝓝 <| a • (0 : E)) := tendsto_id.const_smul a
[GOAL]
case refine'_2.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
a : 𝕜
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun x => a • x) (𝓝 0) (𝓝 (a • 0))
⊢ ∃ j x,
    ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
      (fun x => a • x) ⁻¹' (↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd})
[PROOFSTEP]
rw [smul_zero] at this
[GOAL]
case refine'_2.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
a : 𝕜
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun x => a • x) (𝓝 0) (𝓝 0)
⊢ ∃ j x,
    ↑φ ⁻¹' {f | ∀ (x : α), x ∈ j.fst → f x ∈ j.snd} ⊆
      (fun x => a • x) ⁻¹' (↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd})
[PROOFSTEP]
refine' ⟨⟨S, (a • ·) ⁻¹' V⟩, ⟨hS, this hV⟩, fun f hf x hx => _⟩
[GOAL]
case refine'_2.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
a : 𝕜
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun x => a • x) (𝓝 0) (𝓝 0)
f : H
hf : f ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, (fun x => a • x) ⁻¹' V).fst → f x ∈ (S, (fun x => a • x) ⁻¹' V).snd}
x : α
hx : x ∈ (S, V).fst
⊢ ↑φ ((fun x => a • x) f) x ∈ (S, V).snd
[PROOFSTEP]
rw [SMulHomClass.map_smul]
[GOAL]
case refine'_2.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
a : 𝕜
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
this : Tendsto (fun x => a • x) (𝓝 0) (𝓝 0)
f : H
hf : f ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, (fun x => a • x) ⁻¹' V).fst → f x ∈ (S, (fun x => a • x) ⁻¹' V).snd}
x : α
hx : x ∈ (S, V).fst
⊢ (a • ↑φ f) x ∈ (S, V).snd
[PROOFSTEP]
exact hf x hx
[GOAL]
case refine'_3
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
⊢ ∀ (m₀ : H) {i : Set α × Set E},
    i.fst ∈ 𝔖 ∧ i.snd ∈ 𝓝 0 → ∀ᶠ (x : 𝕜) in 𝓝 0, x • m₀ ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
[PROOFSTEP]
rintro u ⟨S, V⟩ ⟨hS, hV⟩
[GOAL]
case refine'_3.mk.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • u ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
rcases h u S hS hV with ⟨r, hrpos, hr⟩
[GOAL]
case refine'_3.mk.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • u ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
rw [Metric.eventually_nhds_iff_ball]
[GOAL]
case refine'_3.mk.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
⊢ ∃ ε, ε > 0 ∧ ∀ (y : 𝕜), y ∈ Metric.ball 0 ε → y • u ∈ ↑φ ⁻¹' {f | ∀ (x : α), x ∈ (S, V).fst → f x ∈ (S, V).snd}
[PROOFSTEP]
refine' ⟨r⁻¹, inv_pos.mpr hrpos, fun a ha x hx => _⟩
[GOAL]
case refine'_3.mk.intro.intro.intro
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : a ∈ Metric.ball 0 r⁻¹
x : α
hx : x ∈ (S, V).fst
⊢ ↑φ (a • u) x ∈ (S, V).snd
[PROOFSTEP]
by_cases ha0 : a = 0
[GOAL]
case pos
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : a ∈ Metric.ball 0 r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : a = 0
⊢ ↑φ (a • u) x ∈ (S, V).snd
[PROOFSTEP]
rw [ha0]
[GOAL]
case pos
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : a ∈ Metric.ball 0 r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : a = 0
⊢ ↑φ (0 • u) x ∈ (S, V).snd
[PROOFSTEP]
simpa using mem_of_mem_nhds hV
[GOAL]
case neg
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : a ∈ Metric.ball 0 r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : ¬a = 0
⊢ ↑φ (a • u) x ∈ (S, V).snd
[PROOFSTEP]
rw [mem_ball_zero_iff] at ha
[GOAL]
case neg
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : ¬a = 0
⊢ ↑φ (a • u) x ∈ (S, V).snd
[PROOFSTEP]
rw [SMulHomClass.map_smul, Pi.smul_apply]
[GOAL]
case neg
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : ¬a = 0
⊢ a • ↑φ u x ∈ (S, V).snd
[PROOFSTEP]
have : φ u x ∈ a⁻¹ • V := by
  have ha0 : 0 < ‖a‖ := norm_pos_iff.mpr ha0
  refine' (hr a⁻¹ _) (Set.mem_image_of_mem (φ u) hx)
  rw [norm_inv, le_inv hrpos ha0]
  exact ha.le
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : ¬a = 0
⊢ ↑φ u x ∈ a⁻¹ • V
[PROOFSTEP]
have ha0 : 0 < ‖a‖ := norm_pos_iff.mpr ha0
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0✝ : ¬a = 0
ha0 : 0 < ‖a‖
⊢ ↑φ u x ∈ a⁻¹ • V
[PROOFSTEP]
refine' (hr a⁻¹ _) (Set.mem_image_of_mem (φ u) hx)
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0✝ : ¬a = 0
ha0 : 0 < ‖a‖
⊢ r ≤ ‖a⁻¹‖
[PROOFSTEP]
rw [norm_inv, le_inv hrpos ha0]
[GOAL]
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝ : TopologicalAddGroup H
this : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0✝ : ¬a = 0
ha0 : 0 < ‖a‖
⊢ ‖a‖ ≤ r⁻¹
[PROOFSTEP]
exact ha.le
[GOAL]
case neg
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup H
inst✝⁷ : Module 𝕜 H
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace H
inst✝³ : UniformSpace E
inst✝² : UniformAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝ : LinearMapClass hom 𝕜 H (α →ᵤ[𝔖] E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
φ : hom
hφ : Inducing ↑φ
h : ∀ (u : H) (s : Set α), s ∈ 𝔖 → Bornology.IsVonNBounded 𝕜 (↑φ u '' s)
this✝¹ : TopologicalAddGroup H
this✝ : HasBasis (𝓝 0) (fun SV => SV.fst ∈ 𝔖 ∧ SV.snd ∈ 𝓝 0) fun i => ↑φ ⁻¹' {f | ∀ (x : α), x ∈ i.fst → f x ∈ i.snd}
u : H
S : Set α
V : Set E
hS : (S, V).fst ∈ 𝔖
hV : (S, V).snd ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜), r ≤ ‖a‖ → ↑φ u '' S ⊆ a • (S, V).snd
a : 𝕜
ha : ‖a‖ < r⁻¹
x : α
hx : x ∈ (S, V).fst
ha0 : ¬a = 0
this : ↑φ u x ∈ a⁻¹ • V
⊢ a • ↑φ u x ∈ (S, V).snd
[PROOFSTEP]
rwa [Set.mem_inv_smul_set_iff₀ ha0] at this


[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
simp only [← Ici_diff_left, continuousWithinAt_diff_self]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iic a] a ⊔ 𝓝[Ici a] a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iio a] a ⊔ 𝓝[Ici a] a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iic a] a ⊔ 𝓝[Ioi a] a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
⊢ 𝓝[Iio a] a ⊔ 𝓝[Ioi a] a = 𝓝[{a}ᶜ] a
[PROOFSTEP]
rw [← nhdsWithin_union, Iio_union_Ioi]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhds_left_sup_nhds_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a
[PROOFSTEP]
rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic, continuousAt_iff_continuous_left_right]


[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