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

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

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

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