internlm/Lean-Github huggingface dataset:
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
          0 ↔
        (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
        (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
have em := ((isOpen_extChartAt_source I a).eventually_mem am).prod_inr (𝓝 c)
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
          0 ↔
        (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
        (Critical (f x.1) x.2 ↔ x.2 = 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 : ℂ
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
          0 ↔
        (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
        (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
simp only [← nhds_prod_eq] at em
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
          0 ↔
        (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
        (Critical (f x.1) x.2 ↔ x.2 = 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 : ℂ
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
          0 ↔
        (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
        (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
apply em.mp
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    x.2 ∈ (extChartAt I a).source →
      (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
              (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
            0 ↔
          (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
        (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
          (Critical (f x.1) x.2 ↔ x.2 = 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 : ℂ
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
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    x.2 ∈ (extChartAt I a).source →
      (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
              (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
            0 ↔
          (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
        (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
          (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
have ezm : ∀ᶠ p : ℂ × S in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source := by
  refine (s.fa _).continuousAt.eventually_mem (extChartAt_source_mem_nhds' I ?_)
  simp only [uncurry, s.f0, mem_extChartAt_source I 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
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
ezm : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    x.2 ∈ (extChartAt I a).source →
      (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
              (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
            0 ↔
          (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
        (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
          (Critical (f x.1) x.2 ↔ x.2 = 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 : ℂ
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
ezm : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    x.2 ∈ (extChartAt I a).source →
      (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
              (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
            0 ↔
          (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
        (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
          (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
apply ezm.mp
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
ezm : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    f x.1 x.2 ∈ (extChartAt I a).source →
      x.2 ∈ (extChartAt I a).source →
        (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
                (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
              0 ↔
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
            (Critical (f x.1) x.2 ↔ x.2 = 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 : ℂ
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
ezm : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    f x.1 x.2 ∈ (extChartAt I a).source →
      x.2 ∈ (extChartAt I a).source →
        (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
                (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
              0 ↔
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
            (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
apply eventually_of_forall
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 : ℂ
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
ezm : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
⊢ ∀ (x : ℂ × S),
    f x.1 x.2 ∈ (extChartAt I a).source →
      x.2 ∈ (extChartAt I a).source →
        (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
                (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
              0 ↔
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
            (Critical (f x.1) x.2 ↔ x.2 = a)
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 : ℂ
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
ezm : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
⊢ ∀ (x : ℂ × S),
    f x.1 x.2 ∈ (extChartAt I a).source →
      x.2 ∈ (extChartAt I a).source →
        (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
                (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
              0 ↔
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
            (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
clear t em
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
⊢ ∀ (x : ℂ × S),
    f x.1 x.2 ∈ (extChartAt I a).source →
      x.2 ∈ (extChartAt I a).source →
        (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
                (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
              0 ↔
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
            (Critical (f x.1) x.2 ↔ x.2 = a)
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
⊢ ∀ (x : ℂ × S),
    f x.1 x.2 ∈ (extChartAt I a).source →
      x.2 ∈ (extChartAt I a).source →
        (deriv (s.fl (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).1)
                (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 =
              0 ↔
            (x.1, ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a).2 = 0) →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c a x.1) (↑(extChartAt I a) x.2) = 0) →
            (Critical (f x.1) x.2 ↔ x.2 = a)
Tactic:
intro ⟨e, z⟩ ezm zm d0 m0
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).1 (e, z).2 ∈ (extChartAt I a).source
zm : (e, z).2 ∈ (extChartAt I a).source
d0 :
  deriv (s.fl ((e, z).1, ↑(extChartAt I a) (e, z).2 - ↑(extChartAt I a) a).1)
        ((e, z).1, ↑(extChartAt I a) (e, z).2 - ↑(extChartAt I a) a).2 =
      0 ↔
    ((e, z).1, ↑(extChartAt I a) (e, z).2 - ↑(extChartAt I a) a).2 = 0
m0 : mfderiv I I (f (e, z).1) (e, z).2 = 0 ↔ deriv (inChart f c a (e, z).1) (↑(extChartAt I a) (e, z).2) = 0
⊢ Critical (f (e, z).1) (e, z).2 ↔ (e, z).2 = a
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).1 (e, z).2 ∈ (extChartAt I a).source
zm : (e, z).2 ∈ (extChartAt I a).source
d0 :
  deriv (s.fl ((e, z).1, ↑(extChartAt I a) (e, z).2 - ↑(extChartAt I a) a).1)
        ((e, z).1, ↑(extChartAt I a) (e, z).2 - ↑(extChartAt I a) a).2 =
      0 ↔
    ((e, z).1, ↑(extChartAt I a) (e, z).2 - ↑(extChartAt I a) a).2 = 0
m0 : mfderiv I I (f (e, z).1) (e, z).2 = 0 ↔ deriv (inChart f c a (e, z).1) (↑(extChartAt I a) (e, z).2) = 0
⊢ Critical (f (e, z).1) (e, z).2 ↔ (e, z).2 = a
Tactic:
simp only at ezm zm d0 m0 ⊢
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
d0 : deriv (s.fl e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ ↑(extChartAt I a) z - ↑(extChartAt I a) a = 0
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
⊢ Critical (f e) z ↔ z = a
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
d0 : deriv (s.fl e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ ↑(extChartAt I a) z - ↑(extChartAt I a) a = 0
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
⊢ Critical (f e) z ↔ z = a
Tactic:
simp only [Super.fl, fl, sub_eq_zero, (PartialEquiv.injOn _).eq_iff zm am] at d0
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
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
d0 : deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
⊢ Critical (f e) z ↔ z = a
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
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
d0 : deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
⊢ Critical (f e) z ↔ z = a
Tactic:
simp only [Critical, m0, ← d0]
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
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
d0 : deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
⊢ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0 ↔
    deriv (_root_.fl f a e) (↑(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
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
d0 : deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
⊢ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0 ↔
    deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
unfold inChart
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
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
d0 : deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
⊢ deriv (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z) = 0 ↔
    deriv (_root_.fl f a e) (↑(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
m0 : mfderiv I I (f e) z = 0 ↔ deriv (inChart f c a e) (↑(extChartAt I a) z) = 0
d0 : deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
⊢ deriv (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z) = 0 ↔
    deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
clear m0 d0
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
⊢ deriv (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z) = 0 ↔
    deriv (_root_.fl f a e) (↑(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
⊢ deriv (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) (↑(extChartAt I a) z) = 0 ↔
    deriv (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
generalize hg : (fun w ↦ extChartAt I (f c a) (f e ((extChartAt I a).symm w))) = g
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 (_root_.fl f a e) (↑(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 (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
have hg' : extChartAt I a ∘ f e ∘ (extChartAt I a).symm = g := by
  rw [← hg]; simp only [Function.comp, s.f0]
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 (_root_.fl f a e) (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0