internlm/Lean-Github huggingface dataset:
Theorem: Grow.unique
Proof 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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have inj := (s.bottcherNear_holomorphic _ (s.mem_near c)).local_inj'
  (s.bottcherNear_mfderiv_ne_zero c)
Proof state after:
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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
inj : ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, a, a), s.bottcherNear p.1 p.2.1 = s.bottcherNear p.1 p.2.2 → p.2.1 = p.2.2
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)
Theorem: Grow.unique
Proof 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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
inj : ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, a, a), s.bottcherNear p.1 p.2.1 = s.bottcherNear p.1 p.2.2 → p.2.1 = p.2.2
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
refine ((t.eventually inj).and (g0.start.and g1.start)).mp (eventually_of_forall ?_)
Proof state after:
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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
inj : ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, a, a), s.bottcherNear p.1 p.2.1 = s.bottcherNear p.1 p.2.2 → p.2.1 = p.2.2
⊢ ∀ (x : ℂ × ℂ),
    (s.bottcherNear (x.1, r0 x.1 x.2, r1 x.1 x.2).1 (x.1, r0 x.1 x.2, r1 x.1 x.2).2.1 =
            s.bottcherNear (x.1, r0 x.1 x.2, r1 x.1 x.2).1 (x.1, r0 x.1 x.2, r1 x.1 x.2).2.2 →
          (x.1, r0 x.1 x.2, r1 x.1 x.2).2.1 = (x.1, r0 x.1 x.2, r1 x.1 x.2).2.2) ∧
        s.bottcherNear x.1 (r0 x.1 x.2) = x.2 ∧ s.bottcherNear x.1 (r1 x.1 x.2) = x.2 →
      uncurry r0 x = uncurry r1 x
Theorem: Grow.unique
Proof 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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
inj : ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, a, a), s.bottcherNear p.1 p.2.1 = s.bottcherNear p.1 p.2.2 → p.2.1 = p.2.2
⊢ ∀ (x : ℂ × ℂ),
    (s.bottcherNear (x.1, r0 x.1 x.2, r1 x.1 x.2).1 (x.1, r0 x.1 x.2, r1 x.1 x.2).2.1 =
            s.bottcherNear (x.1, r0 x.1 x.2, r1 x.1 x.2).1 (x.1, r0 x.1 x.2, r1 x.1 x.2).2.2 →
          (x.1, r0 x.1 x.2, r1 x.1 x.2).2.1 = (x.1, r0 x.1 x.2, r1 x.1 x.2).2.2) ∧
        s.bottcherNear x.1 (r0 x.1 x.2) = x.2 ∧ s.bottcherNear x.1 (r1 x.1 x.2) = x.2 →
      uncurry r0 x = uncurry r1 x
Tactic:
intro ⟨e, y⟩ ⟨inj, s0, s1⟩
Proof state after:
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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
inj✝ : ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, a, a), s.bottcherNear p.1 p.2.1 = s.bottcherNear p.1 p.2.2 → p.2.1 = p.2.2
e y : ℂ
inj :
  s.bottcherNear ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).1
        ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.1 =
      s.bottcherNear ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).1
        ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.2 →
    ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.1 =
      ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.2
s0 : s.bottcherNear (e, y).1 (r0 (e, y).1 (e, y).2) = (e, y).2
s1 : s.bottcherNear (e, y).1 (r1 (e, y).1 (e, y).2) = (e, y).2
⊢ uncurry r0 (e, y) = uncurry r1 (e, y)
Theorem: Grow.unique
Proof 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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : ¬p0 < 0
m : (c, 0) ∈ {c} ×ˢ closedBall 0 p0
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 (c, 0)) (𝓝 (c, a, a))
inj✝ : ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, a, a), s.bottcherNear p.1 p.2.1 = s.bottcherNear p.1 p.2.2 → p.2.1 = p.2.2
e y : ℂ
inj :
  s.bottcherNear ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).1
        ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.1 =
      s.bottcherNear ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).1
        ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.2 →
    ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.1 =
      ((e, y).1, r0 (e, y).1 (e, y).2, r1 (e, y).1 (e, y).2).2.2
s0 : s.bottcherNear (e, y).1 (r0 (e, y).1 (e, y).2) = (e, y).2
s1 : s.bottcherNear (e, y).1 (r1 (e, y).1 (e, y).2) = (e, y).2
⊢ uncurry r0 (e, y) = uncurry r1 (e, y)
Tactic:
exact inj (s0.trans s1.symm)
Proof state after:
no goals
Theorem: Grow.unique
Proof 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 r0 r1 : ℂ → ℂ → S
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
pos : p0 < 0
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
simp only [Metric.closedBall_eq_empty.mpr pos, singleton_prod, image_empty, nhdsSet_empty,
  Filter.EventuallyEq, Filter.eventually_bot]
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ ∃ r', Grow s c p n r'
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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'
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof 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)
Theorem: GrowOpen.grow
Proof 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) }
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
n : ℕ := s.np c p
⊢ IsCompact ({c} ×ˢ closedBall 0 p)
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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 _ _)
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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])
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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]
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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)
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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] })
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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]
Proof state after:
no goals
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Theorem: GrowOpen.grow
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : 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
Proof 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
Theorem: GrowOpen.grow
Proof 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]
Proof 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
Theorem: GrowOpen.grow
Proof 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⟩
Proof 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