internlm/Lean-Github huggingface dataset:
Theorem: Super.bottcherNear_eq_zero
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
m : (c, z) ∈ s.near
⊢ s.bottcherNear c z = 0 ↔ z = a
Tactic:
simp only [Super.bottcherNear]
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
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
Theorem: Super.bottcherNear_eq_zero
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
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
Tactic:
constructor
Proof state after:
case mp
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
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 → z = a

case mpr
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
m : (c, z) ∈ s.near
⊢ z = a → _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mp
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
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 → z = a
Tactic:
intro za
Proof state after:
case mp
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
m : (c, z) ∈ s.near
za : _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
⊢ z = a
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mp
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
m : (c, z) ∈ s.near
za : _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
⊢ z = a
Tactic:
contrapose za
Proof state after:
case mp
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
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ¬_root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mp
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
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ¬_root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
apply bottcherNear_ne_zero (s.superNearC.s (Set.mem_univ _)) (s.mem_near_to_near' m)
Proof state after:
case mp
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
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) (c, z).2 - ↑(extChartAt I a) a ≠ 0
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mp
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
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) (c, z).2 - ↑(extChartAt I a) a ≠ 0
Tactic:
simp only [sub_ne_zero]
Proof state after:
case mp
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
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) z ≠ ↑(extChartAt I a) a
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mp
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
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) z ≠ ↑(extChartAt I a) a
Tactic:
exact (extChartAt I a).injOn.ne (s.near_subset_chart m) (mem_extChartAt_source I a) za
Proof state after:
no goals
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mpr
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
m : (c, z) ∈ s.near
⊢ z = a → _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
intro za
Proof state after:
case mpr
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
m : (c, z) ∈ s.near
za : z = a
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Theorem: Super.bottcherNear_eq_zero
Proof state before:
case mpr
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
m : (c, z) ∈ s.near
za : z = a
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
simp only [za, sub_self, bottcherNear_zero]
Proof state after:
no goals
Theorem: Super.bottcherNear_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
⊢ s.bottcherNear c a = 0
Tactic:
simp only [Super.bottcherNear, sub_self, bottcherNear_zero]
Proof state after:
no goals
Theorem: Super.bottcherNear_mfderiv_ne_zero
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 : ℂ
⊢ mfderiv I I (s.bottcherNear c) a ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (f := _root_.bottcherNear (s.fl c) d)
Proof state after:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ 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
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ 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]
Proof state after:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Tactic:
exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
Proof state after:
no goals
Theorem: Super.bottcherNear_mfderiv_ne_zero
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 : ℂ
⊢ 1 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ 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
Proof state after:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
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
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
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]
Proof state after:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
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
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof state before:
case a
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
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
Proof 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
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof 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
Proof 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
Theorem: Super.bottcherNear_mfderiv_ne_zero
Proof 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
Proof state after:
no goals
Theorem: Super.bottcherNear_has_inv
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 : ℂ
⊢ ∃ bi,
    HolomorphicAt (I.prod I) I (uncurry bi) (c, 0) ∧
      (∀ᶠ (p : ℂ × S) in 𝓝 (c, a), bi p.1 (s.bottcherNear p.1 p.2) = p.2) ∧
        ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear p.1 (bi p.1 p.2) = p.2
Tactic:
have h := complex_inverse_fun (s.bottcherNear_holomorphic _ (s.mem_near c))
    (s.bottcherNear_mfderiv_ne_zero 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 : ℂ
h :
  ∃ g,
    HolomorphicAt (I.prod I) I (uncurry g) (c, s.bottcherNear c a) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, a), g x.1 (s.bottcherNear x.1 x.2) = x.2) ∧
        ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNear c a), s.bottcherNear x.1 (g x.1 x.2) = x.2
⊢ ∃ bi,
    HolomorphicAt (I.prod I) I (uncurry bi) (c, 0) ∧
      (∀ᶠ (p : ℂ × S) in 𝓝 (c, a), bi p.1 (s.bottcherNear p.1 p.2) = p.2) ∧
        ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear p.1 (bi p.1 p.2) = p.2
Theorem: Super.bottcherNear_has_inv
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 : ℂ
h :
  ∃ g,
    HolomorphicAt (I.prod I) I (uncurry g) (c, s.bottcherNear c a) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, a), g x.1 (s.bottcherNear x.1 x.2) = x.2) ∧
        ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNear c a), s.bottcherNear x.1 (g x.1 x.2) = x.2
⊢ ∃ bi,
    HolomorphicAt (I.prod I) I (uncurry bi) (c, 0) ∧
      (∀ᶠ (p : ℂ × S) in 𝓝 (c, a), bi p.1 (s.bottcherNear p.1 p.2) = p.2) ∧
        ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear p.1 (bi p.1 p.2) = p.2
Tactic:
simp only [s.bottcherNear_a] at h
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 : ℂ
h :
  ∃ g,
    HolomorphicAt (I.prod I) I (uncurry g) (c, 0) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, a), g x.1 (s.bottcherNear x.1 x.2) = x.2) ∧
        ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (g x.1 x.2) = x.2
⊢ ∃ bi,
    HolomorphicAt (I.prod I) I (uncurry bi) (c, 0) ∧
      (∀ᶠ (p : ℂ × S) in 𝓝 (c, a), bi p.1 (s.bottcherNear p.1 p.2) = p.2) ∧
        ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear p.1 (bi p.1 p.2) = p.2
Theorem: Super.bottcherNear_has_inv
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 : ℂ
h :
  ∃ g,
    HolomorphicAt (I.prod I) I (uncurry g) (c, 0) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, a), g x.1 (s.bottcherNear x.1 x.2) = x.2) ∧
        ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (g x.1 x.2) = x.2
⊢ ∃ bi,
    HolomorphicAt (I.prod I) I (uncurry bi) (c, 0) ∧
      (∀ᶠ (p : ℂ × S) in 𝓝 (c, a), bi p.1 (s.bottcherNear p.1 p.2) = p.2) ∧
        ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear p.1 (bi p.1 p.2) = p.2
Tactic:
exact h
Proof state after:
no goals
Theorem: Super.f_noncritical_near_a
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ∀ᶠ (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
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 : 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
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 : 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
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))
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.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))
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), Critical (f p.1) p.2 ↔ p.2 = a
Tactic:
apply (inChart_critical (s.fa (c, a))).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))
⊢ ∀ᶠ (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)
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))
⊢ ∀ᶠ (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
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))
⊢ ∀ᶠ (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))
⊢ ∀ᶠ (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
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
⊢ ∀ᶠ (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)