Theorem: GrowOpen.grow (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 : GrowOpen s c p r
inst✝ : OnePreimage s
⊢ ∃ r', Grow s c p (s.np c p) r'
Tactic:
set n := s.np c p
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∃ r', 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
⊢ ∃ r', Grow s c p n r'
Tactic:
have m0 : (c, (0 : ℂ)) ∈ ({c} ×ˢ ball 0 p : Set (ℂ × ℂ)) := by
  simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff, mem_ball_self g.pos]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ ∃ r', 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ ∃ r', Grow s c p n r'
Tactic:
use curry b.u
State after:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ Grow s c p n (curry b.u)

State before:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ Grow s c p n (curry b.u)
Tactic:
exact
  { nonneg := g.pos.le
    zero := by rw [curry, b.uf.self_of_nhdsSet m0, uncurry, g.zero]
    start := by
      refine g.start.mp ((b.uf.filter_mono (nhds_le_nhdsSet m0)).mp (eventually_of_forall ?_))
      intro x e b; simp only [curry, uncurry, Prod.mk.eta] at e ⊢; rw [e]; exact b
    eqn := by
      have fp := b.up
      simp only [closure_prod_eq, closure_singleton, closure_ball _ g.pos.ne'] at fp
      exact fp.mp (eventually_of_forall fun x e ↦ e.eqn.self_of_nhds) }
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ IsCompact (closure ({c} ×ˢ ball 0 p))
Tactic:
simp only [closure_prod_eq, closure_ball _ g.pos.ne', closure_singleton]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ IsCompact ({c} ×ˢ closedBall 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ IsCompact ({c} ×ˢ closedBall 0 p)
Tactic:
exact isCompact_singleton.prod (isCompact_closedBall _ _)
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∀ {f_1 g : ℂ × ℂ → S} {x : ℂ × ℂ}, Eqns s n r (curry f_1) x → (𝓝 x).EventuallyEq f_1 g → Eqns s n r (curry g) x
Tactic:
intro r0 r1 x e0 r01
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
x : ℂ × ℂ
e0 : Eqns s n r (curry r0) x
r01 : (𝓝 x).EventuallyEq r0 r1
⊢ Eqns s n r (curry r1) x

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
x : ℂ × ℂ
e0 : Eqns s n r (curry r0) x
r01 : (𝓝 x).EventuallyEq r0 r1
⊢ Eqns s n r (curry r1) x
Tactic:
exact e0.congr (by simp only [Function.uncurry_curry, r01])
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
x : ℂ × ℂ
e0 : Eqns s n r (curry r0) x
r01 : (𝓝 x).EventuallyEq r0 r1
⊢ (𝓝 x).EventuallyEq (uncurry (curry r0)) (uncurry (curry r1))
Tactic:
simp only [Function.uncurry_curry, r01]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ ball 0 p), Eqns s n r (curry (uncurry r)) x
Tactic:
simp only [Filter.eventually_iff]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ {x | Eqns s n r (curry (uncurry r)) x} ∈ 𝓝ˢ ({c} ×ˢ 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ {x | Eqns s n r (curry (uncurry r)) x} ∈ 𝓝ˢ ({c} ×ˢ ball 0 p)
Tactic:
rw [mem_nhdsSet_iff_forall]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∀ x ∈ {c} ×ˢ ball 0 p, {x | Eqns s n r (curry (uncurry r)) x} ∈ 𝓝 x

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∀ x ∈ {c} ×ˢ ball 0 p, {x | Eqns s n r (curry (uncurry r)) x} ∈ 𝓝 x
Tactic:
intro x m
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
x : ℂ × ℂ
m : x ∈ {c} ×ˢ ball 0 p
⊢ {x | Eqns s n r (curry (uncurry r)) x} ∈ 𝓝 x

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
x : ℂ × ℂ
m : x ∈ {c} ×ˢ ball 0 p
⊢ {x | Eqns s n r (curry (uncurry r)) x} ∈ 𝓝 x
Tactic:
exact (g.eqn.filter_mono (nhds_le_nhdsSet m)).eventually_nhds.mp
  (eventually_of_forall fun y e ↦
  { eqn := e
    start := by
      simp only [Function.curry_uncurry, Filter.EventuallyEq.refl, imp_true_iff] })
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
x : ℂ × ℂ
m : x ∈ {c} ×ˢ ball 0 p
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ y.2 = 0 → (𝓝 y).EventuallyEq (uncurry (curry (uncurry r))) (uncurry r)
Tactic:
simp only [Function.curry_uncurry, Filter.EventuallyEq.refl, imp_true_iff]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∀ {x : ℂ × ℂ},
    x ∈ closure ({c} ×ˢ ball 0 p) →
      ∃ g,
        (∀ᶠ (z : ℂ × ℂ) in 𝓝 x, Eqns s n r (curry g) z) ∧ ∃ᶠ (z : ℂ × ℂ) in 𝓝 x, z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
intro ⟨c', x⟩ m
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : (c', x) ∈ closure ({c} ×ˢ ball 0 p)
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : (c', x) ∈ closure ({c} ×ˢ ball 0 p)
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
simp only [closure_prod_eq, closure_ball _ g.pos.ne', closure_singleton, mem_prod_eq,
  mem_singleton_iff, mem_closedBall, Complex.dist_eq, sub_zero] at m
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
have ct : Tendsto (fun x ↦ (c, x)) (𝓝 x) (𝓝 (c, x)) :=
  continuousAt_const.prod continuousAt_id
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
by_cases x0 : x ≠ 0
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

case neg
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : ¬x ≠ 0
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

State before:
case pos
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
rw [m.1]
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

State before:
case pos
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
rcases g.point m.2 with ⟨r', e, rr⟩
State after:
case pos.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z

State before:
case pos.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
use uncurry r'
State after:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry (uncurry r')) z) ∧
    ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r' z = uncurry r z

State before:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry (uncurry r')) z) ∧
    ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r' z = uncurry r z
Tactic:
constructor
State after:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry (uncurry r')) z

case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r' z = uncurry r z

State before:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry (uncurry r')) z
Tactic:
have t : ContinuousAt (fun y : ℂ × ℂ ↦ y.2) (c, x) := continuousAt_snd
State after:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
t : ContinuousAt (fun y => y.2) (c, x)
⊢ ∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry (uncurry r')) z

State before:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
t : ContinuousAt (fun y => y.2) (c, x)
⊢ ∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), Eqns s n r (curry (uncurry r')) z
Tactic:
refine e.eventually_nhds.mp ((t.eventually_ne x0).mp (eventually_of_forall ?_))
State after:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
t : ContinuousAt (fun y => y.2) (c, x)
⊢ ∀ (x : ℂ × ℂ), x.2 ≠ 0 → (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s (s.np c p) r' x) → Eqns s n r (curry (uncurry r')) x

State before:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
t : ContinuousAt (fun y => y.2) (c, x)
⊢ ∀ (x : ℂ × ℂ), x.2 ≠ 0 → (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s (s.np c p) r' x) → Eqns s n r (curry (uncurry r')) x
Tactic:
intro y y0 e
State after:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
t : ContinuousAt (fun y => y.2) (c, x)
y : ℂ × ℂ
y0 : y.2 ≠ 0
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r' x
⊢ Eqns s n r (curry (uncurry r')) y

State before:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
t : ContinuousAt (fun y => y.2) (c, x)
y : ℂ × ℂ
y0 : y.2 ≠ 0
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r' x
⊢ Eqns s n r (curry (uncurry r')) y
Tactic:
exact
  { eqn := e
    start := fun h ↦ (y0 h).elim }
State after:
no goals

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r' z = uncurry r z
Tactic:
refine ct.frequently (rr.mp (eventually_of_forall ?_))
State after:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∀ (x : ℂ), x ∈ ball 0 p ∧ r' c x = r c x → (c, x) ∈ {c} ×ˢ ball 0 p ∧ uncurry r' (c, x) = uncurry r (c, x)

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x ≠ 0
r' : ℂ → ℂ → S
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
⊢ ∀ (x : ℂ), x ∈ ball 0 p ∧ r' c x = r c x → (c, x) ∈ {c} ×ˢ ball 0 p ∧ uncurry r' (c, x) = uncurry r (c, x)
Tactic:
intro x ⟨m, e⟩
State after:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x✝ : ℂ
m✝ : c' = c ∧ Complex.abs x✝ ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x✝) (𝓝 (c, x✝))
x0 : x✝ ≠ 0
r' : ℂ → ℂ → S
e✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x✝), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x✝, y ∈ ball 0 p ∧ r' c y = r c y
x : ℂ
m : x ∈ ball 0 p
e : r' c x = r c x
⊢ (c, x) ∈ {c} ×ˢ ball 0 p ∧ uncurry r' (c, x) = uncurry r (c, x)

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x✝ : ℂ
m✝ : c' = c ∧ Complex.abs x✝ ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x✝) (𝓝 (c, x✝))
x0 : x✝ ≠ 0
r' : ℂ → ℂ → S
e✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x✝), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x✝, y ∈ ball 0 p ∧ r' c y = r c y
x : ℂ
m : x ∈ ball 0 p
e : r' c x = r c x
⊢ (c, x) ∈ {c} ×ˢ ball 0 p ∧ uncurry r' (c, x) = uncurry r (c, x)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff]
State after:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x✝ : ℂ
m✝ : c' = c ∧ Complex.abs x✝ ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x✝) (𝓝 (c, x✝))
x0 : x✝ ≠ 0
r' : ℂ → ℂ → S
e✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x✝), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x✝, y ∈ ball 0 p ∧ r' c y = r c y
x : ℂ
m : x ∈ ball 0 p
e : r' c x = r c x
⊢ x ∈ ball 0 p ∧ uncurry r' (c, x) = uncurry r (c, x)

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x✝ : ℂ
m✝ : c' = c ∧ Complex.abs x✝ ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x✝) (𝓝 (c, x✝))
x0 : x✝ ≠ 0
r' : ℂ → ℂ → S
e✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x✝), Eqn s (s.np c p) r' y
rr : ∃ᶠ (y : ℂ) in 𝓝 x✝, y ∈ ball 0 p ∧ r' c y = r c y
x : ℂ
m : x ∈ ball 0 p
e : r' c x = r c x
⊢ x ∈ ball 0 p ∧ uncurry r' (c, x) = uncurry r (c, x)
Tactic:
use m, e
State after:
no goals

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : ¬x ≠ 0
⊢ ∃ g,
    (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry g) z) ∧
      ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ g z = uncurry r z
Tactic:
use uncurry r
State after:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : ¬x ≠ 0
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry (uncurry r)) z) ∧
    ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r z = uncurry r z

State before:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : ¬x ≠ 0
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry (uncurry r)) z) ∧
    ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r z = uncurry r z
Tactic:
simp only [not_not] at x0
State after:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x = 0
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry (uncurry r)) z) ∧
    ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r z = uncurry r z

State before:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
ct : Tendsto (fun x => (c, x)) (𝓝 x) (𝓝 (c, x))
x0 : x = 0
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), Eqns s n r (curry (uncurry r)) z) ∧
    ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c', x), z ∈ {c} ×ˢ ball 0 p ∧ uncurry r z = uncurry r z
