case inl
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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 : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖0‖
⊢ a • x ∈ s ↔ 0 • x ∈ s

case inr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
⊢ a • x ∈ s ↔ b • x ∈ s
obtain rfl | hb := eq_or_ne b 0
case inr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
case inr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
have ha : a ≠ 0 := norm_ne_zero_iff.1 (ne_of_eq_of_ne h <| norm_ne_zero_iff.2 hb)
case inl
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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 : 𝕜
hs : Balanced 𝕜 s
h : a = 0
⊢ a • x ∈ s ↔ 0 • x ∈ s
case inl
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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 : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖0‖
⊢ a • x ∈ s ↔ 0 • x ∈ s
rw [norm_zero, norm_eq_zero] at h
no goals
case inl
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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 : 𝕜
hs : Balanced 𝕜 s
h : a = 0
⊢ a • x ∈ s ↔ 0 • x ∈ s
rw [h]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹) • b • x ∈ s
case inr.mpr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹ * b) • x ∈ s
rw [← smul_eq_mul, smul_assoc]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ ‖a * b⁻¹‖ ≤ 1
case inr.mpr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹) • b • x ∈ s
refine' hs.smul_mem _ h'
no goals
case inr.mpr
𝕜 : Type u_1
𝕝 : Type ?u.103382
E : Type u_2
ι : Sort ?u.103388
κ : ι → Sort ?u.103393
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
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ ‖a * b⁻¹‖ ≤ 1
simp [← h, ha]