internlm/Lean-Github huggingface dataset:
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r1 c 0 = a
Tactic:
rw [← 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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r0 c 0 = a
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r0 c 0 = a
Tactic:
exact g.zero
Proof state after:
no goals
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
refine g.start.mp ((e.filter_mono (nhds_le_nhdsSet (mem_domain c g.nonneg))).mp ?_)
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    uncurry r0 x = uncurry r1 x → s.bottcherNear x.1 (r0 x.1 x.2) = x.2 → s.bottcherNear x.1 (r1 x.1 x.2) = x.2
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    uncurry r0 x = uncurry r1 x → s.bottcherNear x.1 (r0 x.1 x.2) = x.2 → s.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
refine eventually_of_forall fun x e s ↦ ?_
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : uncurry r0 x = uncurry r1 x
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : uncurry r0 x = uncurry r1 x
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
simp only [uncurry] at 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 : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
rw [← 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 : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
Tactic:
exact s
Proof state after:
no goals
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r1 x
Tactic:
have eqn := g.eqn
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
eqn : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r0 x
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r1 x
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
eqn : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r0 x
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r1 x
Tactic:
simp only [Filter.EventuallyEq, eventually_nhdsSet_iff_forall] at eqn 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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
⊢ ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
⊢ ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x
Tactic:
intro x m
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x
Tactic:
refine (eqn x m).mp ((e x m).eventually_nhds.mp (eventually_of_forall fun y e eqn ↦ ?_))
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, uncurry r0 x = uncurry r1 x
eqn : Eqn s n r0 y
⊢ Eqn s n r1 y
Theorem: Grow.congr
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, uncurry r0 x = uncurry r1 x
eqn : Eqn s n r0 y
⊢ Eqn s n r1 y
Tactic:
exact eqn.congr e
Proof state after:
no goals
Theorem: Eqn.potential
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
⊢ s.potential x.1 (r x.1 x.2) = Complex.abs x.2
Tactic:
simp only [s.potential_eq e.near, Super.potential', e.eqn, Complex.abs.map_pow, ← Nat.cast_pow,
  Real.pow_rpow_inv_natCast (Complex.abs.nonneg _) (pow_ne_zero _ s.d0)]
Proof state after:
no goals
Theorem: eqn_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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r y
x0 : x.2 ≠ 0
⊢ mfderiv I I (s.bottcherNearIter n x.1) (r x.1 x.2) ≠ 0
Tactic:
rcases x with ⟨c, x⟩
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : (c, x).2 ≠ 0
⊢ mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : (c, x).2 ≠ 0
⊢ mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
Tactic:
contrapose x0
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : ¬mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
⊢ ¬(c, x).2 ≠ 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : ¬mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
⊢ ¬(c, x).2 ≠ 0
Tactic:
simp only [not_not] at x0 ⊢
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (s.bottcherNearIter n c) (r c x) = 0
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (s.bottcherNearIter n c) (r c x) = 0
⊢ x = 0
Tactic:
replace x0 : mfderiv I I (fun y ↦ s.bottcherNearIter n c (r c y)) x = 0 := by
  rw [←Function.comp_def,
    mfderiv_comp x (s.bottcherNearIter_holomorphic e.self_of_nhds.near).along_snd.mdifferentiableAt
      e.self_of_nhds.holo.along_snd.mdifferentiableAt,
    x0, ContinuousLinearMap.zero_comp]
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
⊢ x = 0
Tactic:
have loc : (fun y ↦ s.bottcherNearIter n c (r c y)) =ᶠ[𝓝 x] fun y ↦ y ^ d ^ n :=
  ((continuousAt_const.prod continuousAt_id).eventually e).mp
    (eventually_of_forall fun _ e ↦ e.eqn)
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0
Tactic:
rw [mfderiv_eq_fderiv, loc.fderiv_eq] at x0
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0
Tactic:
have d := (differentiableAt_pow (𝕜 := ℂ) (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d✝ ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d✝ ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
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:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
rw [x0] at d
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ 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:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ 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:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Theorem: eqn_noncritical
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ 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: eqn_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✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (s.bottcherNearIter n c) (r c x) = 0
⊢ mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
Tactic:
rw [←Function.comp_def,
  mfderiv_comp x (s.bottcherNearIter_holomorphic e.self_of_nhds.near).along_snd.mdifferentiableAt
    e.self_of_nhds.holo.along_snd.mdifferentiableAt,
  x0, ContinuousLinearMap.zero_comp]
Proof state after:
no goals
Theorem: Grow.p1
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : Grow s c p n r
⊢ p < 1
Tactic:
by_contra p1
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : Grow s c p n r
p1 : ¬p < 1
⊢ False