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

case h.inr
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = OfNat.ofNat 0 x
case h
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = OfNat.ofNat 0 x
obtain rfl | hx := eq_or_ne x 0
no goals
case h.inl
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ 0} = OfNat.ofNat 0 0
simp only [csInf_Ioi, mem_zero, Pi.zero_apply, eq_self_iff_true, sep_true, smul_zero]
case h.inr
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = 0
case h.inr
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = OfNat.ofNat 0 x
simp only [mem_zero, Pi.zero_apply, inv_eq_zero, smul_eq_zero]
case h.e'_2.h.e'_3
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hx : x ≠ 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = ∅
case h.inr
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = 0
convert Real.sInf_empty
no goals
case h.e'_2.h.e'_3
𝕜 : Type ?u.24181
E : Type u_1
F : Type ?u.24187
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hx : x ≠ 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = ∅
exact eq_empty_iff_forall_not_mem.2 fun r hr => hr.2.elim (ne_of_gt hr.1) hx