internlm/Lean-Github huggingface dataset:
Theorem: Grow.open
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases domain_open' bp bo with ⟨q, pq, qb⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Theorem: Grow.open
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
use q, pq
Proof state after:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q n r
Theorem: Grow.open
Proof state before:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q n r
Tactic:
apply m.mp
Proof state after:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, (x, r x 0) ∈ s.near → Grow s x q n r
Theorem: Grow.open
Proof state before:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c, (x, r x 0) ∈ s.near → Grow s x q n r
Tactic:
apply ((continuousAt_id.prod continuousAt_const).eventually g.start.eventually_nhds).mp
Proof state after:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n r
Theorem: Grow.open
Proof state before:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n r
Tactic:
refine eventually_nhds_iff.mpr ⟨a, ?_, ao, am⟩
Proof state after:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a, (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n r
Theorem: Grow.open
Proof state before:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a, (∀ᶠ (x : ℂ × ℂ) in 𝓝 (id x, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2) → (x, r x 0) ∈ s.near → Grow s x q n r
Tactic:
intro c' am' start m
Proof state after:
case right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ Grow s c' q n r
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
Tactic:
refine (continuousAt_id.prod ?_).eventually_mem (s.isOpen_near.mem_nhds ?_)
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ContinuousAt (fun c' => r c' 0) c

case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ (id c, r c 0) ∈ s.near
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ ContinuousAt (fun c' => r c' 0) c
Tactic:
exact (g.eqn.filter_mono (nhds_le_nhdsSet (mem_domain c
  g.nonneg))).self_of_nhds.holo.along_fst.continuousAt
Proof state after:
no goals
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
⊢ (id c, r c 0) ∈ s.near
Tactic:
simp only [id, g.zero, s.mem_near c]
Proof state after:
no goals
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ r c' 0 = a✝
Tactic:
have e := start.self_of_nhds
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 : Grow s c p n r
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : s.bottcherNear (id c', 0).1 (r (id c', 0).1 (id c', 0).2) = (id c', 0).2
⊢ r c' 0 = a✝
Theorem: Grow.open
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 : Grow s c p n r
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : s.bottcherNear (id c', 0).1 (r (id c', 0).1 (id c', 0).2) = (id c', 0).2
⊢ r c' 0 = a✝
Tactic:
simp only [id, s.bottcherNear_eq_zero m] at e
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 : Grow s c p n r
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : r c' 0 = a✝
⊢ r c' 0 = a✝
Theorem: Grow.open
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 : Grow s c p n r
e✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
e : r c' 0 = a✝
⊢ r c' 0 = a✝
Tactic:
exact e
Proof state after:
no goals
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c'} ×ˢ closedBall 0 q), Eqn s n r x
Tactic:
refine eventually_nhdsSet_iff_exists.mpr ⟨a ×ˢ b, ao.prod bo, ?_, ?_⟩
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ {c'} ×ˢ closedBall 0 q ⊆ a ×ˢ b

case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
p : ℝ
s : Super f d a✝
r : ℂ → ℂ → S
g : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a ×ˢ b, Eqn s n r x
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ {c'} ×ˢ closedBall 0 q ⊆ a ×ˢ b
Tactic:
exact prod_mono (singleton_subset_iff.mpr am') qb
Proof state after:
no goals
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
⊢ ∀ x ∈ a ×ˢ b, Eqn s n r x
Tactic:
intro x ⟨cm, xm⟩
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
x : ℂ × ℂ
cm : x.1 ∈ a
xm : x.2 ∈ b
⊢ Eqn s n r x
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
q : ℝ
pq : p < q
qb : closedBall 0 q ⊆ b
m✝ : ∀ᶠ (c' : ℂ) in 𝓝 c, (c', r c' 0) ∈ s.near
c' : ℂ
am' : c' ∈ a
start : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (id c', 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
m : (c', r c' 0) ∈ s.near
x : ℂ × ℂ
cm : x.1 ∈ a
xm : x.2 ∈ b
⊢ Eqn s n r x
Tactic:
exact sub x ⟨aa _ cm, bb _ xm⟩
Proof state after:
no goals
Theorem: GrowOpen.point
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
x : ℂ
ax : Complex.abs x ≤ p
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
Tactic:
by_cases za : abs 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
x : ℂ
ax : Complex.abs x ≤ p
za : Complex.abs x = 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y

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
x : ℂ
ax : Complex.abs x ≤ p
za : ¬Complex.abs x = 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y