case h
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Iio a ↔ x ∈ Iio (r • a)
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
⊢ r • Iio a = Iio (r • a)
ext x
case h
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) ↔ x < r * a
case h
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ r • Iio a ↔ x ∈ Iio (r • a)
simp only [mem_smul_set, smul_eq_mul, mem_Iio]
case h.mp
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) → x < r * a

case h.mpr
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x < r * a → ∃ y, y < a ∧ r * y = x
case h
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) ↔ x < r * a
constructor
case h.mp.intro.intro
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w < a
⊢ r * a_w < r * a
case h.mp
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y < a ∧ r * y = x) → x < r * a
rintro ⟨a_w, a_h_left, rfl⟩
no goals
case h.mp.intro.intro
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
a_w : K
a_h_left : a_w < a
⊢ r * a_w < r * a
exact (mul_lt_mul_left hr).mpr a_h_left
case h.mpr
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ ∃ y, y < a ∧ r * y = x
case h.mpr
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x < r * a → ∃ y, y < a ∧ r * y = x
rintro h
case h.mpr
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a ∧ r * (x / r) = x
case h.mpr
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ ∃ y, y < a ∧ r * y = x
use x / r
case h.mpr.left
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a

case h.mpr.right
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
case h.mpr
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a ∧ r * (x / r) = x
constructor
case h.mpr.right
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
case h.mpr.left
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ x / r < a

case h.mpr.right
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
exact (div_lt_iff' hr).mpr h
no goals
case h.mpr.right
α : Type ?u.63203
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x < r * a
⊢ r * (x / r) = x
exact mul_div_cancel' _ (ne_of_gt hr)