internlm/Lean-Github huggingface dataset:
Theorem: GrowOpen.grow
Proof 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]
Proof 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
Theorem: GrowOpen.grow
Proof 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)
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
⊢ ∀ {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
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
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
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
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 ?_
Proof 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
Theorem: GrowOpen.grow
Proof 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
Proof 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
Theorem: GrowOpen.grow
Proof 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
Proof 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
Theorem: GrowOpen.grow
Proof 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]
Proof 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
Theorem: GrowOpen.grow
Proof 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
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
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]
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
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]
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
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 ?_))
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
⊢ ∀ (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
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
⊢ ∀ (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
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
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
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
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 ⊢
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
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
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
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]
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
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
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
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
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
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
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
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
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
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
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
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
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
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)
Proof state after:
no goals
Theorem: join_r
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
have above : ∀ k, p k ≤ ps := fun k ↦ mono.ge_of_tendsto tend k
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Theorem: join_r
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
generalize hrs : (fun e x : ℂ ↦
  if h : abs x < ps then r (Nat.find (tend.exists_lt h)) e x else a) = rs
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Theorem: join_r
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
use rs
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Theorem: join_r
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
⊢ ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
intro k x xk
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
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))