𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
⊢ gauge s 0 = 0
rw [gauge_def']
case pos
𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
h : 0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

case neg
𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
h : ¬0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
by_cases h : (0 : E) ∈ s
no goals
case pos
𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
h : 0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
simp only [smul_zero, sep_true, h, csInf_Ioi]
no goals
case neg
𝕜 : Type ?u.20500
E : Type u_1
F : Type ?u.20506
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
h : ¬0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
simp only [smul_zero, sep_false, h, Real.sInf_empty]