internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_noncritical
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
set n := s.np c (abs x)
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
⊢ mfderiv I I (s.ray c) x ≠ 0
Theorem: Super.ray_noncritical
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
have h : mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0 := by
  have e : s.bottcherNearIter n c ∘ s.ray c =ᶠ[𝓝 x] fun x ↦ x ^ d ^ n :=
    (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_iter post)
  rw [e.mfderiv_eq]; contrapose x0; simp only [not_not] at x0 ⊢
  rw [mfderiv_eq_fderiv] at x0
  have d := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
  apply_fun (fun x ↦ x 1) at x0
  rw [x0] at d
  replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
  rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d
  simp only [s.d0, false_and_iff, false_or_iff] at d; exact d.1
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h : mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Theorem: Super.ray_noncritical
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h : mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
simp only [mfderiv_comp x
    (s.bottcherNearIter_holomorphic (s.ray_near post)).along_snd.mdifferentiableAt
    (s.ray_holomorphic post).along_snd.mdifferentiableAt,
  Ne, mderiv_comp_eq_zero_iff, not_or] at h
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h :
  ¬mfderiv I I (fun y => s.bottcherNearIter (s.np c (Complex.abs x)) c y) (s.ray c x) = 0 ∧ ¬mfderiv I I (s.ray c) x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Theorem: Super.ray_noncritical
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h :
  ¬mfderiv I I (fun y => s.bottcherNearIter (s.np c (Complex.abs x)) c y) (s.ray c x) = 0 ∧ ¬mfderiv I I (s.ray c) x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
exact h.2
Proof state after:
no goals
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
⊢ mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
Tactic:
have e : s.bottcherNearIter n c ∘ s.ray c =ᶠ[𝓝 x] fun x ↦ x ^ d ^ n :=
  (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_iter post)
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
Tactic:
rw [e.mfderiv_eq]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
Tactic:
contrapose x0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : ¬mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
⊢ ¬¬x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : ¬mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
⊢ ¬¬x = 0
Tactic:
simp only [not_not] at x0 ⊢
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : mfderiv I I (fun x => x ^ d ^ n) x = 0
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : mfderiv I I (fun x => x ^ d ^ n) x = 0
⊢ x = 0
Tactic:
rw [mfderiv_eq_fderiv] at x0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : fderiv ℂ (fun x => x ^ d ^ n) x = 0
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : fderiv ℂ (fun x => x ^ d ^ n) x = 0
⊢ x = 0
Tactic:
have d := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : fderiv ℂ (fun x => x ^ d✝ ^ n) x = 0
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : fderiv ℂ (fun x => x ^ d✝ ^ n) x = 0
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 0
Tactic:
apply_fun (fun x ↦ x 1) at x0
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
rw [x0] at d
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 0
Tactic:
rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Tactic:
simp only [s.d0, false_and_iff, false_or_iff] at d
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Theorem: Super.ray_noncritical
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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Tactic:
exact d.1
Proof state after:
no goals
Theorem: Super.ray_inj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
⊢ (c, x0) ∈ s.ext → (c, x1) ∈ s.ext → s.ray c x0 = s.ray c x1 → x0 = x1
Tactic:
intro p0 p1 e
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
⊢ x0 = x1
Theorem: Super.ray_inj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
⊢ x0 = x1
Tactic:
have ax : abs x0 = abs x1 := by simp only [← s.ray_potential p0, ← s.ray_potential p1, e]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
⊢ x0 = x1
Theorem: Super.ray_inj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
⊢ x0 = x1
Tactic:
by_cases x00 : x0 = 0
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : x0 = 0
⊢ x0 = x1

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
⊢ x0 = x1
Theorem: Super.ray_inj
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
⊢ x0 = x1
Tactic:
have tc : ∀ (x : ℂ) (t), ContinuousAt (fun t : ℝ ↦ ↑t * x) t := fun x t ↦
  Complex.continuous_ofReal.continuousAt.mul continuousAt_const
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
⊢ x0 = x1
Theorem: Super.ray_inj
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
⊢ x0 = x1
Tactic:
have pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc (0 : ℝ) 1 → (c, ↑t * x) ∈ s.ext := by
  intro x t p m
  simp only [Super.ext, mem_setOf, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos m.1] at p ⊢
  exact lt_of_le_of_lt (mul_le_of_le_one_left (Complex.abs.nonneg _) m.2) p
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
⊢ x0 = x1
Theorem: Super.ray_inj
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
⊢ x0 = x1
Tactic:
set u : Set ℝ := {t : ℝ | s.ray c (t * x0) = s.ray c (t * x1)}
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
⊢ x0 = x1
Theorem: Super.ray_inj
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
⊢ x0 = x1
Tactic:
suffices h : Ioc (0 : ℝ) 1 ⊆ interior u by
  replace h := _root_.trans h interior_subset
  replace tc := (tc x0 0).prod_mk (tc x1 0); simp only [← nhds_prod_eq] at tc
  simp only [ContinuousAt, Complex.ofReal_zero, MulZeroClass.zero_mul] at tc
  have inj := tc.eventually ((s.ray_holomorphic (s.mem_ext c)).along_snd.local_inj
    (s.ray_noncritical_zero c))
  rcases Metric.eventually_nhds_iff.mp inj with ⟨r, rp, inj⟩
  simp only [Real.dist_eq, sub_zero] at inj
  set t := min 1 (r / 2)
  have t0 : 0 < t := lt_min zero_lt_one (half_pos rp)
  have t01 : t ∈ Ioc (0 : ℝ) 1 := mem_Ioc.mpr ⟨t0, min_le_left _ _⟩
  specialize @inj t (by simp only [abs_of_pos t0, min_lt_of_right_lt (half_lt_self rp)]) (h t01)
  exact mul_left_cancel₀ (Complex.ofReal_ne_zero.mpr t0.ne') inj
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
⊢ Ioc 0 1 ⊆ interior u