Tactic:
simp only [m.1, x0, eq_self_iff_true, and_true_iff] at ct ⊢
State after:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), Eqns s n r (curry (uncurry r)) z) ∧ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), z ∈ {c} ×ˢ ball 0 p

State before:
case 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
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ (∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), Eqns s n r (curry (uncurry r)) z) ∧ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), z ∈ {c} ×ˢ ball 0 p
Tactic:
constructor
State after:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), Eqns s n r (curry (uncurry r)) z

case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), z ∈ {c} ×ˢ ball 0 p

State before:
case h.left
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∀ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), Eqns s n r (curry (uncurry r)) z
Tactic:
refine
  (g.eqn.filter_mono (nhds_le_nhdsSet ?_)).eventually_nhds.mp
    (eventually_of_forall fun y e ↦ ?_)
State after:
case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ (c, 0) ∈ {c} ×ˢ ball 0 p

case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ Eqns s n r (curry (uncurry r)) y

State before:
case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ (c, 0) ∈ {c} ×ˢ ball 0 p

case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ Eqns s n r (curry (uncurry r)) y
Tactic:
use rfl, mem_ball_self g.pos
State after:
case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ Eqns s n r (curry (uncurry r)) y

State before:
case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ Eqns s n r (curry (uncurry r)) y
Tactic:
simp only [Function.curry_uncurry]
State after:
case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ Eqns s n r r y

