[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ sSup s⁻¹ = (sInf s)⁻¹
[PROOFSTEP]
rw [← image_inv, sSup_image]
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ ⨆ (a : α) (_ : a ∈ s), a⁻¹ = (sInf s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_sInf _).symm
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ sInf s⁻¹ = (sSup s)⁻¹
[PROOFSTEP]
rw [← image_inv, sInf_image]
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s✝ t s : Set α
⊢ ⨅ (a : α) (_ : a ∈ s), a⁻¹ = (sSup s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_sSup _).symm
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
⊢ sSup (s / t) = sSup s / sInf t
[PROOFSTEP]
simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]
[GOAL]
α : Type u_1
inst✝³ : CompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
⊢ sInf (s / t) = sInf s / sSup t
[PROOFSTEP]
simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup s⁻¹ = (sInf s)⁻¹
[PROOFSTEP]
rw [← image_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup (Inv.inv '' s) = (sInf s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_csInf' hs₀ hs₁).symm
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
⊢ sInf s⁻¹ = (sSup s)⁻¹
[PROOFSTEP]
rw [← image_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
⊢ sInf (Inv.inv '' s) = (sSup s)⁻¹
[PROOFSTEP]
exact ((OrderIso.inv α).map_csSup' hs₀ hs₁).symm
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddBelow t
⊢ sSup (s / t) = sSup s / sInf t
[PROOFSTEP]
rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t
[PROOFSTEP]
rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioo a b = Ioo (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioo a b ↔ x ∈ Ioo (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y < b) ∧ r * y = x) ↔ r * a < x ∧ x < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y < b) ∧ r * y = x) → r * a < x ∧ x < r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a✝ < r * a ∧ r * a < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a✝ < r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a < x ∧ x < r * b → ∃ y, (a < y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x < r * b
⊢ ∃ y, (a < y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x < r * b
⊢ (a < x / r ∧ x / r < b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x < r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Icc a b = Icc (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Icc a b ↔ x ∈ Icc (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Icc]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x) ↔ r * a ≤ x ∧ x ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x) → r * a ≤ x ∧ x ≤ r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a✝ ≤ r * a ∧ r * a ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a✝ ≤ r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a ≤ x ∧ x ≤ r * b → ∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x ≤ r * b
⊢ ∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x ≤ r * b
⊢ (a ≤ x / r ∧ x / r ≤ b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(le_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x ≤ r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ico a b = Ico (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ico a b ↔ x ∈ Ico (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ico]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y < b) ∧ r * y = x) ↔ r * a ≤ x ∧ x < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a ≤ y ∧ y < b) ∧ r * y = x) → r * a ≤ x ∧ x < r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a✝ ≤ r * a ∧ r * a < r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a✝ ≤ r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ ≤ a
a_h_left_right : a < b
⊢ r * a < r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a ≤ x ∧ x < r * b → ∃ y, (a ≤ y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x < r * b
⊢ ∃ y, (a ≤ y ∧ y < b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x < r * b
⊢ (a ≤ x / r ∧ x / r < b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(le_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a ≤ x
a_right : x < r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioc a b = Ioc (r • a) (r • b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioc a b ↔ x ∈ Ioc (r • a) (r • b)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y ≤ b) ∧ r * y = x) ↔ r * a < x ∧ x ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, (a < y ∧ y ≤ b) ∧ r * y = x) → r * a < x ∧ x ≤ r * b
[PROOFSTEP]
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a✝ < r * a ∧ r * a ≤ r * b
[PROOFSTEP]
constructor
[GOAL]
case h.mp.intro.intro.intro.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a✝ < r * a
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left_left
[GOAL]
case h.mp.intro.intro.intro.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a✝ b r : K
hr : 0 < r
a : K
a_h_left_left : a✝ < a
a_h_left_right : a ≤ b
⊢ r * a ≤ r * b
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left_right
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a < x ∧ x ≤ r * b → ∃ y, (a < y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
rintro ⟨a_left, a_right⟩
[GOAL]
case h.mpr.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x ≤ r * b
⊢ ∃ y, (a < y ∧ y ≤ b) ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x ≤ r * b
⊢ (a < x / r ∧ x / r ≤ b) ∧ r * (x / r) = x
[PROOFSTEP]
refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
a_left : r * a < x
a_right : x ≤ r * b
⊢ r * (x / r) = x
[PROOFSTEP]
rw [mul_div_cancel' _ (ne_of_gt hr)]
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioi a = Ioi (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioi a ↔ x ∈ Ioi (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, a < y ∧ r * y = x) ↔ r * a < x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, a < y ∧ r * y = x) → r * a < x
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a < a_w
⊢ r * a < r * a_w
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ r * a < x → ∃ y, a < y ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ ∃ y, a < y ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ a < x / r ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ a < x / r
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ r * (x / r) = x
[PROOFSTEP]
exact (lt_div_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : r * a < x
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Iio a = Iio (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Iio a ↔ x ∈ Iio (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Iio]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) ↔ x < r * a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) → x < r * a
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w < a
⊢ r * a_w < r * a
[PROOFSTEP]
exact (mul_lt_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x < r * a → ∃ y, y < a ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ ∃ y, y < a ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
[PROOFSTEP]
exact (div_lt_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ici a = Ici (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ici a ↔ x ∈ Ici (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Ici a ∧ r * y = x) ↔ x ∈ Ici (r * a)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Ici a ∧ r * y = x) → x ∈ Ici (r * a)
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w ∈ Ici a
⊢ r * a_w ∈ Ici (r * a)
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ Ici (r * a) → ∃ y, y ∈ Ici a ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ ∃ y, y ∈ Ici a ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ x / r ∈ Ici a ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ x / r ∈ Ici a
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact (le_div_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Ici (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
[GOAL]
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Iic a = Iic (r • a)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Iic a ↔ x ∈ Iic (r • a)
[PROOFSTEP]
simp only [mem_smul_set, smul_eq_mul, mem_Iio]
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Iic a ∧ r * y = x) ↔ x ∈ Iic (r * a)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Iic a ∧ r * y = x) → x ∈ Iic (r * a)
[PROOFSTEP]
rintro ⟨a_w, a_h_left, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w ∈ Iic a
⊢ r * a_w ∈ Iic (r * a)
[PROOFSTEP]
exact (mul_le_mul_left hr).mpr a_h_left
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ Iic (r * a) → ∃ y, y ∈ Iic a ∧ r * y = x
[PROOFSTEP]
rintro h
[GOAL]
case h.mpr
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ ∃ y, y ∈ Iic a ∧ r * y = x
[PROOFSTEP]
use x / r
[GOAL]
case h
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ x / r ∈ Iic a ∧ r * (x / r) = x
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ x / r ∈ Iic a
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact (div_le_iff' hr).mpr h
[GOAL]
case h.right
α : Type u_1
K : Type u_2
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ r * (x / r) = x
[PROOFSTEP]
exact mul_div_cancel' _ (ne_of_gt hr)
