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

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

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