Theorem: gl_f (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ g (fl (f d) ∞ c) d z = gl d c z
Tactic:
simp only [fl_f, gl, g]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Tactic:
by_cases z0 : z = 0
State after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

State before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Tactic:
simp only [if_pos, z0, zero_pow (d_ne_zero _), MulZeroClass.mul_zero, add_zero, inv_one]
State after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

State before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Tactic:
rw [if_neg z0, div_eq_mul_inv _ (_ + _), mul_comm, mul_div_assoc, div_self (pow_ne_zero _ z0),
  mul_one]
State after:
no goals