case intro
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
⊢ a ≤ x
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
no goals
case intro
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε
exact h _ ((lt_mul_iff_one_lt_right' b).1 hxb)