internlm/Lean-Github huggingface dataset:
Theorem: Super.critical_a
Proof state before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0 ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (extChartAt_symm_mderiv_ne_zero' ?_)
Proof state after:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x + ↑(extChartAt I a) a) 0 ≠ 0

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target
Theorem: Super.critical_a
Proof state before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x + ↑(extChartAt I a) a) 0 ≠ 0
Tactic:
rw [mfderiv_eq_fderiv, fderiv_add_const, ←mfderiv_eq_fderiv]
Proof state after:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x) 0 ≠ 0
Theorem: Super.critical_a
Proof state before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x) 0 ≠ 0
Tactic:
exact id_mderiv_ne_zero
Proof state after:
no goals
Theorem: Super.critical_a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
rw [zero_add]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target
Theorem: Super.critical_a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
apply mem_extChartAt_target
Proof state after:
no goals
Theorem: Super.critical_a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ f c (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ∈ (extChartAt I a).source
Tactic:
simp only [zero_add, e, s.f0]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ a ∈ (extChartAt I a).source
Theorem: Super.critical_a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ a ∈ (extChartAt I a).source
Tactic:
apply mem_extChartAt_source
Proof state after:
no goals
Theorem: Super.f_nontrivial
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 : ℂ
⊢ NontrivialHolomorphicAt (f c) a
Tactic:
refine ⟨(s.fa _).along_snd, ?_⟩
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 : ℂ
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ f c a
Theorem: Super.f_nontrivial
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 : ℂ
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ f c a
Tactic:
simp only [s.f0]
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 : ℂ
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
Theorem: Super.f_nontrivial
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 : ℂ
n : ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
Tactic:
contrapose n
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 : ℂ
n : ¬∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
⊢ ¬∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ¬∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
⊢ ¬∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
simp only [Filter.not_frequently, not_not, Super.fl, fl, Function.comp, sub_eq_zero] at n ⊢
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Tactic:
have gc : ContinuousAt (fun x ↦ (extChartAt I a).symm (x + extChartAt I a a)) 0 := by
  refine (continuousAt_extChartAt_symm I a).comp_of_eq ?_ (by simp only [zero_add])
  exact continuousAt_id.add continuousAt_const
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Tactic:
simp only [ContinuousAt, zero_add, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] at gc
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Tactic:
refine (gc.eventually n).mp (eventually_of_forall ?_)
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ (x : ℂ), f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a → _root_.fl f a c x = 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ (x : ℂ), f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a → _root_.fl f a c x = 0
Tactic:
intro x 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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
x : ℂ
h : f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a
⊢ _root_.fl f a c x = 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
x : ℂ
h : f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a
⊢ _root_.fl f a c x = 0
Tactic:
simp only [_root_.fl, Function.comp, h, sub_self]
Proof state after:
no goals
Theorem: Super.f_nontrivial
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 : ℂ
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
have e := (nontrivialHolomorphicAt_of_order (s.fla c).along_snd ?_).nonconst
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
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 (c, 0).2, uncurry s.fl ((c, 0).1, w) ≠ uncurry s.fl ((c, 0).1, (c, 0).2)
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0

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
c : ℂ
⊢ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 ≠ 0
Theorem: Super.f_nontrivial
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
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 (c, 0).2, uncurry s.fl ((c, 0).1, w) ≠ uncurry s.fl ((c, 0).1, (c, 0).2)
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
simp only [s.fl0, uncurry] at e
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
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Theorem: Super.f_nontrivial
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
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
exact e
Proof state after:
no goals
Theorem: Super.f_nontrivial
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
c : ℂ
⊢ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 ≠ 0
Tactic:
simp only [Super.fl, s.fd, uncurry]
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
c : ℂ
⊢ d ≠ 0
Theorem: Super.f_nontrivial
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
c : ℂ
⊢ d ≠ 0
Tactic:
exact s.d0
Proof state after:
no goals
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
Tactic:
refine (continuousAt_extChartAt_symm I a).comp_of_eq ?_ (by simp only [zero_add])
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ContinuousAt (fun x => x + ↑(extChartAt I a) a) 0
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ContinuousAt (fun x => x + ↑(extChartAt I a) a) 0
Tactic:
exact continuousAt_id.add continuousAt_const
Proof state after:
no goals
Theorem: Super.f_nontrivial
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 : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ 0 + ↑(extChartAt I a) a = ↑(extChartAt I a) a
Tactic:
simp only [zero_add]
Proof state after:
no goals
Theorem: Super.stays_in_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 : ℂ
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
apply ContinuousAt.eventually_mem_nhd
Proof state after:
case fc
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 : ℂ
⊢ ContinuousAt (fun y => f y.1 y.2) (c, a)

case m
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 : ℂ
⊢ (extChartAt I a).source ∈ 𝓝 (f (c, a).1 (c, a).2)
Theorem: Super.stays_in_chart
Proof state before:
case fc
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 : ℂ
⊢ ContinuousAt (fun y => f y.1 y.2) (c, a)

case m
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 : ℂ
⊢ (extChartAt I a).source ∈ 𝓝 (f (c, a).1 (c, a).2)
Tactic:
exact (s.fa.continuous.comp continuous_id).continuousAt
Proof state after:
case m
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 : ℂ
⊢ (extChartAt I a).source ∈ 𝓝 (f (c, a).1 (c, a).2)
Theorem: Super.stays_in_chart
Proof state before:
case m
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 : ℂ
⊢ (extChartAt I a).source ∈ 𝓝 (f (c, a).1 (c, a).2)
Tactic:
simp only [s.f0, Function.comp_id, Function.uncurry_apply_pair, extChartAt_source_mem_nhds I a]
Proof state after:
no goals
Theorem: Super.fr_prop
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 : ℂ
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
rcases(s.fla c).exists_ball_analyticOn with ⟨r0, r0p, fla⟩
Proof state after:
case intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Theorem: Super.fr_prop
Proof state before:
case intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
rcases eventually_nhds_iff.mp (s.stays_in_chart c) with ⟨t, tp, ot, ta⟩
Proof state after:
case intro.intro.intro.intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Theorem: Super.fr_prop
Proof state before:
case intro.intro.intro.intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ (extChartAt (I.prod I) (c, a)).source,
        ↑(extChartAt (I.prod I) (c, a)) p ∈ ball (↑(extChartAt (I.prod I) (c, a)) (c, a)) r →
          f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
set ch := extChartAt II (c, a)
Proof state after:
case intro.intro.intro.intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Theorem: Super.fr_prop
Proof state before:
case intro.intro.intro.intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
set s := ch.target ∩ ch.symm ⁻¹' t
Proof state after:
case intro.intro.intro.intro.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 : ℂ
r0 : ℝ
r0p : 0 < r0
fla : AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r0)
t : Set (ℂ × S)
tp : ∀ x ∈ t, f x.1 x.2 ∈ (extChartAt I a).source
ot : IsOpen t
ta : (c, a) ∈ t
ch : PartialEquiv (ℂ × S) (ℂ × ℂ) := extChartAt (I.prod I) (c, a)
s : Set (ℂ × ℂ) := ch.target ∩ ↑ch.symm ⁻¹' t
⊢ ∃ r > 0,
    AnalyticOn ℂ (uncurry s✝.fl) (ball (c, 0) r) ∧
      ∀ p ∈ ch.source, ↑ch p ∈ ball (↑ch (c, a)) r → f p.1 p.2 ∈ (extChartAt I a).source