Theorem: Super.f_noncritical_near_a (Ray/Dynamics/BottcherNearM.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.2 = a
Tactic:
have t : ContinuousAt (fun p : ℂ × S ↦ (p.1, extChartAt I a p.2 - extChartAt I a a)) (c, a) := by
  refine continuousAt_fst.prod (ContinuousAt.sub ?_ continuousAt_const)
  exact (continuousAt_extChartAt I a).comp_of_eq continuousAt_snd rfl
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 : ContinuousAt (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) (c, a)
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.2 = a

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 : ContinuousAt (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) (c, a)
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.2 = a
Tactic:
simp only [ContinuousAt, sub_self] at t
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))
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.2 = a

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))
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.2 = a
Tactic:
apply (inChart_critical (s.fa (c, a))).mp
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))
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (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)

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))
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, a),
    (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 (t.eventually (df_ne_zero s.superNearC (Set.mem_univ c))).mp
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))
⊢ ∀ᶠ (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)

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))
⊢ ∀ᶠ (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 am := mem_extChartAt_source I a
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
⊢ ∀ᶠ (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)

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)
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)

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
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)

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
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)

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]
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)

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
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)

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
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)

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
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)

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
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

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 ⊢
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

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
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

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]
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

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
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

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
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

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
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

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]
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

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']
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

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'
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

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]
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

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
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

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 _)
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

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 _)
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

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]
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

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 (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:
rw [deriv.comp _ _ _]
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 (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a) *
        deriv (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a) =
      0 ↔
    deriv g (↑(extChartAt I a) z) = 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 : ℂ
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)
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) 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
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)
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)

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)
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)

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
State after:
no goals

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 ?_)
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

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]
State after:
no goals

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]
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))

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]
State after:
no goals

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]
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)

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
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)

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
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)

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]
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)

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
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

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 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
Tactic:
apply (s.fa _).along_snd.comp
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 => ↑(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

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 x => ↑(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
Tactic:
exact HolomorphicAt.extChartAt_symm (PartialEquiv.map_source _ zm)
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
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source

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
⊢ f e (↑(extChartAt I a).symm (↑(extChartAt I a) z)) ∈ (extChartAt I a).source
Tactic:
simp only [PartialEquiv.left_inv _ zm, s.f0]
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
⊢ f e z ∈ (extChartAt I a).source

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
⊢ f e z ∈ (extChartAt I a).source
Tactic:
exact ezm
State after:
no goals

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
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
⊢ DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
apply DifferentiableAt.comp
State after:
case hg
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
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a)

case hf
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
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)

State before:
case hg
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
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a)

case hf
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
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
simp only [sub_add_cancel, dg]
State after:
case hf
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
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)

State before:
case hf
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
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
exact differentiableAt_id.add (differentiableAt_const _)
State after:
no goals

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 g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a) *
        deriv (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_add_const, deriv_sub_const, deriv_id'', mul_one, sub_add_cancel, Function.comp]
State after:
no goals

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
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)
⊢ DifferentiableAt ℂ g (↑(extChartAt I a) z - ↑(extChartAt I a) a + ↑(extChartAt I a) a)
Tactic:
simp only [sub_add_cancel, dg]
State after:
no goals

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
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)
⊢ DifferentiableAt ℂ (fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
exact differentiableAt_id.add (differentiableAt_const _)
State after:
no goals