Theorem: Super.ray_bij (Ray/Dynamics/Ray.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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ BijOn (fun y => (y.1, s.ray y.1 y.2)) s.ext s.post
Tactic:
refine ⟨fun _ m ↦ s.ray_post m, ?_, ?_⟩
State after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ InjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext

case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ SurjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext s.post

State before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ InjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext
Tactic:
intro ⟨c0, x0⟩ m0 ⟨c1, x1⟩ m1 e
State after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : (fun y => (y.1, s.ray y.1 y.2)) (c0, x0) = (fun y => (y.1, s.ray y.1 y.2)) (c1, x1)
⊢ (c0, x0) = (c1, x1)

State before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : (fun y => (y.1, s.ray y.1 y.2)) (c0, x0) = (fun y => (y.1, s.ray y.1 y.2)) (c1, x1)
⊢ (c0, x0) = (c1, x1)
Tactic:
simp only [Prod.ext_iff] at e ⊢
State after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : c0 = c1 ∧ s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1

State before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : c0 = c1 ∧ s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Tactic:
rcases e with ⟨ec, ex⟩
State after:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1

State before:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Tactic:
rw [ec] at m0 ex
State after:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 c1 : ℂ
m0 : (c1, x0) ∈ s.ext
x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c1 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1

State before:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 c1 : ℂ
m0 : (c1, x0) ∈ s.ext
x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c1 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Tactic:
use ec, s.ray_inj m0 m1 ex
State after:
no goals

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ SurjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext s.post
Tactic:
intro ⟨c, x⟩ m
State after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ (c, x) ∈ (fun y => (y.1, s.ray y.1 y.2)) '' s.ext

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ (c, x) ∈ (fun y => (y.1, s.ray y.1 y.2)) '' s.ext
Tactic:
simp only [mem_image, Prod.ext_iff]
State after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ ∃ x_1 ∈ s.ext, x_1.1 = c ∧ s.ray x_1.1 x_1.2 = x

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ ∃ x_1 ∈ s.ext, x_1.1 = c ∧ s.ray x_1.1 x_1.2 = x
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
State after:
case refine_2.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x✝ : S
m✝ : (c, x✝) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = x✝
⊢ ∃ x ∈ s.ext, x.1 = c ∧ s.ray x.1 x.2 = x✝

State before:
case refine_2.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x✝ : S
m✝ : (c, x✝) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = x✝
⊢ ∃ x ∈ s.ext, x.1 = c ∧ s.ray x.1 x.2 = x✝
Tactic:
use⟨c, x⟩, m, rfl, e
State after:
no goals