internlm/Lean-Github huggingface dataset:
Theorem: Super.near_subset_chart
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
h : (c, z) ∈ (extChartAt (I.prod I) (0, a)).source
⊢ z ∈ (extChartAt I a).source
Tactic:
simp only [extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod_eq] at h
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
h : c ∈ (extChartAt I 0).source ∧ z ∈ (extChartAt I a).source
⊢ z ∈ (extChartAt I a).source
Theorem: Super.near_subset_chart
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 : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
h : c ∈ (extChartAt I 0).source ∧ z ∈ (extChartAt I a).source
⊢ z ∈ (extChartAt I a).source
Tactic:
exact h.2
Proof state after:
no goals
Theorem: Super.mem_near_to_near'
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 : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
have h := Set.mem_of_mem_inter_right m
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 : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : p ∈ ↑(extChartAt (I.prod I) (0, a)) ⁻¹' {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Theorem: Super.mem_near_to_near'
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 : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : p ∈ ↑(extChartAt (I.prod I) (0, a)) ⁻¹' {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
simp only [Set.mem_preimage, extChartAt_prod, PartialEquiv.prod_coe, extChartAt_eq_refl,
  PartialEquiv.refl_coe, id] at h
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 : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : (p.1, ↑(extChartAt I a) p.2) ∈ {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Theorem: Super.mem_near_to_near'
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 : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h : (p.1, ↑(extChartAt I a) p.2) ∈ {p | (p.1, p.2 - ↑(extChartAt I a) a) ∈ s.near'}
⊢ (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a) ∈ s.near'
Tactic:
exact h
Proof state after:
no goals
Theorem: Super.stays_near
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 : ℕ
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 ⊢
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 : ℕ
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'
Theorem: Super.stays_near
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 : ℕ
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⟩
Proof 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'
Theorem: Super.stays_near
Proof 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
Proof 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'
Theorem: Super.stays_near
Proof 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
Proof 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'
Theorem: Super.stays_near
Proof 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)
Proof 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)
Theorem: Super.stays_near
Proof 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]
Proof 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)
Theorem: Super.stays_near
Proof 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]
Proof state after:
no goals
Theorem: Super.stays_near
Proof 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
Proof 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'
Theorem: Super.stays_near
Proof 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
Proof 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'
Theorem: Super.stays_near
Proof 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
Proof state after:
no goals
Theorem: Super.iter_stays_near
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✝ : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
n : ℕ
⊢ (c, (f c)^[n] z) ∈ s.near
Tactic:
induction' n with n h
Proof state after:
case zero
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)^[0] z) ∈ s.near

case succ
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
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Theorem: Super.iter_stays_near
Proof state before:
case zero
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)^[0] z) ∈ s.near

case succ
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
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Tactic:
simp only [Function.iterate_zero, id, m]
Proof state after:
case succ
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
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Theorem: Super.iter_stays_near
Proof state before:
case succ
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
n : ℕ
h : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Tactic:
simp only [Nat.add_succ, Function.iterate_succ', s.stays_near h, Function.comp]
Proof state after:
no goals
Theorem: Super.iter_stays_near'
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 : ℕ
s : Super f d a✝
a b : ℕ
m : (c, (f c)^[a] z) ∈ s.near
ab : a ≤ b
⊢ (c, (f c)^[b] z) ∈ s.near
Tactic:
rw [← Nat.sub_add_cancel ab, Function.iterate_add_apply]
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 : ℕ
s : Super f d a✝
a b : ℕ
m : (c, (f c)^[a] z) ∈ s.near
ab : a ≤ b
⊢ (c, (f c)^[b - a] ((f c)^[a] z)) ∈ s.near
Theorem: Super.iter_stays_near'
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 : ℕ
s : Super f d a✝
a b : ℕ
m : (c, (f c)^[a] z) ∈ s.near
ab : a ≤ b
⊢ (c, (f c)^[b - a] ((f c)^[a] z)) ∈ s.near
Tactic:
exact s.iter_stays_near m _
Proof state after:
no goals
Theorem: Super.reaches_near
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 : ℕ
s : Super f d a✝
z : S
a : Attracts (f c) z a✝
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
rw [Attracts, Filter.tendsto_iff_forall_eventually_mem] at a
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 : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Theorem: Super.reaches_near
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 : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
have e := a {z | (c, z) ∈ s.near} ?_
Proof 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 : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
e : ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ {z | (c, z) ∈ s.near}
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near

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 : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝
Theorem: Super.reaches_near
Proof 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 : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
e : ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ {z | (c, z) ∈ s.near}
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near

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 : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝
Tactic:
exact e
Proof 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 : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝
Theorem: Super.reaches_near
Proof 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 : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝
Tactic:
apply IsOpen.mem_nhds
Proof state after:
case refine_1.hs
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ IsOpen {z | (c, z) ∈ s.near}

case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}
Theorem: Super.reaches_near
Proof state before:
case refine_1.hs
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ IsOpen {z | (c, z) ∈ s.near}

case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}
Tactic:
apply IsOpen.snd_preimage s.isOpen_near
Proof state after:
case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}
Theorem: Super.reaches_near
Proof state before:
case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}
Tactic:
exact s.mem_near c
Proof state after:
no goals