𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
⊢ Bornology.IsVonNBounded 𝕜 s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
⊢ Bornology.IsVonNBounded 𝕜 s
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
⊢ Bornology.IsVonNBounded 𝕜 s
intro U hU
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 (0 + 0))
⊢ Absorbs 𝕜 U s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U s
have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 ((0 : E) + (0 : E))) :=
  tendsto_add
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
⊢ Absorbs 𝕜 U s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 (0 + 0))
⊢ Absorbs 𝕜 U s
rw [add_zero] at h
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    id i.fst ×ˢ id i.snd
⊢ Absorbs 𝕜 U s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
⊢ Absorbs 𝕜 U s
have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
⊢ Absorbs 𝕜 U s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    id i.fst ×ˢ id i.snd
⊢ Absorbs 𝕜 U s
simp_rw [← nhds_prod_eq, id.def] at h'
case intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
⊢ Absorbs 𝕜 U s
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
⊢ Absorbs 𝕜 U s
rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ Absorbs 𝕜 U s
case intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
⊢ Absorbs 𝕜 U s
rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ Absorbs 𝕜 U (⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd)
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ Absorbs 𝕜 U s
refine' Absorbs.mono_right _ hs
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ ∀ (i : E), i ∈ t → Absorbs 𝕜 U (i +ᵥ x.snd)
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ Absorbs 𝕜 U (⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd)
rw [ht.absorbs_iUnion]
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
⊢ ∀ (i : E), i ∈ t → Absorbs 𝕜 U (i +ᵥ x.snd)
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ ∀ (i : E), i ∈ t → Absorbs 𝕜 U (i +ᵥ x.snd)
have hx_fstsnd : x.fst + x.snd ⊆ U := by
  intro z hz
  rcases Set.mem_add.mp hz with ⟨z1, z2, hz1, hz2, hz⟩
  have hz' : (z1, z2) ∈ x.fst ×ˢ x.snd := ⟨hz1, hz2⟩
  simpa only [hz] using h'' hz'
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.fst + x.snd) (y +ᵥ x.snd)
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
⊢ ∀ (i : E), i ∈ t → Absorbs 𝕜 U (i +ᵥ x.snd)
refine' fun y _ => Absorbs.mono_left _ hx_fstsnd
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.fst + x.snd) ({y} + x.snd)
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.fst + x.snd) (y +ᵥ x.snd)
rw [← Set.singleton_vadd, vadd_eq_add]
no goals
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.fst + x.snd) ({y} + x.snd)
exact (absorbent_nhds_zero hx.1.1).absorbs.add hx.2.2.absorbs_self
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz : z ∈ x.fst + x.snd
⊢ z ∈ U
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ x.fst + x.snd ⊆ U
intro z hz
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz✝ : z ∈ x.fst + x.snd
z1 z2 : E
hz1 : z1 ∈ x.fst
hz2 : z2 ∈ x.snd
hz : z1 + z2 = z
⊢ z ∈ U
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz : z ∈ x.fst + x.snd
⊢ z ∈ U
rcases Set.mem_add.mp hz with ⟨z1, z2, hz1, hz2, hz⟩
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz✝ : z ∈ x.fst + x.snd
z1 z2 : E
hz1 : z1 ∈ x.fst
hz2 : z2 ∈ x.snd
hz : z1 + z2 = z
hz' : (z1, z2) ∈ x.fst ×ˢ x.snd
⊢ z ∈ U
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz✝ : z ∈ x.fst + x.snd
z1 z2 : E
hz1 : z1 ∈ x.fst
hz2 : z2 ∈ x.snd
hz : z1 + z2 = z
⊢ z ∈ U
have hz' : (z1, z2) ∈ x.fst ×ˢ x.snd := ⟨hz1, hz2⟩
no goals
case intro.intro.intro.intro
𝕜 : Type u_2
𝕜' : Type ?u.221754
E : Type u_1
E' : Type ?u.221760
F : Type ?u.221763
ι : Type ?u.221766
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz✝ : z ∈ x.fst + x.snd
z1 z2 : E
hz1 : z1 ∈ x.fst
hz2 : z2 ∈ x.snd
hz : z1 + z2 = z
hz' : (z1, z2) ∈ x.fst ×ˢ x.snd
⊢ z ∈ U
simpa only [hz] using h'' hz'