-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem TotallyBounded.isVonNBounded {s : Set E} (hs : TotallyBounded s) :
    Bornology.IsVonNBounded 𝕜 s

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x => x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U s

Tactic:
refine Absorbs.mono_right ?_ hs

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x => x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x => x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)

Tactic:
rw [ht.absorbs_biUnion]

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x => x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => id i.1 ×ˢ id i.2
⊢ Absorbs 𝕜 U s

Tactic:
simp_rw [← nhds_prod_eq, id] at h'

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => i.1 ×ˢ i.2
⊢ Absorbs 𝕜 U s

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk h✝
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i => (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i => i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x => x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)

Tactic:
exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
if h : ∃ x : 𝕜, 1 < ‖x‖ then
  letI : NontriviallyNormedField 𝕜 := ⟨h⟩
  rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
  intro U hU
  have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
    continuous_add.tendsto' _ _ (zero_add _)
  have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
  simp_rw [← nhds_prod_eq, id] at h'
  rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
  rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
  refine Absorbs.mono_right ?_ hs
  rw [ht.absorbs_biUnion]
  have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
    h'' <| mk_mem_prod hz1 hz2
  refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
  exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
else
  haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
  exact Bornology.IsVonNBounded.of_boundedSpace

Result:
no goals