exact log_eq_of_pos (lt_of_lt_of_le (mul_pos pos pp.pos) le_self_add)
  (Exponential.add_mul Ha Hp) (le_trans (mul_le_mul' ha' hp') le_self_add) (by
    rcases Hp.uniq (exponential_of_pow2 pp)
    calc
      a * p + b < a * p + p    := by simp [hb]
      _         = (a + 1) * p  := by simp [add_mul]
      _         ≤ 2 * (a' * p) := by simp [←mul_assoc]; exact mul_le_mul_right (lt_iff_succ_le.mp ha))
case intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a p b : M
pos : 0 < a
pp : Pow2 p
hb : b < p
a' : M
ha' : a' ≤ a
Ha : Exponential (log a) a'
ha : a < 2 * a'
p' : M
hp' : p' ≤ p
Hp : Exponential (log p) p'
hp : p < 2 * p'
⊢ log (a * p + b) = log a + log p
no goals