𝕜 : Type ?u.36600
E : Type u_1
F : Type ?u.36606
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
x : E
this : ∀ (x : E), -x ∈ s ↔ x ∈ s
⊢ gauge s (-x) = gauge s x
𝕜 : Type ?u.36600
E : Type u_1
F : Type ?u.36606
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
x : E
⊢ gauge s (-x) = gauge s x
have : ∀ x, -x ∈ s ↔ x ∈ s := fun x => ⟨fun h => by simpa using symmetric _ h, symmetric x⟩
no goals
𝕜 : Type ?u.36600
E : Type u_1
F : Type ?u.36606
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
x : E
this : ∀ (x : E), -x ∈ s ↔ x ∈ s
⊢ gauge s (-x) = gauge s x
simp_rw [gauge_def', smul_neg, this]
no goals
𝕜 : Type ?u.36600
E : Type u_1
F : Type ?u.36606
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
x✝ x : E
h : -x ∈ s
⊢ x ∈ s
simpa using symmetric _ h