α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ ↑⌈x⌉₊ < 1.38 * x
refine' (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le _
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ (1.38 - 1) * x
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x
rw [← le_sub_iff_add_le', ← sub_one_mul]
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 1 ≤ (1.38 - 1) * x
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ (1.38 - 1) * x
have : (1.38 : ℝ) = 69 / 50 := by norm_num
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 0 < 50 / 19
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 1 ≤ (1.38 - 1) * x
rwa [this, show (69 / 50 - 1 : ℝ) = (50 / 19)⁻¹ by norm_num1, ←
  div_eq_inv_mul, one_le_div]
no goals
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 0 < 50 / 19
norm_num1
no goals
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 0 ≤ 50 / 19
norm_num
no goals
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1.38 = 69 / 50
norm_num
no goals
α : Type ?u.699750
β : Type ?u.699753
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 69 / 50 - 1 = (50 / 19)⁻¹
norm_num1