internlm/Lean-Github huggingface dataset:
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
hg' : ↑(extChartAt I a) ∘ f e ∘ ↑(extChartAt I a).symm = g
⊢ deriv g (↑(extChartAt I a) z) = 0 ↔ deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
rw [_root_.fl, hg']
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
hg' : ↑(extChartAt I a) ∘ f e ∘ ↑(extChartAt I a).symm = g
⊢ deriv g (↑(extChartAt I a) z) = 0 ↔
    deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
hg' : ↑(extChartAt I a) ∘ f e ∘ ↑(extChartAt I a).symm = g
⊢ deriv g (↑(extChartAt I a) z) = 0 ↔
    deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0
Tactic:
clear hg'
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ deriv g (↑(extChartAt I a) z) = 0 ↔
    deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ deriv g (↑(extChartAt I a) z) = 0 ↔
    deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0
Tactic:
rw [Iff.comm]
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Tactic:
have dg : DifferentiableAt ℂ g (extChartAt I a z) := by
  rw [← hg]; apply AnalyticAt.differentiableAt; apply HolomorphicAt.analyticAt I I
  simp only [s.f0]
  apply (HolomorphicAt.extChartAt _).comp; apply (s.fa _).along_snd.comp
  exact HolomorphicAt.extChartAt_symm (PartialEquiv.map_source _ zm)
  simp only [PartialEquiv.left_inv _ zm, s.f0]; exact ezm
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Tactic:
have d0 : ∀ z, DifferentiableAt ℂ (fun z ↦ z - extChartAt I a a) z := fun z ↦
  differentiableAt_id.sub (differentiableAt_const _)
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Tactic:
have d1 : DifferentiableAt ℂ (g ∘ fun z : ℂ ↦ z + extChartAt I a a)
    (extChartAt I a z - extChartAt I a a) := by
  apply DifferentiableAt.comp; simp only [sub_add_cancel, dg]
  exact differentiableAt_id.add (differentiableAt_const _)
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ deriv ((fun z => z - ↑(extChartAt I a) a) ∘ g ∘ fun z => z + ↑(extChartAt I a) a)
        (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Tactic:
simp only [deriv.comp _ (d0 _) d1, deriv_sub_const, deriv_id'', one_mul]
Proof state after:
case hp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ deriv (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔
    deriv g (↑(extChartAt I a) z) = 0
Theorem: Super.f_noncritical_near_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 : ℂ
⊢ ContinuousAt (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) (c, a)
Tactic:
refine continuousAt_fst.prod (ContinuousAt.sub ?_ 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 : ℂ
⊢ ContinuousAt (fun p => ↑(extChartAt I a) p.2) (c, a)
Theorem: Super.f_noncritical_near_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 : ℂ
⊢ ContinuousAt (fun p => ↑(extChartAt I a) p.2) (c, a)
Tactic:
exact (continuousAt_extChartAt I a).comp_of_eq continuousAt_snd rfl
Proof state after:
no goals
Theorem: Super.f_noncritical_near_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 : ℂ
t : Tendsto (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) (𝓝 (c, a)) (𝓝 (c, 0))
am : a ∈ (extChartAt I a).source
em : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), x.2 ∈ (extChartAt I a).source
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
Tactic:
refine (s.fa _).continuousAt.eventually_mem (extChartAt_source_mem_nhds' I ?_)
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 : ℂ
t : Tendsto (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) (𝓝 (c, a)) (𝓝 (c, 0))
am : a ∈ (extChartAt I a).source
em : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), x.2 ∈ (extChartAt I a).source
⊢ uncurry f (c, a) ∈ (extChartAt I a).source
Theorem: Super.f_noncritical_near_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 : ℂ
t : Tendsto (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) (𝓝 (c, a)) (𝓝 (c, 0))
am : a ∈ (extChartAt I a).source
em : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), x.2 ∈ (extChartAt I a).source
⊢ uncurry f (c, a) ∈ (extChartAt I a).source
Tactic:
simp only [uncurry, s.f0, mem_extChartAt_source I a]
Proof state after:
no goals
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ ↑(extChartAt I a) ∘ f e ∘ ↑(extChartAt I a).symm = g
Tactic:
rw [← hg]
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ ↑(extChartAt I a) ∘ f e ∘ ↑(extChartAt I a).symm = fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ ↑(extChartAt I a) ∘ f e ∘ ↑(extChartAt I a).symm = fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))
Tactic:
simp only [Function.comp, s.f0]
Proof state after:
no goals
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z)
Tactic:
rw [← hg]
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ DifferentiableAt ℂ (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ DifferentiableAt ℂ (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Tactic:
apply AnalyticAt.differentiableAt
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ AnalyticAt ℂ (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ AnalyticAt ℂ (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Tactic:
apply HolomorphicAt.analyticAt I I
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Tactic:
simp only [s.f0]
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun w => ↑(extChartAt I a) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Theorem: Super.f_noncritical_near_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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun w => ↑(extChartAt I a) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z)
Tactic:
apply (HolomorphicAt.extChartAt _).comp
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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ HolomorphicAt I I (fun x => f e (↑(extChartAt I a).symm x)) (↑(extChartAt I a) z)

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 : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source