Theorem: Super.bottcherNear_has_inv (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 : ℂ
⊢ ∃ 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)
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

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

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