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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
set s := superF d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
generalize hg : fl (f d) ∞ c = g
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have ct : c⁻¹ ∈ {z : ℂ | abs z < (max 16 (abs c / 2))⁻¹} := by
  simp only [mem_setOf, map_inv₀]
  apply inv_lt_inv_of_lt; bound; refine max_lt lo (half_lt_self (lt_trans (by norm_num) lo))
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have mem : c ∉ multibrot d := multibrot_two_lt (lt_trans (by norm_num) lo)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have nz : ∀ n, (f d c)^[n] c ≠ 0 := by
  intro n; contrapose mem; simp only [not_not] at mem ⊢; exact multibrot_of_zero mem
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have iter : ∀ n, ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹) := by
  intro n; induction' n with n h
  have cp : c ≠ 0 := Complex.abs.ne_zero_iff.mp (lt_trans (by norm_num) lo).ne'
  simp only [Function.iterate_zero_apply, inv_coe cp, toComplex_coe]
  have e : (f d c)^[n] ↑c = ((g^[n] c⁻¹ : ℂ) : 𝕊)⁻¹ := by rw [← h, inv_inv]
  simp only [Function.iterate_succ_apply', e]
  generalize hz : g^[n] c⁻¹ = z
  simp only [← hg, fl, extChartAt_inf, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply,
    invEquiv_apply, RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, sub_zero,
    Function.comp, add_zero, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm,
    coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm]
  rw [coe_toComplex]
  simp only [Ne, inv_eq_inf, ← hz, ← h, inv_inv, ← Function.iterate_succ_apply' (f d c)]
  apply nz
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have b := mem
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : c ∉ multibrot d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : c ∉ multibrot d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
simp only [multibrot_basin', not_not] at b
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have attracts := (s.basin_attracts b).eventually (s.bottcher_eq_bottcherNear c)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
rcases (attracts.and (s.basin_stays b)).exists with ⟨n, eq, _⟩
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
n : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
n : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
clear attracts b
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
simp only [Super.bottcherNear, extChartAt_inf, PartialEquiv.trans_apply,
  coePartialEquiv_symm_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, RiemannSphere.inv_inf,
  toComplex_zero, sub_zero, Super.fl, hg, iter, toComplex_coe] at eq
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n := s.bottcher_eqn_iter n
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n := by
  rw [← hg]; exact bottcherNear_eqn_iter (superNearF d c) ct n
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
rw [e0, e1] at eq
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
clear e0 e1 iter
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have ae : abs (bottcher' d c) = abs (bottcherNear g d c⁻¹) := by
  apply (pow_left_inj (Complex.abs.nonneg _) (Complex.abs.nonneg _)
    (pow_ne_zero n (d_ne_zero d))).mp
  simp only [← Complex.abs.map_pow, eq]
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
rw [ae, ← hg]
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcherNear (fl (f d) ∞ c) d c⁻¹) ≤ 3 * Complex.abs c⁻¹

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcherNear (fl (f d) ∞ c) d c⁻¹) ≤ 3 * Complex.abs c⁻¹
Tactic:
exact bottcherNear_le (superNearF d c) ct
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
simp only [mem_setOf, map_inv₀]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
apply inv_lt_inv_of_lt
State after:
case hb
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ 0 < max 16 (Complex.abs c / 2)

case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c

State before:
case hb
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ 0 < max 16 (Complex.abs c / 2)

case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Tactic:
bound
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Tactic:
refine max_lt lo (half_lt_self (lt_trans (by norm_num) lo))
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ 2 < 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
⊢ ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
Tactic:
intro n
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
n : ℕ
⊢ (f d c)^[n] ↑c ≠ 0

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
n : ℕ
⊢ (f d c)^[n] ↑c ≠ 0
Tactic:
contrapose mem
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : ¬(f d c)^[n] ↑c ≠ 0
⊢ ¬c ∉ multibrot d

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : ¬(f d c)^[n] ↑c ≠ 0
⊢ ¬c ∉ multibrot d
Tactic:
simp only [not_not] at mem ⊢
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : (f d c)^[n] ↑c = 0
⊢ c ∈ multibrot d

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : (f d c)^[n] ↑c = 0
⊢ c ∈ multibrot d
Tactic:
exact multibrot_of_zero mem
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
Tactic:
intro n
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
⊢ ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
⊢ ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
Tactic:
induction' n with n h
State after:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)

State before:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
have cp : c ≠ 0 := Complex.abs.ne_zero_iff.mp (lt_trans (by norm_num) lo).ne'
State after:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
cp : c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)

State before:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
cp : c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
simp only [Function.iterate_zero_apply, inv_coe cp, toComplex_coe]
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
have e : (f d c)^[n] ↑c = ((g^[n] c⁻¹ : ℂ) : 𝕊)⁻¹ := by rw [← h, inv_inv]
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
simp only [Function.iterate_succ_apply', e]
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ (f d c (↑(g^[n] c⁻¹))⁻¹)⁻¹ = ↑(g (g^[n] c⁻¹))

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ (f d c (↑(g^[n] c⁻¹))⁻¹)⁻¹ = ↑(g (g^[n] c⁻¹))
Tactic:
generalize hz : g^[n] c⁻¹ = z
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(g z)

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(g z)
Tactic:
simp only [← hg, fl, extChartAt_inf, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply,
  invEquiv_apply, RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, sub_zero,
  Function.comp, add_zero, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm,
  coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm]
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(f d c (↑z)⁻¹)⁻¹.toComplex

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(f d c (↑z)⁻¹)⁻¹.toComplex
Tactic:
rw [coe_toComplex]
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ ≠ ∞

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ ≠ ∞
Tactic:
simp only [Ne, inv_eq_inf, ← hz, ← h, inv_inv, ← Function.iterate_succ_apply' (f d c)]
State after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ ¬(f d c)^[n.succ] ↑c = 0

State before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ ¬(f d c)^[n.succ] ↑c = 0
Tactic:
apply nz
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
Tactic:
rw [← h, inv_inv]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
Tactic:
rw [← hg]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ bottcherNear (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] c⁻¹) = bottcherNear (fl (f d) ∞ c) d c⁻¹ ^ d ^ n

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ bottcherNear (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] c⁻¹) = bottcherNear (fl (f d) ∞ c) d c⁻¹ ^ d ^ n
Tactic:
exact bottcherNear_eqn_iter (superNearF d c) ct n
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
Tactic:
apply (pow_left_inj (Complex.abs.nonneg _) (Complex.abs.nonneg _)
  (pow_ne_zero n (d_ne_zero d))).mp
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ^ d ^ n = Complex.abs (bottcherNear g d c⁻¹) ^ d ^ n

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ^ d ^ n = Complex.abs (bottcherNear g d c⁻¹) ^ d ^ n
Tactic:
simp only [← Complex.abs.map_pow, eq]
State after:
no goals