Theorem: pass_through (Ray/Dynamics/Multibrot/PotentialLower.lean)

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
m : (c, ↑z) ∈ ⋯.basin
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
set s := superF 2
State after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : (c, ↑z) ∈ s.basin
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
simp only [s.basin_iff_attracts, Attracts, RiemannSphere.tendsto_inf_iff_tendsto_atInf, f_f'_iter,
  tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs] at m
State after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
rcases Filter.tendsto_atTop_atTop.mp m 5 with ⟨n,h⟩
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
generalize hp : (fun n ↦ 4 < abs ((f' 2 c)^[n] z)) = p
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
replace h : p n := by rw [←hp]; linarith [h n (by linarith)]
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
generalize hk : Nat.find (p := p) ⟨_,h⟩ = k
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
have k4 : p k := by rw [←hk]; exact Nat.find_spec (p := p) ⟨_,h⟩
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
have k0 : k ≠ 0 := by
  contrapose k4
  simp only [not_not] at k4
  simp only [k4, ←hp, not_lt, Function.iterate_zero_apply, z4]
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
have k1 : 1 ≤ k := Nat.pos_iff_ne_zero.mpr k0
State after:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20

State before:
case intro
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ∃ n, Complex.abs ((f' 2 c)^[n + 1] z) ∈ Ioc 4 20
Tactic:
use k-1
State after:
case h
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ Complex.abs ((f' 2 c)^[k - 1 + 1] z) ∈ Ioc 4 20

State before:
case h
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ Complex.abs ((f' 2 c)^[k - 1 + 1] z) ∈ Ioc 4 20
Tactic:
have lt : ¬p (k-1) := by apply Nat.find_min; rw [hk]; omega
State after:
case h
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
lt : ¬p (k - 1)
⊢ Complex.abs ((f' 2 c)^[k - 1 + 1] z) ∈ Ioc 4 20

State before:
case h
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
lt : ¬p (k - 1)
⊢ Complex.abs ((f' 2 c)^[k - 1 + 1] z) ∈ Ioc 4 20
Tactic:
simp only [Nat.sub_add_cancel k1, ←hp, not_lt] at k4 k1 lt ⊢
State after:
case h
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
⊢ Complex.abs ((f' 2 c)^[k] z) ∈ Ioc 4 20

State before:
case h
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
⊢ Complex.abs ((f' 2 c)^[k] z) ∈ Ioc 4 20
Tactic:
use k4
State after:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20

State before:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20
Tactic:
have fs := iter_small 2 c ((f' 2 c)^[k-1] z)
State after:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs (f' 2 c ((f' 2 c)^[k - 1] z)) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20

State before:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs (f' 2 c ((f' 2 c)^[k - 1] z)) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20
Tactic:
simp only [←Function.iterate_succ_apply', Nat.succ_eq_add_one, Nat.sub_add_cancel k1] at fs
State after:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs ((f' 2 c)^[k] z) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20

State before:
case right
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs ((f' 2 c)^[k] z) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ Complex.abs ((f' 2 c)^[k] z) ≤ 20
Tactic:
exact le_trans fs (le_trans (add_le_add (pow_le_pow_left (Complex.abs.nonneg _) lt 2) c4)
  (by norm_num))
State after:
no goals

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ p n
Tactic:
rw [←hp]
State after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) n

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) n
Tactic:
linarith [h n (by linarith)]
State after:
no goals

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
h : ∀ (a : ℕ), n ≤ a → 5 ≤ Complex.abs ((f' 2 c)^[a] z)
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
⊢ n ≤ n
Tactic:
linarith
State after:
no goals

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ p k
Tactic:
rw [←hk]
State after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ p (Nat.find ⋯)

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
⊢ p (Nat.find ⋯)
Tactic:
exact Nat.find_spec (p := p) ⟨_,h⟩
State after:
no goals

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
⊢ k ≠ 0
Tactic:
contrapose k4
State after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : ¬k ≠ 0
⊢ ¬p k

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : ¬k ≠ 0
⊢ ¬p k
Tactic:
simp only [not_not] at k4
State after:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : k = 0
⊢ ¬p k

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : k = 0
⊢ ¬p k
Tactic:
simp only [k4, ←hp, not_lt, Function.iterate_zero_apply, z4]
State after:
no goals

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ¬p (k - 1)
Tactic:
apply Nat.find_min
State after:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < Nat.find ?H

case H
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ∃ n, p n

State before:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < Nat.find ?H

case H
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ ∃ n, p n
Tactic:
rw [hk]
State after:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < k

State before:
case a
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k4 : p k
k0 : k ≠ 0
k1 : 1 ≤ k
⊢ k - 1 < k
Tactic:
omega
State after:
no goals

State before:
c z : ℂ
c4 : Complex.abs c ≤ 4
z4 : Complex.abs z ≤ 4
s : Super (f 2) 2 OnePoint.infty := superF 2
m : Filter.Tendsto (fun x => Complex.abs ((f' 2 c)^[x] z)) Filter.atTop Filter.atTop
n : ℕ
p : ℕ → Prop
hp : (fun n => 4 < Complex.abs ((f' 2 c)^[n] z)) = p
h : p n
k : ℕ
hk : Nat.find ⋯ = k
k0 : k ≠ 0
k1 : 1 ≤ k
k4 : 4 < Complex.abs ((f' 2 c)^[k] z)
lt : Complex.abs ((f' 2 c)^[k - 1] z) ≤ 4
fs : Complex.abs ((f' 2 c)^[k] z) ≤ Complex.abs ((f' 2 c)^[k - 1] z) ^ 2 + Complex.abs c
⊢ 4 ^ 2 + 4 ≤ 20
Tactic:
norm_num
State after:
no goals