case h
𝕜 : Type ?u.33039
E : Type u_1
F : Type ?u.33045
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x✝ : E
⊢ gauge ∅ x✝ = OfNat.ofNat 0 x✝
𝕜 : Type ?u.33039
E : Type u_1
F : Type ?u.33045
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
⊢ gauge ∅ = 0
ext
no goals
case h
𝕜 : Type ?u.33039
E : Type u_1
F : Type ?u.33045
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x✝ : E
⊢ gauge ∅ x✝ = OfNat.ofNat 0 x✝
simp only [gauge_def', Real.sInf_empty, mem_empty_iff_false, Pi.zero_apply, sep_false]