𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
⊢ sInf {r | 0 < r ∧ x ∈ r • s} = sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
⊢ gauge s x = sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
rw [gauge]
case h
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
⊢ {r | 0 < r ∧ x ∈ r • s} = {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
⊢ sInf {r | 0 < r ∧ x ∈ r • s} = sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
apply congr_arg
case h.h
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
x✝ : ℝ
⊢ x✝ ∈ {r | 0 < r ∧ x ∈ r • s} ↔ x✝ ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
case h
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
⊢ {r | 0 < r ∧ x ∈ r • s} = {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
ext
case h.h
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
x✝ : ℝ
⊢ 0 < x✝ ∧ x ∈ x✝ • s ↔ 0 < x✝ ∧ x✝⁻¹ • x ∈ s
case h.h
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
x✝ : ℝ
⊢ x✝ ∈ {r | 0 < r ∧ x ∈ r • s} ↔ x✝ ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
simp only [mem_setOf, mem_Ioi]
no goals
case h.h
𝕜 : Type ?u.5140
E : Type u_1
F : Type ?u.5146
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
x✝ : ℝ
⊢ 0 < x✝ ∧ x ∈ x✝ • s ↔ 0 < x✝ ∧ x✝⁻¹ • x ∈ s
exact and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _