Theorem: Super.f_noncritical_near_a
Proof state before:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ deriv (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 _ _ _]
Proof state after:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
am : a ∈ (extChartAt I a).source
ezm✝ : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), f p.1 p.2 ∈ (extChartAt I a).source
e : ℂ
z : S
ezm : f e z ∈ (extChartAt I a).source
zm : z ∈ (extChartAt I a).source
g : ℂ → ℂ
hg : (fun w => ↑(extChartAt I (f c a)) (f e (↑(extChartAt I a).symm w))) = g
dg : DifferentiableAt ℂ g (↑(extChartAt I a) z)
d0 : ∀ (z : ℂ), DifferentiableAt ℂ (fun z => z - ↑(extChartAt I a) a) z
d1 : DifferentiableAt ℂ (g ∘ fun z => z + ↑(extChartAt I a) a) (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ deriv g (↑(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)