internlm/Lean-Github huggingface dataset:
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
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝[t] x) (𝓝 z)
Tactic:
refine Filter.Tendsto.mono_left ?_ nhdsWithin_le_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 : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
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
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
have ic := ian.along_snd.continuousAt
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 : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : ContinuousAt (fun y => i c (y ^ d ^ n)) x
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
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
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : ContinuousAt (fun y => i c (y ^ d ^ n)) x
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
simp only [ContinuousAt, ←bz] at ic
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 : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (i c (b c z)))
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
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
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (i c (b c z)))
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
rw [ib.self_of_nhds] at ic
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 : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (c, z).2)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
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
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (c, z).2)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
exact ic
Proof state after:
no goals
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
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have ba := s.bottcherNearIter_holomorphic e0.self_of_nhds.near
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)
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
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)
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
have inj := ba.local_inj' (eqn_noncritical e0 x0)
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, 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)
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, 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
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
⊢ (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
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
⊢ (𝓝 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)
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).EventuallyEq (uncurry r0) (uncurry r1)
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).EventuallyEq (uncurry r0) (uncurry r1)
Tactic:
apply (t.eventually inj).mp
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 : ℂ × ℂ) 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
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 : ℂ × ℂ) 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 ↦ ?_))
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
⊢ uncurry r0 x = uncurry r1 x
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
⊢ uncurry r0 x = uncurry r1 x
Tactic:
specialize inj _
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, 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