case inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖0‖
⊢ a • s ⊆ 0 • s

case inr
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
⊢ a • s ⊆ b • s
obtain rfl | hb := eq_or_ne b 0
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (fun x => a • x) x ∈ b • s
case inr
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s
rintro _ ⟨x, hx, rfl⟩
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ b⁻¹ • a • x ∈ s
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (fun x => a • x) x ∈ b • s
refine' ⟨b⁻¹ • a • x, _, smul_inv_smul₀ hb _⟩
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (b⁻¹ • a) • x ∈ s
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ b⁻¹ • a • x ∈ s
rw [← smul_assoc]
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖b⁻¹ • a‖ ≤ 1
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (b⁻¹ • a) • x ∈ s
refine' hs _ _ (smul_mem_smul_set hx)
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖a‖ / ‖b‖ ≤ 1
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖b⁻¹ • a‖ ≤ 1
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
no goals
case inr.intro.intro
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖a‖ / ‖b‖ ≤ 1
exact div_le_one_of_le h (norm_nonneg _)
case inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ a • s ⊆ 0 • s
case inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖0‖
⊢ a • s ⊆ 0 • s
rw [norm_zero] at h
case inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ 0 • s ⊆ 0 • s
case inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ a • s ⊆ 0 • s
rw [norm_eq_zero.1 (h.antisymm <| norm_nonneg _)]
case inl.inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ 0 • ∅ ⊆ 0 • ∅

case inl.inr
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 • s ⊆ 0 • s
case inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ 0 • s ⊆ 0 • s
obtain rfl | h := s.eq_empty_or_nonempty
case inl.inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ ∅ ⊆ ∅
case inl.inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ 0 • ∅ ⊆ 0 • ∅
simp_rw [smul_set_empty]
no goals
case inl.inl
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ ∅ ⊆ ∅
rfl
case inl.inr
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 ⊆ 0
case inl.inr
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 • s ⊆ 0 • s
simp_rw [zero_smul_set h]
no goals
case inl.inr
𝕜 : Type u_3
𝕝 : Type u_1
E : Type u_2
ι : Sort ?u.58606
κ : ι → Sort ?u.58611
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 ⊆ 0
rfl