case h
α : Type ?u.59044
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioc a b ↔ x ∈ Ioc (r • a) (r • b)
α : Type ?u.59044
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Ioc a b = Ioc (r • a) (r • b)
ext x
case h
α : Type ?u.59044
K : Type u_1
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
case h
α : Type ?u.59044
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Ioc a b ↔ x ∈ Ioc (r • a) (r • b)
simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
case h.mp
α : Type ?u.59044
K : Type u_1
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

case h.mpr
α : Type ?u.59044
K : Type u_1
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
case h
α : Type ?u.59044
K : Type u_1
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
constructor
case h.mp.intro.intro.intro
α : Type ?u.59044
K : Type u_1
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
case h.mp
α : Type ?u.59044
K : Type u_1
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
rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
case h.mp.intro.intro.intro.left
α : Type ?u.59044
K : Type u_1
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.59044
K : Type u_1
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
case h.mp.intro.intro.intro
α : Type ?u.59044
K : Type u_1
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
constructor
case h.mp.intro.intro.intro.right
α : Type ?u.59044
K : Type u_1
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
case h.mp.intro.intro.intro.left
α : Type ?u.59044
K : Type u_1
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.59044
K : Type u_1
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
exact (mul_lt_mul_left hr).mpr a_h_left_left
no goals
case h.mp.intro.intro.intro.right
α : Type ?u.59044
K : Type u_1
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
exact (mul_le_mul_left hr).mpr a_h_left_right
case h.mpr.intro
α : Type ?u.59044
K : Type u_1
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
case h.mpr
α : Type ?u.59044
K : Type u_1
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
rintro ⟨a_left, a_right⟩
case h.mpr.intro
α : Type ?u.59044
K : Type u_1
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
case h.mpr.intro
α : Type ?u.59044
K : Type u_1
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
use x / r
case h.mpr.intro
α : Type ?u.59044
K : Type u_1
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
case h.mpr.intro
α : Type ?u.59044
K : Type u_1
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
refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
no goals
case h.mpr.intro
α : Type ?u.59044
K : Type u_1
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
rw [mul_div_cancel' _ (ne_of_gt hr)]