State before:
case h.left.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ Eqns s n r r y
Tactic:
exact
  { eqn := e
    start := by
      simp only [Filter.EventuallyEq.refl, imp_true_iff, Filter.eventually_true] }
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, Eqn s (s.np c p) r x
⊢ y.2 = 0 → (𝓝 y).EventuallyEq (uncurry r) (uncurry r)
Tactic:
simp only [Filter.EventuallyEq.refl, imp_true_iff, Filter.eventually_true]
State after:
no goals

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), z ∈ {c} ×ˢ ball 0 p
Tactic:
refine ct.frequently (Filter.Eventually.frequently ?_)
State after:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, (c, x) ∈ {c} ×ˢ ball 0 p

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, (c, x) ∈ {c} ×ˢ ball 0 p
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff]
State after:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ ball 0 p

State before:
case h.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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
c' x : ℂ
m : c' = c ∧ Complex.abs x ≤ p
x0 : x = 0
ct : Tendsto (fun x => (c, x)) (𝓝 0) (𝓝 (c, 0))
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ ball 0 p
Tactic:
exact isOpen_ball.eventually_mem (mem_ball_self g.pos)
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∀ {f0 f1 : ℂ × ℂ → S} {t : Set (ℂ × ℂ)},
    IsOpen t →
      IsPreconnected t →
        (∀ x ∈ t, Eqns s n r (curry f0) x) → (∀ x ∈ t, Eqns s n r (curry f1) x) → (∃ x ∈ t, f0 x = f1 x) → EqOn f0 f1 t
