Theorem: Grow.open (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
g : Grow s c p n r
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
have e := g.eqn
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
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
simp only [isCompact_singleton.nhdsSet_prod_eq (isCompact_closedBall _ _)] at e
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
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases Filter.mem_prod_iff.mp e with ⟨a', an, b', bn, sub⟩
State after:
case 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : a' ×ˢ b' ⊆ {x | (fun x => Eqn s n r x) x}
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r

State before:
case 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : a' ×ˢ b' ⊆ {x | (fun x => Eqn s n r x) x}
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
simp only [subset_setOf] at sub
State after:
case 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r

State before:
case 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases eventually_nhds_iff.mp (nhdsSet_singleton.subst an) with ⟨a, aa, ao, am⟩
State after:
case 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r

State before:
case 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases eventually_nhdsSet_iff_exists.mp bn with ⟨b, bo, bp, bb⟩
State after:
case intro.intro.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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r

State before:
case intro.intro.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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases domain_open' bp bo with ⟨q, pq, qb⟩
State after:
case intro.intro.intro.intro.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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r

State before:
case intro.intro.intro.intro.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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
use q, pq
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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q n r
Tactic:
apply m.mp
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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, (x, r x 0) ∈ s.near → Grow s x q n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, (x, r x 0) ∈ s.near → Grow s x q n r
Tactic:
apply ((continuousAt_id.prod continuousAt_const).eventually g.start.eventually_nhds).mp
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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n r
Tactic:
refine eventually_nhds_iff.mpr ⟨a, ?_, ao, am⟩
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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a, (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a, (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n r
Tactic:
intro c' am' start m
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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ Grow s c' q n 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
Tactic:
refine (continuousAt_id.prod ?_).eventually_mem (s.isOpen_near.mem_nhds ?_)
State after:
case refine_1
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
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ContinuousAt (fun c' => r c' 0) c

case refine_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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ (id c, r c 0) ∈ s.near

State before:
case refine_1
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
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ContinuousAt (fun c' => r c' 0) c
Tactic:
exact (g.eqn.filter_mono (nhds_le_nhdsSet (mem_domain c
  g.nonneg))).self_of_nhds.holo.along_fst.continuousAt
State after:
no goals

State before:
case refine_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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ (id c, r c 0) ∈ s.near
Tactic:
simp only [id, g.zero, 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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ r c' 0 = a✝
Tactic:
have e := start.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
g : Grow s c p n r
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : s.bottcherNear (id c', 0).1 (r (id c', 0).1 (id c', 0).2) = (id c', 0).2
⊢ r c' 0 = a✝

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
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : s.bottcherNear (id c', 0).1 (r (id c', 0).1 (id c', 0).2) = (id c', 0).2
⊢ r c' 0 = a✝
Tactic:
simp only [id, s.bottcherNear_eq_zero m] at e
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
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : r c' 0 = a✝
⊢ r c' 0 = a✝

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
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : r c' 0 = a✝
⊢ r c' 0 = a✝
Tactic:
exact e
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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c'} ×ˢ closedBall 0 q), Eqn s n r x
Tactic:
refine eventually_nhdsSet_iff_exists.mpr ⟨a ×ˢ b, ao.prod bo, ?_, ?_⟩
State after:
case refine_1
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
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ {c'} ×ˢ closedBall 0 q ⊆ a ×ˢ b

case refine_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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a ×ˢ b, Eqn s n r x

State before:
case refine_1
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
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ {c'} ×ˢ closedBall 0 q ⊆ a ×ˢ b
Tactic:
exact prod_mono (singleton_subset_iff.mpr am') qb
State after:
no goals

State before:
case refine_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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a ×ˢ b, Eqn s n r x
Tactic:
intro x ⟨cm, xm⟩
State after:
case refine_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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
x : ℂ × ℂ
cm : x.1 ∈ a
xm : x.2 ∈ b
⊢ Eqn s n r x

State before:
case refine_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
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
x : ℂ × ℂ
cm : x.1 ∈ a
xm : x.2 ∈ b
⊢ Eqn s n r x
Tactic:
exact sub x ⟨aa _ cm, bb _ xm⟩
State after:
no goals