Theorem: log_add (Ray/Misc/Bounds.lean)

State before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ (a + b).log = a.log + (1 + b / a).log
Tactic:
have d0 : 0 < 1 + b/a := by field_simp [a0.ne']; bound
State after:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
d0 : 0 < 1 + b / a
⊢ (a + b).log = a.log + (1 + b / a).log

State before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
d0 : 0 < 1 + b / a
⊢ (a + b).log = a.log + (1 + b / a).log
Tactic:
rw [←Real.log_mul a0.ne' d0.ne', left_distrib, mul_one, mul_div_cancel₀ _ a0.ne']
State after:
no goals

State before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ 0 < 1 + b / a
Tactic:
field_simp [a0.ne']
State after:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ 0 < a

State before:
a b : ℝ
a0 : 0 < a
ab0 : 0 < a + b
⊢ 0 < a
Tactic:
bound
State after:
no goals