Theorem: Super.grow_start (Ray/Dynamics/Grow.lean)

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
s : Super f d a
c : ℂ
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have ba := s.bottcherNear_holomorphic _ (s.mem_near c)
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have nc := s.bottcherNear_mfderiv_ne_zero c
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rcases complex_inverse_fun ba nc with ⟨r, ra, rb, br⟩
State after:
case intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, s.bottcherNear c a)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNear c a), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, s.bottcherNear c a)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNear c a), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rw [s.bottcherNear_a] at ra br
State after:
case intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have rm : ∀ᶠ x : ℂ × ℂ in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near := by
  refine (continuousAt_fst.prod ra.continuousAt).eventually_mem (s.isOpen_near.mem_nhds ?_)
  have r0 := rb.self_of_nhds; simp only [s.bottcherNear_a] at r0
  simp only [uncurry, r0]; exact s.mem_near c
State after:
case intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rcases eventually_nhds_iff.mp (ra.eventually.and (br.and rm)) with ⟨t, h, o, m⟩
State after:
case intro.intro.intro.intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
h : ∀ x ∈ t, HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
o : IsOpen t
m : (c, 0) ∈ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.intro.intro.intro.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 : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
h : ∀ x ∈ t, HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
o : IsOpen t
m : (c, 0) ∈ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rcases Metric.isOpen_iff.mp o _ m with ⟨p, pp, sub⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.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 : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
h : ∀ x ∈ t, HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.intro.intro.intro.intro.intro.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 : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
h : ∀ x ∈ t, HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
replace h := fun (x : ℂ × ℂ) m ↦ h x (sub m)
State after:
case intro.intro.intro.intro.intro.intro.intro.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 : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.intro.intro.intro.intro.intro.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 : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have nb : ball (c, (0 : ℂ)) p ∈ 𝓝ˢ ({c} ×ˢ closedBall (0 : ℂ) (p / 2)) := by
  rw [isOpen_ball.mem_nhdsSet, ← ball_prod_same]; apply prod_mono
  rw [singleton_subset_iff]; exact mem_ball_self pp
  apply Metric.closedBall_subset_ball; exact half_lt_self pp
State after:
case intro.intro.intro.intro.intro.intro.intro.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 : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r

State before:
case intro.intro.intro.intro.intro.intro.intro.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 : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
use p / 2, r, half_pos pp
State after:
case right
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ Grow s c (p / 2) 0 r

State before:
case right
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ Grow s c (p / 2) 0 r
Tactic:
exact
  { nonneg := (half_pos pp).le
    zero := by convert rb.self_of_nhds; simp only [s.bottcherNear_a]
    start := Filter.eventually_iff_exists_mem.mpr ⟨_, ball_mem_nhds _ pp, fun _ m ↦ (h _ m).2.1⟩
    eqn :=
      Filter.eventually_iff_exists_mem.mpr
        ⟨_, nb, fun _ m ↦
          { holo := (h _ m).1
            near := (h _ m).2.2
            eqn := by simp only [Function.iterate_zero_apply, pow_zero, pow_one, (h _ m).2.1] }⟩ }
State after:
no goals

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
Tactic:
refine (continuousAt_fst.prod ra.continuousAt).eventually_mem (s.isOpen_near.mem_nhds ?_)
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Tactic:
have r0 := rb.self_of_nhds
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r (c, a).1 (s.bottcherNear (c, a).1 (c, a).2) = (c, a).2
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r (c, a).1 (s.bottcherNear (c, a).1 (c, a).2) = (c, a).2
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Tactic:
simp only [s.bottcherNear_a] at r0
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Tactic:
simp only [uncurry, r0]
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ (c, a) ∈ s.near

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ (c, a) ∈ s.near
Tactic:
exact s.mem_near c
State after:
no goals

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
Tactic:
rw [isOpen_ball.mem_nhdsSet, ← ball_prod_same]
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ×ˢ closedBall 0 (p / 2) ⊆ ball c p ×ˢ ball 0 p

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ×ˢ closedBall 0 (p / 2) ⊆ ball c p ×ˢ ball 0 p
Tactic:
apply prod_mono
State after:
case hs
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ⊆ ball c p

case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p

State before:
case hs
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ⊆ ball c p

case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Tactic:
rw [singleton_subset_iff]
State after:
case hs
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ c ∈ ball c p

case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p

State before:
case hs
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ c ∈ ball c p

case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Tactic:
exact mem_ball_self pp
State after:
case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p

State before:
case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Tactic:
apply Metric.closedBall_subset_ball
State after:
case ht.h
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ p / 2 < p

State before:
case ht.h
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ p / 2 < p
Tactic:
exact half_lt_self pp
State after:
no goals

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ r c 0 = a
Tactic:
convert rb.self_of_nhds
State after:
case h.e'_2.h.e'_2
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ 0 = s.bottcherNear (c, a).1 (c, a).2

State before:
case h.e'_2.h.e'_2
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ 0 = s.bottcherNear (c, a).1 (c, a).2
Tactic:
simp only [s.bottcherNear_a]
State after:
no goals

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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m✝ : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
x✝ : ℂ × ℂ
m : x✝ ∈ ball (c, 0) p
⊢ s.bottcherNear x✝.1 ((f x✝.1)^[0] (r x✝.1 x✝.2)) = x✝.2 ^ d ^ 0
Tactic:
simp only [Function.iterate_zero_apply, pow_zero, pow_one, (h _ m).2.1]
State after:
no goals