case inl
𝕜 : Type ?u.46236
E : Type u_1
F : Type ?u.46242
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
ha : 0 ≤ 0
hx : x ∈ 0 • s
⊢ gauge s x ≤ 0

case inr
𝕜 : Type ?u.46236
E : Type u_1
F : Type ?u.46242
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a
𝕜 : Type ?u.46236
E : Type u_1
F : Type ?u.46242
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
ha : 0 ≤ a
hx : x ∈ a • s
⊢ gauge s x ≤ a
obtain rfl | ha' := ha.eq_or_lt
no goals
case inl
𝕜 : Type ?u.46236
E : Type u_1
F : Type ?u.46242
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
ha : 0 ≤ 0
hx : x ∈ 0 • s
⊢ gauge s x ≤ 0
rw [mem_singleton_iff.1 (zero_smul_set_subset _ hx), gauge_zero]
no goals
case inr
𝕜 : Type ?u.46236
E : Type u_1
F : Type ?u.46242
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a
exact csInf_le gauge_set_bddBelow ⟨ha', hx⟩