Theorem: Super.fla (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 : ℂ
⊢ AnalyticAt ℂ (uncurry s.fl) (c, 0)
Tactic:
rw [@analyticAt_iff_holomorphicAt _ _ (ℂ × ℂ) (ModelProd ℂ ℂ) _ _ _ ℂ ℂ _ _ _ II 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 : ℂ
⊢ HolomorphicAt (I.prod I) I (uncurry s.fl) (c, 0)

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 : ℂ
⊢ HolomorphicAt (I.prod I) I (uncurry s.fl) (c, 0)
Tactic:
refine (((analyticAt_id _ _).sub analyticAt_const).holomorphicAt I I).comp ?_
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 : ℂ
⊢ HolomorphicAt (I.prod I) I
    (fun x => (↑(extChartAt I a) ∘ f x.1 ∘ ↑(extChartAt I a).symm) ((fun z => z + ↑(extChartAt I a) a) x.2)) (c, 0)

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 : ℂ
⊢ HolomorphicAt (I.prod I) I
    (fun x => (↑(extChartAt I a) ∘ f x.1 ∘ ↑(extChartAt I a).symm) ((fun z => z + ↑(extChartAt I a) a) x.2)) (c, 0)
Tactic:
refine (HolomorphicAt.extChartAt ?_).comp ?_
State after:
case refine_1
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 : ℂ
⊢ (f (c, 0).1 ∘ ↑(extChartAt I a).symm) ((fun z => z + ↑(extChartAt I a) a) (c, 0).2) ∈ (extChartAt I a).source

case refine_2
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (fun x => (f x.1 ∘ ↑(extChartAt I a).symm) ((fun z => z + ↑(extChartAt I a) a) x.2)) (c, 0)

State before:
case refine_1
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 : ℂ
⊢ (f (c, 0).1 ∘ ↑(extChartAt I a).symm) ((fun z => z + ↑(extChartAt I a) a) (c, 0).2) ∈ (extChartAt I a).source
Tactic:
simp only [s.f0, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
  ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, Function.comp_apply, zero_add,
  PartialEquiv.coe_trans_symm, PartialHomeomorph.coe_coe_symm, ModelWithCorners.toPartialEquiv_coe_symm,
  ModelWithCorners.left_inv, PartialHomeomorph.left_inv, mem_chart_source, PartialEquiv.trans_source,
  ModelWithCorners.source_eq, Set.preimage_univ, Set.inter_univ]
State after:
no goals

State before:
case refine_2
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (fun x => (f x.1 ∘ ↑(extChartAt I a).symm) ((fun z => z + ↑(extChartAt I a) a) x.2)) (c, 0)
Tactic:
refine (s.fa _).comp₂ holomorphicAt_fst ?_
State after:
case refine_2
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a).symm ((fun z => z + ↑(extChartAt I a) a) x.2)) (c, 0)

State before:
case refine_2
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a).symm ((fun z => z + ↑(extChartAt I a) a) x.2)) (c, 0)
Tactic:
refine (HolomorphicAt.extChartAt_symm ?_).comp ?_
State after:
case refine_2.refine_1
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 : ℂ
⊢ (fun z => z + ↑(extChartAt I a) a) (c, 0).2 ∈ (extChartAt I a).target

case refine_2.refine_2
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (fun x => (fun z => z + ↑(extChartAt I a) a) x.2) (c, 0)

State before:
case refine_2.refine_1
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 : ℂ
⊢ (fun z => z + ↑(extChartAt I a) a) (c, 0).2 ∈ (extChartAt I a).target
Tactic:
simp only [extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
  ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, Function.comp_apply, zero_add,
  PartialEquiv.trans_target, ModelWithCorners.target_eq, ModelWithCorners.toPartialEquiv_coe_symm,
  Set.mem_inter_iff, Set.mem_range_self, Set.mem_preimage, ModelWithCorners.left_inv,
  PartialHomeomorph.map_source, mem_chart_source, and_self_iff]
State after:
no goals

State before:
case refine_2.refine_2
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (fun x => (fun z => z + ↑(extChartAt I a) a) x.2) (c, 0)
Tactic:
exact ((analyticAt_snd _).add analyticAt_const).holomorphicAt _ _
State after:
no goals