ceil_log2_le_floor_four_add_log2

lemma ceil_log2_le_floor_four_add_log2 {l : ℝ} (hl : 2 ≤ l) :    ⌈Real.logb 2 ((l + 6 / 5) / 5⁻¹)⌉₊ ≤ ⌊4 + Real.logb 2 l⌋₊ := by  have : 2 ≤ Real.logb 2 (l + 6 / 5) + Real.logb 2 5 :=    calc      _ ≥ Real.logb 2 (2 ^ (0 : ℝ)) + Real.logb 2 (2 ^ (2 : ℝ)) :=        add_le_add          (Real.logb_le_logb_of_le one_lt_two (by positivity) (by linarith))          (Real.logb_le_logb_of_le one_lt_two (by positivity) (by norm_num))      _ ≥ _ := by simp_rw [Real.logb_rpow zero_lt_two one_lt_two.ne']; norm_num  rw [div_inv_eq_mul, Real.logb_mul (by positivity) (by positivity), Nat.le_floor_iff']  · calc      _ ≤ 1 + Real.logb 2 (l + 6 / 5) + Real.logb 2 5 := by        rw [add_rotate]; exact (Nat.ceil_lt_add_one (zero_le_two.trans this)).le      _ ≤ 1 + Real.logb 2 (8 / 5 * l) + Real.logb 2 5 := by        gcongr        · exact one_lt_two        · linarith      _ = _ := by        rw [add_assoc, ← Real.logb_mul (by positivity) (by positivity), ← mul_rotate,          show (5 : ℝ) * (8 / 5) = 2 ^ 3 by norm_num,          Real.logb_mul (by positivity) (by positivity), ← Real.rpow_natCast,          Real.logb_rpow zero_lt_two one_lt_two.ne', ← add_assoc]        norm_num  · exact (zero_lt_one.trans_le (Nat.one_le_ceil_iff.mpr (zero_lt_two.trans_le this))).ne'