Theorem: Super.bottcherNear_mfderiv_ne_zero (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 : ℂ
⊢ mfderiv I I (s.bottcherNear c) a ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (f := _root_.bottcherNear (s.fl c) d)
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 : ℂ
⊢ mfderiv I I (_root_.bottcherNear (s.fl c) d) (↑(extChartAt I a) a - ↑(extChartAt I a) a) ≠ 0

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 : ℂ
⊢ mfderiv I I (fun x => ↑(extChartAt I a) x - ↑(extChartAt I a) a) a ≠ 0

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 : ℂ
⊢ mfderiv I I (_root_.bottcherNear (s.fl c) d) (↑(extChartAt I a) a - ↑(extChartAt I a) a) ≠ 0
Tactic:
simp only [sub_self, mfderiv_eq_fderiv,
  (_root_.bottcherNear_monic (s.superNearC.s (Set.mem_univ c))).hasFDerivAt.fderiv]
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 : ℂ
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0

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 : ℂ
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Tactic:
exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
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 : ℂ
⊢ 1 ≠ 0
Tactic:
norm_num
State after:
no goals

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 : ℂ
⊢ mfderiv I I (fun x => ↑(extChartAt I a) x - ↑(extChartAt I a) a) a ≠ 0
Tactic:
have u : (fun z : S ↦ extChartAt I a z - extChartAt I a a) =
    extChartAt I a - fun _ : S ↦ extChartAt I a a := rfl
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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ mfderiv I I (fun x => ↑(extChartAt I a) x - ↑(extChartAt I a) a) a ≠ 0

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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ mfderiv I I (fun x => ↑(extChartAt I a) x - ↑(extChartAt I a) a) a ≠ 0
Tactic:
rw [u, mfderiv_sub, mfderiv_const, sub_zero]
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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ mfderiv I I (↑(extChartAt I a)) a ≠ 0

case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (↑(extChartAt I a)) a

case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (fun x => ↑(extChartAt I a) a) a

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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ mfderiv I I (↑(extChartAt I a)) a ≠ 0

case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (↑(extChartAt I a)) a

case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (fun x => ↑(extChartAt I a) a) a
Tactic:
exact extChartAt_mderiv_ne_zero a
State after:
case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (↑(extChartAt I a)) a

case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (fun x => ↑(extChartAt I a) a) a

State before:
case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (↑(extChartAt I a)) a

case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (fun x => ↑(extChartAt I a) a) a
Tactic:
exact (HolomorphicAt.extChartAt (mem_extChartAt_source I a)).mdifferentiableAt
State after:
case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (fun x => ↑(extChartAt I a) a) a

State before:
case a.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 : ℂ
u : (fun z => ↑(extChartAt I a) z - ↑(extChartAt I a) a) = ↑(extChartAt I a) - fun x => ↑(extChartAt I a) a
⊢ MDifferentiableAt I I (fun x => ↑(extChartAt I a) a) a
Tactic:
apply mdifferentiableAt_const
State after:
no goals