internlm/Lean-Github huggingface dataset:
Theorem: Super.potential_minima_only_a
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}} →
      Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z
Tactic:
refine eventually_of_forall fun w m lt ↦ ?_
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : w ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}}
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Theorem: Super.potential_minima_only_a
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : w ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}}
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Tactic:
rw [mem_setOf, mem_setOf] at m
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : ((c, w).1, (f✝ (c, w).1)^[s.nz c z] (c, w).2) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Theorem: Super.potential_minima_only_a
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : ((c, w).1, (f✝ (c, w).1)^[s.nz c z] (c, w).2) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Tactic:
simp only at m
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Theorem: Super.potential_minima_only_a
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ s.potential c w < s.potential c z
Tactic:
simp only [s.potential_eq m, s.potential_eq near, Super.potential']
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] w)) ^ (↑d ^ s.nz c z)⁻¹ <
    Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] z)) ^ (↑d ^ s.nz c z)⁻¹
Theorem: Super.potential_minima_only_a
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m✝ : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
w : S
m : (c, (f✝ c)^[s.nz c z] w) ∈ s.near
lt : Complex.abs (f w) < Complex.abs (f z)
⊢ Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] w)) ^ (↑d ^ s.nz c z)⁻¹ <
    Complex.abs (s.bottcherNear c ((f✝ c)^[s.nz c z] z)) ^ (↑d ^ s.nz c z)⁻¹
Tactic:
exact Real.rpow_lt_rpow (Complex.abs.nonneg _) lt
  (inv_pos.mpr (pow_pos (Nat.cast_pos.mpr s.dp) _))
Proof state after:
no goals
Theorem: Super.potential_minima_only_a
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ ∃ᶠ (x : ℂ) in 𝓝 (f z), Complex.abs x < Complex.abs (f z)
Tactic:
apply frequently_smaller
Proof state after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ f z ≠ 0
Theorem: Super.potential_minima_only_a
Proof state before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ f z ≠ 0
Tactic:
contrapose m
Proof state after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : ¬f z ≠ 0
⊢ ¬¬z = a
Theorem: Super.potential_minima_only_a
Proof state before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : ¬f z ≠ 0
⊢ ¬¬z = a
Tactic:
simp only [not_not] at m ⊢
Proof state after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : f z = 0
⊢ z = a
Theorem: Super.potential_minima_only_a
Proof state before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : f z = 0
⊢ z = a
Tactic:
replace m := (s.bottcherNear_eq_zero near).mp m
Proof state after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : (f✝ c)^[s.nz c z] z = a
⊢ z = a
Theorem: Super.potential_minima_only_a
Proof state before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : (f✝ c)^[s.nz c z] z = a
⊢ z = a
Tactic:
rw [s.preimage_eq] at m
Proof state after:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : z = a
⊢ z = a
Theorem: Super.potential_minima_only_a
Proof state before:
case z0
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
p : Postcritical s c z
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
m : z = a
⊢ z = a
Tactic:
exact m
Proof state after:
no goals
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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⟩
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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)]
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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⟩
Proof 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
Theorem: pass_through
Proof 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]
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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 ⊢
Proof 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
Theorem: pass_through
Proof 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
Proof 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
Theorem: pass_through
Proof 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)
Proof 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