Theorem: Grow.unique (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
p0 p1 : ℝ
n0 n1 : ℕ
g0 : Grow s c p0 n0 r0
g1 : Grow s c p1 n1 r1
p01 : p0 ≤ p1
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
by_cases pos : p0 < 0
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 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)

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
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p0)).EventuallyEq (uncurry r0) (uncurry r1)

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
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have m : (c, (0 : ℂ)) ∈ {c} ×ˢ closedBall (0 : ℂ) p0 := mem_domain c (not_lt.mp pos)
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
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p0)).EventuallyEq (uncurry r0) (uncurry r1)

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
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
refine HolomorphicOn.eq_of_locally_eq g0.holo (g1.holo.mono (domain_mono _ p01))
    (domain_preconnected _ _) ⟨(c, 0), m, ?_⟩
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
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)

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
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have t : ContinuousAt (fun x : ℂ × ℂ ↦ (x.1, r0 x.1 x.2, r1 x.1 x.2)) (c, 0) :=
  continuousAt_fst.prod
    ((g0.eqn.filter_mono (nhds_le_nhdsSet m)).self_of_nhds.holo.continuousAt.prod
      (g1.eqn.filter_mono (nhds_le_nhdsSet (domain_mono c p01 m))).self_of_nhds.holo.continuousAt)
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 : ContinuousAt (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (c, 0)
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)

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 : ContinuousAt (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (c, 0)
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
simp only [ContinuousAt, g0.zero, g1.zero] at t
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))
⊢ (𝓝 (c, 0)).EventuallyEq (uncurry r0) (uncurry r1)

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)
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)

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 ?_)
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

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⟩
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)

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)
State after:
no goals

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]
State after:
no goals