internlm/Lean-Github huggingface dataset:
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) = 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]
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 : (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 : (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
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 : r0 x.1 x.2 = r1 x.1 x.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 : r0 x.1 x.2 = r1 x.1 x.2
⊢ uncurry r0 x = uncurry r1 x
Tactic:
exact inj
Proof state after:
no goals
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
ne : ∃ x ∈ t, uncurry r1 x = uncurry r2 x
⊢ EqOn (uncurry r1) (uncurry r2) t
Tactic:
set u := {x | uncurry r1 x = uncurry r2 x}
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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
ne : ∃ x ∈ t, uncurry r1 x = uncurry r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
⊢ EqOn (uncurry r1) (uncurry r2) t
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
ne : ∃ x ∈ t, uncurry r1 x = uncurry r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
⊢ EqOn (uncurry r1) (uncurry r2) t
Tactic:
replace ne : (t ∩ u).Nonempty := ne
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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
⊢ EqOn (uncurry r1) (uncurry r2) t
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
⊢ EqOn (uncurry r1) (uncurry r2) t
Tactic:
have op : t ∩ u ⊆ interior u := by
  intro ⟨c, x⟩ ⟨mt, mu⟩; rw [mem_interior_iff_mem_nhds]
  by_cases x0 : x = 0; exact ((e1 _ mt).start x0).trans ((e2 _ mt).start x0).symm
  exact eqn_unique (e1 _ mt).eqn (e2 _ mt).eqn mu 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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
⊢ EqOn (uncurry r1) (uncurry r2) t
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
⊢ EqOn (uncurry r1) (uncurry r2) t
Tactic:
have cl : t ∩ closure u ⊆ u := by
  intro x ⟨mt, mu⟩; simp only [mem_setOf, mem_closure_iff_frequently, mem_inter_iff] at mu ⊢
  exact tendsto_nhds_unique_of_frequently_eq (e1 _ mt).holo.continuousAt
    (e2 _ mt).holo.continuousAt mu
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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
cl : t ∩ closure u ⊆ u
⊢ EqOn (uncurry r1) (uncurry r2) t
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
cl : t ∩ closure u ⊆ u
⊢ EqOn (uncurry r1) (uncurry r2) t
Tactic:
exact _root_.trans (pre.relative_clopen ne op cl) interior_subset
Proof state after:
no goals
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
⊢ t ∩ u ⊆ interior u
Tactic:
intro ⟨c, x⟩ ⟨mt, mu⟩
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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
⊢ (c, x) ∈ interior u
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
⊢ (c, x) ∈ interior u
Tactic:
rw [mem_interior_iff_mem_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 r0 r1 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
⊢ u ∈ 𝓝 (c, x)
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
⊢ u ∈ 𝓝 (c, x)
Tactic:
by_cases x0 : x = 0
Proof 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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
x0 : x = 0
⊢ u ∈ 𝓝 (c, x)

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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
x0 : ¬x = 0
⊢ u ∈ 𝓝 (c, x)
Theorem: eqns_unique
Proof 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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
x0 : x = 0
⊢ u ∈ 𝓝 (c, x)

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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
x0 : ¬x = 0
⊢ u ∈ 𝓝 (c, x)
Tactic:
exact ((e1 _ mt).start x0).trans ((e2 _ mt).start x0).symm
Proof 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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
x0 : ¬x = 0
⊢ u ∈ 𝓝 (c, x)
Theorem: eqns_unique
Proof 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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
c x : ℂ
mt : (c, x) ∈ t
mu : (c, x) ∈ u
x0 : ¬x = 0
⊢ u ∈ 𝓝 (c, x)
Tactic:
exact eqn_unique (e1 _ mt).eqn (e2 _ mt).eqn mu x0
Proof state after:
no goals
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
⊢ t ∩ closure u ⊆ u
Tactic:
intro x ⟨mt, mu⟩
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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
x : ℂ × ℂ
mt : x ∈ t
mu : x ∈ closure u
⊢ x ∈ u
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
x : ℂ × ℂ
mt : x ∈ t
mu : x ∈ closure u
⊢ x ∈ u
Tactic:
simp only [mem_setOf, mem_closure_iff_frequently, mem_inter_iff] at mu ⊢
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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
x : ℂ × ℂ
mt : x ∈ t
mu : ∃ᶠ (x : ℂ × ℂ) in 𝓝 x, x ∈ u
⊢ x ∈ u
Theorem: eqns_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 r2 : ℂ → ℂ → S
t : Set (ℂ × ℂ)
pre : IsPreconnected t
e1 : ∀ x ∈ t, Eqns s n r0 r1 x
e2 : ∀ x ∈ t, Eqns s n r0 r2 x
u : Set (ℂ × ℂ) := {x | uncurry r1 x = uncurry r2 x}
ne : (t ∩ u).Nonempty
op : t ∩ u ⊆ interior u
x : ℂ × ℂ
mt : x ∈ t
mu : ∃ᶠ (x : ℂ × ℂ) in 𝓝 x, x ∈ u
⊢ x ∈ u
Tactic:
exact tendsto_nhds_unique_of_frequently_eq (e1 _ mt).holo.continuousAt
  (e2 _ mt).holo.continuousAt mu
Proof state after:
no goals
Theorem: Grow.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
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
Proof 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)
Theorem: Grow.unique
Proof 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)
Proof 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)
Theorem: Grow.unique
Proof 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, ?_⟩
Proof 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)
Theorem: Grow.unique
Proof 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)
Proof 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)
Theorem: Grow.unique
Proof 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
Proof 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)