𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ sInf {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} = sInf {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (‖r‖ • x) = gauge s (r • x)
unfold gauge
case e_a.h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ sInf {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} = sInf {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
congr with θ
case e_a.h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ↑‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
case e_a.h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
rw [@IsROrC.real_smul_eq_coe_smul 𝕜]
case e_a.h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
⊢ ‖↑‖r‖‖ = ‖r‖
case e_a.h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ θ ∈ {r_1 | 0 < r_1 ∧ ↑‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
refine' and_congr_right fun hθ => (hs.smul _).mem_smul_iff _
no goals
case e_a.h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.160196
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
a : ℝ
inst✝² : IsROrC 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
⊢ ‖↑‖r‖‖ = ‖r‖
rw [IsROrC.norm_ofReal, abs_norm]