Theorem: Grow.congr (Ray/Dynamics/Grow.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ r1 c 0 = a
Tactic:
have e := e.self_of_nhdsSet (mem_domain c g.nonneg)
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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : uncurry r0 (c, 0) = uncurry r1 (c, 0)
⊢ r1 c 0 = a

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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : uncurry r0 (c, 0) = uncurry r1 (c, 0)
⊢ r1 c 0 = a
Tactic:
simp only [uncurry] at e
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r1 c 0 = a

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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r1 c 0 = a
Tactic:
rw [← e]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r0 c 0 = a

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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r0 c 0 = a
Tactic:
exact g.zero
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
refine g.start.mp ((e.filter_mono (nhds_le_nhdsSet (mem_domain c g.nonneg))).mp ?_)
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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    uncurry r0 x = uncurry r1 x → s.bottcherNear x.1 (r0 x.1 x.2) = x.2 → s.bottcherNear x.1 (r1 x.1 x.2) = x.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    uncurry r0 x = uncurry r1 x → s.bottcherNear x.1 (r0 x.1 x.2) = x.2 → s.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
refine eventually_of_forall fun x e s ↦ ?_
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 r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : uncurry r0 x = uncurry r1 x
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : uncurry r0 x = uncurry r1 x
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
simp only [uncurry] at e
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r1 x.1 x.2) = x.2
Tactic:
rw [← e]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s✝ c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
x : ℂ × ℂ
e : r0 x.1 x.2 = r1 x.1 x.2
s : s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
⊢ s✝.bottcherNear x.1 (r0 x.1 x.2) = x.2
Tactic:
exact s
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r1 x
Tactic:
have eqn := g.eqn
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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
eqn : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r0 x
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r1 x

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
eqn : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r0 x
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r1 x
Tactic:
simp only [Filter.EventuallyEq, eventually_nhdsSet_iff_forall] at eqn e ⊢
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
⊢ ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
⊢ ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x
Tactic:
intro x m
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r1 x
Tactic:
refine (eqn x m).mp ((e x m).eventually_nhds.mp (eventually_of_forall fun y e eqn ↦ ?_))
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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, uncurry r0 x = uncurry r1 x
eqn : Eqn s n r0 y
⊢ Eqn s n r1 y

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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
eqn✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, Eqn s n r0 x
e✝ : ∀ x ∈ {c} ×ˢ closedBall 0 p, ∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry r0 x = uncurry r1 x
x : ℂ × ℂ
m : x ∈ {c} ×ˢ closedBall 0 p
y : ℂ × ℂ
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝 y, uncurry r0 x = uncurry r1 x
eqn : Eqn s n r0 y
⊢ Eqn s n r1 y
Tactic:
exact eqn.congr e
State after:
no goals