Theorem: Super.stays_near (Ray/Dynamics/BottcherNearM.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 : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, f c z) ∈ s.near
Tactic:
simp only [Super.near, extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod, Set.mem_inter_iff,
  mem_extChartAt_source, extChartAt_eq_refl, PartialEquiv.refl_source, Set.mem_univ, true_and_iff,
  Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_setOf_eq,
  sub_self] at m ⊢
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
⊢ f c z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'

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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
⊢ f c z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
rcases mem_iUnion.mp (s.near_subset' m.2) with ⟨b, mb⟩
State after:
case intro
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ ball (b, 0) (s.fr b)
⊢ f c z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'

State before:
case intro
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ ball (b, 0) (s.fr b)
⊢ f c z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
simp only [mem_ball_iff_norm, Prod.norm_def, max_lt_iff, Prod.fst_sub, Prod.snd_sub,
  sub_zero] at mb
State after:
case intro
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ f c z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'

State before:
case intro
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ f c z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
constructor
State after:
case intro.left
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ f c z ∈ (extChartAt I a).source

case intro.right
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'

State before:
case intro.left
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ f c z ∈ (extChartAt I a).source
Tactic:
apply s.fr_stays b (c, z)
State after:
case intro.left.ps
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ (c, z) ∈ (extChartAt (I.prod I) (b, a)).source

case intro.left.pr
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ ↑(extChartAt (I.prod I) (b, a)) (c, z) ∈ ball (↑(extChartAt (I.prod I) (b, a)) (b, a)) (s.fr b)

State before:
case intro.left.ps
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ (c, z) ∈ (extChartAt (I.prod I) (b, a)).source

case intro.left.pr
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ ↑(extChartAt (I.prod I) (b, a)) (c, z) ∈ ball (↑(extChartAt (I.prod I) (b, a)) (b, a)) (s.fr b)
Tactic:
simp only [m.1, Super.near, extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod,
  Set.mem_inter_iff, mem_extChartAt_source, extChartAt_eq_refl, PartialEquiv.refl_source,
  Set.mem_univ, true_and_iff, Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id,
  Set.mem_setOf_eq, sub_self]
State after:
case intro.left.pr
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ ↑(extChartAt (I.prod I) (b, a)) (c, z) ∈ ball (↑(extChartAt (I.prod I) (b, a)) (b, a)) (s.fr b)

State before:
case intro.left.pr
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ ↑(extChartAt (I.prod I) (b, a)) (c, z) ∈ ball (↑(extChartAt (I.prod I) (b, a)) (b, a)) (s.fr b)
Tactic:
simp only [m.1, mb.1, mb.2, Super.near, extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod,
  Set.mem_inter_iff, mem_extChartAt_source, extChartAt_eq_refl, PartialEquiv.refl_source,
  Set.mem_univ, true_and_iff, Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id,
  Set.mem_setOf_eq, sub_self, mem_ball_iff_norm, Prod.norm_def, max_lt_iff, Prod.fst_sub,
  Prod.snd_sub, sub_zero]
State after:
no goals

State before:
case intro.right
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
⊢ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
have h := (s.superNearC.s (Set.mem_univ c)).ft m.2
State after:
case intro.right
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
h : s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ {z | (c, z) ∈ s.near'}
⊢ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'

State before:
case intro.right
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
h : s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ {z | (c, z) ∈ s.near'}
⊢ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
simp only [Super.fl, _root_.fl, Function.comp, sub_add_cancel, PartialEquiv.left_inv _ m.1] at h
State after:
case intro.right
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
h : ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a ∈ {z | (c, z) ∈ s.near'}
⊢ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'

State before:
case intro.right
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : z ∈ (extChartAt I a).source ∧ (c, ↑(extChartAt I a) z - ↑(extChartAt I a) a) ∈ s.near'
b : ℂ
mb : ‖c - b‖ < s.fr b ∧ ‖↑(extChartAt I a) z - ↑(extChartAt I a) a‖ < s.fr b
h : ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a ∈ {z | (c, z) ∈ s.near'}
⊢ (c, ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
exact h
State after:
no goals