𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
⊢ Balanced 𝕜 (balancedHull 𝕜 s)
intro a ha
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i j, x ∈ a • i • s) → ∃ i j, x ∈ i • s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s
simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ ∃ i j, x ∈ i • s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i j, x ∈ a • i • s) → ∃ i j, x ∈ i • s
rintro x ⟨r, hr, hx⟩
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx✝ : x ∈ a • r • s
hx : x ∈ (a • r) • s
⊢ ∃ i j, x ∈ i • s
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ ∃ i j, x ∈ i • s
rw [← smul_assoc] at hx
no goals
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.26762
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx✝ : x ∈ a • r • s
hx : x ∈ (a • r) • s
⊢ ∃ i j, x ∈ i • s
exact ⟨a • r, (SeminormedRing.norm_mul _ _).trans (mul_le_one ha (norm_nonneg r) hr), hx⟩