internlm/Lean-Github huggingface dataset:
Theorem: GrowOpen.grow
Proof 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'
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
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
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
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
Proof 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
Theorem: GrowOpen.grow
Proof 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
Proof 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
Theorem: GrowOpen.grow
Proof 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 ?_))
Proof 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
Theorem: GrowOpen.grow
Proof 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
Proof 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
Theorem: GrowOpen.grow
Proof 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 }
Proof state after:
no goals
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
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 ?_))
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
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)
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
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⟩
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
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)
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
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]
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
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)
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
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
Proof state after:
no goals
Theorem: GrowOpen.grow
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 : ℂ → ℂ → 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
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
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
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
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
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
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
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
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 ⊢
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
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
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
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
Proof 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
Theorem: GrowOpen.grow
Proof 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 ↦ ?_)
Proof 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
Theorem: GrowOpen.grow
Proof 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
Proof 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
Theorem: GrowOpen.grow
Proof 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]
Proof 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
Theorem: GrowOpen.grow
Proof 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] }
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
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]
Proof state after:
no goals
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))
⊢ ∃ᶠ (z : ℂ × ℂ) in 𝓝 (c, 0), z ∈ {c} ×ˢ ball 0 p
Tactic:
refine ct.frequently (Filter.Eventually.frequently ?_)
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, (c, x) ∈ {c} ×ˢ ball 0 p