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

State before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
have d0 : 1 + b/a ≠ 0 := by field_simp [a0, ab0]
State after:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log

State before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
have a0' : abs a ≠ 0 := Complex.abs.ne_zero a0
State after:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log

State before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log
Tactic:
have d0' : abs (1 + b / a) ≠ 0 := Complex.abs.ne_zero d0
State after:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
d0 : 1 + b / a ≠ 0
a0' : Complex.abs a ≠ 0
d0' : Complex.abs (1 + b / a) ≠ 0
⊢ (Complex.abs (a + b)).log = (Complex.abs a).log + (Complex.abs (1 + b / a)).log

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

State before:
a b : ℂ
a0 : a ≠ 0
ab0 : a + b ≠ 0
⊢ 1 + b / a ≠ 0
Tactic:
field_simp [a0, ab0]
State after:
no goals