𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
⊢ gauge (a • s) = gauge (abs a • s)
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
⊢ gauge (a • s) = (abs a)⁻¹ • gauge s
rw [← gauge_smul_left_of_nonneg (abs_nonneg a)]
case inl
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = a
⊢ gauge (a • s) = gauge (abs a • s)

case inr
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ gauge (a • s) = gauge (abs a • s)
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
⊢ gauge (a • s) = gauge (abs a • s)
obtain h | h := abs_choice a
no goals
case inl
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = a
⊢ gauge (a • s) = gauge (abs a • s)
rw [h]
case inr
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ gauge (a • s) = gauge (a • -s)
case inr
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ gauge (a • s) = gauge (abs a • s)
rw [h, Set.neg_smul_set, ← Set.smul_set_neg]
case inr.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ a • s = a • -s
case inr
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ gauge (a • s) = gauge (a • -s)
apply congr_arg
case inr.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ s = -s
case inr.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ a • s = a • -s
apply congr_arg
case inr.h.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
y : E
⊢ y ∈ s ↔ y ∈ -s
case inr.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
⊢ s = -s
ext y
case inr.h.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
y : E
hy : y ∈ -s
⊢ y ∈ s
case inr.h.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
y : E
⊢ y ∈ s ↔ y ∈ -s
refine' ⟨symmetric _, fun hy => _⟩
case inr.h.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
y : E
hy : y ∈ -s
⊢ - -y ∈ s
case inr.h.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
y : E
hy : y ∈ -s
⊢ y ∈ s
rw [← neg_neg y]
no goals
case inr.h.h.h
𝕜 : Type ?u.145387
E : Type u_2
F : Type ?u.145393
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁶ : LinearOrderedField α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : OrderedSMul α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ (x : E), x ∈ s → -x ∈ s
a : α
h : abs a = -a
y : E
hy : y ∈ -s
⊢ - -y ∈ s
exact symmetric _ hy