Theorem: eqn_unique
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 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]
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 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