Theorem: eqn_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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have ba := s.bottcherNearIter_holomorphic e0.self_of_nhds.near
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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)

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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have inj := ba.local_inj' (eqn_noncritical e0 x0)
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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r0 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)

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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r0 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
nth_rw 2 [r01] at inj
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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)

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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have t : Tendsto (fun x : ℂ × ℂ ↦ (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x)
    (𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2)) :=
  continuousAt_fst.prod (e0.self_of_nhds.holo.continuousAt.prod e1.self_of_nhds.holo.continuousAt)
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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x) (𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2))
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)

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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x) (𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2))
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
apply (t.eventually inj).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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x) (𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2))
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 x,
    (s.bottcherNearIter n (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.bottcherNearIter n (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) →
      uncurry r0 x = uncurry 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
x : ℂ × ℂ
e0 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r0 y
e1 : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r1 y
r01 : r0 x.1 x.2 = r1 x.1 x.2
x0 : x.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x.1, r0 x.1 x.2)
inj :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x) (𝓝 (x.1, r0 x.1 x.2, r1 x.1 x.2))
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 x,
    (s.bottcherNearIter n (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.bottcherNearIter n (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) →
      uncurry r0 x = uncurry r1 x
Tactic:
refine e0.mp (e1.mp (eventually_of_forall fun x e1 e0 inj ↦ ?_))
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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj :
  s.bottcherNearIter n (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.bottcherNearIter n (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
⊢ uncurry r0 x = uncurry 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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj :
  s.bottcherNearIter n (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.bottcherNearIter n (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
⊢ uncurry r0 x = uncurry r1 x
Tactic:
specialize inj _
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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj :
  s.bottcherNearIter n (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.bottcherNearIter n (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.bottcherNearIter n (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.bottcherNearIter n (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

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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : (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
⊢ uncurry r0 x = uncurry 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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj :
  s.bottcherNearIter n (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.bottcherNearIter n (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.bottcherNearIter n (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.bottcherNearIter n (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

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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : (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
⊢ uncurry r0 x = uncurry r1 x
Tactic:
simp only [Prod.fst]
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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj :
  s.bottcherNearIter n (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.bottcherNearIter n (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.bottcherNearIter n x.1 (r0 x.1 x.2) = s.bottcherNearIter n x.1 (r1 x.1 x.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 r0 r1 : ℂ → ℂ → S
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : (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
⊢ uncurry r0 x = uncurry 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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj :
  s.bottcherNearIter n (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.bottcherNearIter n (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.bottcherNearIter n x.1 (r0 x.1 x.2) = s.bottcherNearIter n x.1 (r1 x.1 x.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 r0 r1 : ℂ → ℂ → S
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : (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
⊢ uncurry r0 x = uncurry r1 x
Tactic:
simp only [uncurry, Prod.fst, Prod.snd, Super.bottcherNearIter, e0.eqn, e1.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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : (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
⊢ uncurry r0 x = uncurry 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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : (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
⊢ uncurry r0 x = uncurry r1 x
Tactic:
simp only [uncurry, Prod.fst, Prod.snd, Prod.ext_iff] at inj
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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : r0 x.1 x.2 = r1 x.1 x.2
⊢ uncurry r0 x = uncurry 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
x✝ : ℂ × ℂ
e0✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r0 y
e1✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x✝, Eqn s n r1 y
r01 : r0 x✝.1 x✝.2 = r1 x✝.1 x✝.2
x0 : x✝.2 ≠ 0
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (x✝.1, r0 x✝.1 x✝.2)
inj✝ :
  ∀ᶠ (p : ℂ × S × S) in 𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2),
    s.bottcherNearIter n p.1 p.2.1 = s.bottcherNearIter n p.1 p.2.2 → p.2.1 = p.2.2
t : Tendsto (fun x => (x.1, r0 x.1 x.2, r1 x.1 x.2)) (𝓝 x✝) (𝓝 (x✝.1, r0 x✝.1 x✝.2, r1 x✝.1 x✝.2))
x : ℂ × ℂ
e1 : Eqn s n r1 x
e0 : Eqn s n r0 x
inj : r0 x.1 x.2 = r1 x.1 x.2
⊢ uncurry r0 x = uncurry r1 x
Tactic:
exact inj
State after:
no goals