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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fl (f d) ∞ = fun c z => z ^ d / (1 + c * z ^ d)
Tactic:
funext c z
State after:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = z ^ d / (1 + c * z ^ d)

State before:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [fl, RiemannSphere.extChartAt_inf, Function.comp, invEquiv_apply,
  PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, PartialEquiv.coe_trans_symm,
  coePartialEquiv_symm_apply, PartialEquiv.symm_symm, coePartialEquiv_apply,
  Equiv.toPartialEquiv_symm_apply, invEquiv_symm, RiemannSphere.inv_inf, toComplex_zero,
  add_zero, sub_zero]
State after:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

State before:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
by_cases z0 : z = 0
State after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [f, f', inv_coe z0, lift_coe', inv_pow]
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
have zd := pow_ne_zero d z0
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
by_cases h : (z ^ d)⁻¹ + c = 0
State after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
rw [inv_coe h, toComplex_coe, eq_div_iff, inv_mul_eq_iff_eq_mul₀ h, right_distrib,
  inv_mul_cancel zd]
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ 1 + c * z ^ d ≠ 0

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ 1 + c * z ^ d ≠ 0
Tactic:
contrapose h
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ ¬¬(z ^ d)⁻¹ + c = 0

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ ¬¬(z ^ d)⁻¹ + c = 0
Tactic:
rw [not_not]
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ (z ^ d)⁻¹ + c = 0

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ (z ^ d)⁻¹ + c = 0
Tactic:
rw [not_not, add_comm, add_eq_zero_iff_eq_neg, ← eq_div_iff zd, neg_div, ←
  inv_eq_one_div, ← add_eq_zero_iff_eq_neg, add_comm] at h
State after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (z ^ d)⁻¹ + c = 0

State before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (z ^ d)⁻¹ + c = 0
Tactic:
exact h
State after:
no goals

State before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [z0, coe_zero, inv_zero', f, lift_inf', RiemannSphere.inv_inf, toComplex_zero,
  zero_pow (d_ne_zero _), zero_div]
State after:
no goals

State before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [h, coe_zero, inv_zero', toComplex_inf]
State after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ 0 = z ^ d / (1 + c * z ^ d)

State before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ 0 = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [← add_eq_zero_iff_neg_eq.mp h, neg_mul, inv_mul_cancel zd, ← sub_eq_add_neg,
  sub_self, div_zero]
State after:
no goals