case refine'_1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ a ≠ 0

case refine'_2
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ A ⊆ a • A
refine' (subset_set_smul_iff₀ _).2 (hA a⁻¹ _)
case refine'_1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖0‖
⊢ False
case refine'_1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ a ≠ 0
rintro rfl
case refine'_1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ 0
⊢ False
case refine'_1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖0‖
⊢ False
rw [norm_zero] at ha
no goals
case refine'_1
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ 0
⊢ False
exact zero_lt_one.not_le ha
case refine'_2
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1
case refine'_2
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1
rw [norm_inv]
no goals
case refine'_2
𝕜 : Type u_1
𝕝 : Type ?u.86571
E : Type u_2
ι : Sort ?u.86577
κ : ι → Sort ?u.86582
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 : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1
exact inv_le_one ha