case inl
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
x : E
ha : 0 ≤ 0
⊢ gauge s (0 • x) = 0 • gauge s x

case inr
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ gauge s (a • x) = a • gauge s x
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
⊢ gauge s (a • x) = a • gauge s x
obtain rfl | ha' := ha.eq_or_lt
case inr
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = sInf (a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s})
case inr
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ gauge s (a • x) = a • gauge s x
rw [gauge_def', gauge_def', ← Real.sInf_smul_of_nonneg ha]
case inr.e_a
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
case inr
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = sInf (a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s})
congr 1
case inr.e_a.h
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} ↔ r ∈ a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
case inr.e_a
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
⊢ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
ext r
case inr.e_a.h
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s ↔ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r
case inr.e_a.h
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} ↔ r ∈ a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
simp_rw [Set.mem_smul_set, Set.mem_sep_iff]
case inr.e_a.h.mp
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s → ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r

case inr.e_a.h.mpr
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ (∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r) → r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s
case inr.e_a.h
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s ↔ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r
constructor
no goals
case inl
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
x : E
ha : 0 ≤ 0
⊢ gauge s (0 • x) = 0 • gauge s x
rw [zero_smul, gauge_zero, zero_smul]
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • a • x ∈ s
⊢ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r
case inr.e_a.h.mp
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s → ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r
rintro ⟨hr, hx⟩
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : r⁻¹ • a • x ∈ s
hr : 0 < r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • a • x ∈ s
⊢ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r
simp_rw [mem_Ioi] at hr⊢
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : r⁻¹ • a • x ∈ s
hr : 0 < r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
have := smul_pos (inv_pos.2 ha') hr
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ (a⁻¹ • r)⁻¹ • x ∈ s
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
refine' ⟨a⁻¹ • r, ⟨this, _⟩, smul_inv_smul₀ ha'.ne' _⟩
no goals
case inr.e_a.h.mp.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ (a⁻¹ • r)⁻¹ • x ∈ s
rwa [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc,
  mem_smul_set_iff_inv_smul_mem₀ (inv_ne_zero ha'.ne'), inv_inv]
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • x ∈ s
⊢ a • r ∈ Ioi 0 ∧ (a • r)⁻¹ • a • x ∈ s
case inr.e_a.h.mpr
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ (∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r) → r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s
rintro ⟨r, ⟨hr, hx⟩, rfl⟩
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • x ∈ s
⊢ a • r ∈ Ioi 0 ∧ (a • r)⁻¹ • a • x ∈ s
rw [mem_Ioi] at hr⊢
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
have := smul_pos ha' hr
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ (a • r)⁻¹ • a • x ∈ s
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
refine' ⟨this, _⟩
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ a • x ∈ a • r • s
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ (a • r)⁻¹ • a • x ∈ s
rw [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc]
no goals
case inr.e_a.h.mpr.intro.intro.intro
𝕜 : Type ?u.102151
E : Type u_2
F : Type ?u.102157
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s✝ t : Set E
a✝ : ℝ
α : Type u_1
inst✝⁴ : LinearOrderedField α
inst✝³ : MulActionWithZero α ℝ
inst✝² : OrderedSMul α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ a • x ∈ a • r • s
exact smul_mem_smul_set hx