Theorem: Super.grow_start
Proof 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]
Proof 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