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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
⊢ Postcritical ⋯ c ↑c
Tactic:
set s := superF d
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ Postcritical s c ↑c

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ Postcritical s c ↑c
Tactic:
simp only [Postcritical, multibrot_p, ← f_0 d, s.potential_eqn]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ s.potential c 0 ^ d < ⋯.potential c 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∉ multibrot d
s : Super (f d) d ∞ := superF d
⊢ s.potential c 0 ^ d < ⋯.potential c 0
Tactic:
simp only [multibrot_basin, not_not] at m
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : (c, 0) ∈ ⋯.basin
⊢ s.potential c 0 ^ d < ⋯.potential c 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
m : (c, 0) ∈ ⋯.basin
⊢ s.potential c 0 ^ d < ⋯.potential c 0
Tactic:
exact pow_lt_self_of_lt_one ((s.potential_pos c).mpr inf_ne_zero.symm)
  (s.potential_lt_one m) (d_gt_one d)
State after:
no goals