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

case h.mpr
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ Iic (r * a) → ∃ y, y ∈ Iic a ∧ r * y = x
case h
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Iic a ∧ r * y = x) ↔ x ∈ Iic (r * a)
constructor
case h.mp.intro.intro
α : Type ?u.66941
K : Type u_1
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)
case h.mp
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ (∃ y, y ∈ Iic a ∧ r * y = x) → x ∈ Iic (r * a)
rintro ⟨a_w, a_h_left, rfl⟩
no goals
case h.mp.intro.intro
α : Type ?u.66941
K : Type u_1
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)
exact (mul_le_mul_left hr).mpr a_h_left
case h.mpr
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ ∃ y, y ∈ Iic a ∧ r * y = x
case h.mpr
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
⊢ x ∈ Iic (r * a) → ∃ y, y ∈ Iic a ∧ r * y = x
rintro h
case h.mpr
α : Type ?u.66941
K : Type u_1
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
case h.mpr
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ ∃ y, y ∈ Iic a ∧ r * y = x
use x / r
case h.mpr.left
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ x / r ∈ Iic a

case h.mpr.right
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ r * (x / r) = x
case h.mpr
α : Type ?u.66941
K : Type u_1
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
constructor
case h.mpr.right
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ r * (x / r) = x
case h.mpr.left
α : Type ?u.66941
K : Type u_1
inst✝ : LinearOrderedField K
a b r : K
hr : 0 < r
x : K
h : x ∈ Iic (r * a)
⊢ x / r ∈ Iic a

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