Theorem: float_real_le_1_le (HOLFloat/Float_theorem.lean)

State before:
x : ℝ
m : ℤ
⊢ 0 < x → 1 ≤ m → x ≤ ↑m * x
Tactic:
intro h₁ h₂
State after:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ x ≤ ↑m * x

State before:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ x ≤ ↑m * x
Tactic:
rw [le_mul_iff_one_le_left]
State after:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 1 ≤ ↑m

x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x

State before:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 1 ≤ ↑m

x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x
Tactic:
norm_cast
State after:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x

State before:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x
Tactic:
exact h₁
State after:
no goals