Theorem: eqns_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 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}
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

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

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

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

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

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

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

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

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

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

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

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

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