Tactic:
intro r0 r1 t _ pre e0 e1 r01
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ EqOn r0 r1 t

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ EqOn r0 r1 t
Tactic:
have u := eqns_unique pre e0 e1 ?_
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
u : EqOn (uncurry (curry r0)) (uncurry (curry r1)) t
⊢ EqOn r0 r1 t

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, uncurry (curry r0) x = uncurry (curry r1) 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
u : EqOn (uncurry (curry r0)) (uncurry (curry r1)) t
⊢ EqOn r0 r1 t

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, uncurry (curry r0) x = uncurry (curry r1) x
Tactic:
simp only [Function.uncurry_curry] at u
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
u : EqOn r0 r1 t
⊢ EqOn r0 r1 t

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, uncurry (curry r0) x = uncurry (curry r1) 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
u : EqOn r0 r1 t
⊢ EqOn r0 r1 t

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, uncurry (curry r0) x = uncurry (curry r1) x
Tactic:
exact u
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, uncurry (curry r0) x = uncurry (curry r1) 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, uncurry (curry r0) x = uncurry (curry r1) x
Tactic:
simp only [Function.uncurry_curry]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, r0 x = r1 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
r0 r1 : ℂ × ℂ → S
t : Set (ℂ × ℂ)
a✝ : IsOpen t
pre : IsPreconnected t
e0 : ∀ x ∈ t, Eqns s n r (curry r0) x
e1 : ∀ x ∈ t, Eqns s n r (curry r1) x
r01 : ∃ x ∈ t, r0 x = r1 x
⊢ ∃ x ∈ t, r0 x = r1 x
Tactic:
exact r01
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
⊢ (c, 0) ∈ {c} ×ˢ ball 0 p
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff, mem_ball_self g.pos]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ curry b.u c 0 = a
Tactic:
rw [curry, b.uf.self_of_nhdsSet m0, uncurry, g.zero]
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (curry b.u x.1 x.2) = x.2
Tactic:
refine g.start.mp ((b.uf.filter_mono (nhds_le_nhdsSet m0)).mp (eventually_of_forall ?_))
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ ∀ (x : ℂ × ℂ),
    b.u x = uncurry r x → s.bottcherNear x.1 (r x.1 x.2) = x.2 → s.bottcherNear x.1 (curry b.u x.1 x.2) = x.2

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ ∀ (x : ℂ × ℂ),
    b.u x = uncurry r x → s.bottcherNear x.1 (r x.1 x.2) = x.2 → s.bottcherNear x.1 (curry b.u x.1 x.2) = x.2
Tactic:
intro x e b
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b✝ : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
x : ℂ × ℂ
e : b✝.u x = uncurry r x
b : s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ s.bottcherNear x.1 (curry b✝.u x.1 x.2) = x.2

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b✝ : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
x : ℂ × ℂ
e : b✝.u x = uncurry r x
b : s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ s.bottcherNear x.1 (curry b✝.u x.1 x.2) = x.2
Tactic:
simp only [curry, uncurry, Prod.mk.eta] 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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b✝ : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
x : ℂ × ℂ
e : b✝.u x = r x.1 x.2
b : s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ s.bottcherNear x.1 (b✝.u x) = x.2

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b✝ : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
x : ℂ × ℂ
e : b✝.u x = r x.1 x.2
b : s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ s.bottcherNear x.1 (b✝.u x) = x.2
Tactic:
rw [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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b✝ : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
x : ℂ × ℂ
e : b✝.u x = r x.1 x.2
b : s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ s.bottcherNear x.1 (r x.1 x.2) = x.2

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b✝ : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
x : ℂ × ℂ
e : b✝.u x = r x.1 x.2
b : s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ s.bottcherNear x.1 (r x.1 x.2) = x.2
Tactic:
exact b
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n (curry b.u) x
Tactic:
have fp := b.up
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
fp : ∀ᶠ (z : ℂ × ℂ) in 𝓝ˢ (closure ({c} ×ˢ ball 0 p)), Eqns s n r (curry b.u) z
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n (curry b.u) x

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
fp : ∀ᶠ (z : ℂ × ℂ) in 𝓝ˢ (closure ({c} ×ˢ ball 0 p)), Eqns s n r (curry b.u) z
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n (curry b.u) x
Tactic:
simp only [closure_prod_eq, closure_singleton, closure_ball _ g.pos.ne'] at fp
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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
fp : ∀ᶠ (z : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqns s n r (curry b.u) z
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n (curry b.u) x

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 : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
b : Base (fun f_1 x => Eqns s n r (curry f_1) x) ({c} ×ˢ ball 0 p) (uncurry r)
m0 : (c, 0) ∈ {c} ×ˢ ball 0 p
fp : ∀ᶠ (z : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqns s n r (curry b.u) z
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n (curry b.u) x
Tactic:
exact fp.mp (eventually_of_forall fun x e ↦ e.eqn.self_of_nhds)
State after:
no goals