internlm/Lean-Github huggingface dataset:
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
h : Complex.abs (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e
⊢ Complex.abs (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e
Tactic:
exact h
Proof state after:
no goals
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
Tactic:
suffices e : ∀ᶠ z : ℂ in atInf, s.bottcher c z = s.bottcherNear c z by
  exact e.mp (eventually_of_forall fun z e ↦ by rw [e])
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z = s.bottcherNear c ↑z
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z = s.bottcherNear c ↑z
Tactic:
refine coe_tendsto_inf.eventually (p := fun z ↦ s.bottcher c z = s.bottcherNear c z) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (y : 𝕊) in 𝓝 ∞, (fun z => s.bottcher c z = s.bottcherNear c z) y
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (y : 𝕊) in 𝓝 ∞, (fun z => s.bottcher c z = s.bottcherNear c z) y
Tactic:
apply s.bottcher_eq_bottcherNear
Proof state after:
no goals
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
e : ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z = s.bottcherNear c ↑z
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
Tactic:
exact e.mp (eventually_of_forall fun z e ↦ by rw [e])
Proof state after:
no goals
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
e✝ : ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z = s.bottcherNear c ↑z
z : ℂ
e : s.bottcher c ↑z = s.bottcherNear c ↑z
⊢ s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
Tactic:
rw [e]
Proof state after:
no goals
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
⊢ Complex.abs z⁻¹ < r
Tactic:
simp only [one_div, map_inv₀] at zr ⊢
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zr : r⁻¹ < Complex.abs z
⊢ (Complex.abs z)⁻¹ < r
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zr : r⁻¹ < Complex.abs z
⊢ (Complex.abs z)⁻¹ < r
Tactic:
exact inv_lt_of_inv_lt rp zr
Proof state after:
no goals
Theorem: potential_tendsto
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ Tendsto (fun z => ⋯.potential c ↑z * Complex.abs z) atInf (𝓝 1)
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => s.potential c ↑z * Complex.abs z) atInf (𝓝 1)
Theorem: potential_tendsto
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => s.potential c ↑z * Complex.abs z) atInf (𝓝 1)
Tactic:
simp only [← s.abs_bottcher, ← Complex.abs.map_mul, ← Complex.abs.map_one]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => Complex.abs (s.bottcher c ↑z * z)) atInf (𝓝 (Complex.abs 1))
Theorem: potential_tendsto
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => Complex.abs (s.bottcher c ↑z * z)) atInf (𝓝 (Complex.abs 1))
Tactic:
exact Complex.continuous_abs.continuousAt.tendsto.comp (bottcher_large_approx d c)
Proof state after:
no goals
Theorem: attracts_shift
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 : ℕ
f : S → S
z a : S
k : ℕ
⊢ Attracts f (f^[k] z) a ↔ Attracts f z a
Tactic:
simp only [Attracts, ← Function.iterate_add_apply]
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 : ℕ
f : S → S
z a : S
k : ℕ
⊢ Tendsto (fun n => f^[n + k] z) atTop (𝓝 a) ↔ Tendsto (fun n => f^[n] z) atTop (𝓝 a)
Theorem: attracts_shift
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 : ℕ
f : S → S
z a : S
k : ℕ
⊢ Tendsto (fun n => f^[n + k] z) atTop (𝓝 a) ↔ Tendsto (fun n => f^[n] z) atTop (𝓝 a)
Tactic:
apply @Filter.tendsto_add_atTop_iff_nat _ fun n ↦ f^[n] z
Proof state after:
no goals
Theorem: Super.dp
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
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Super.d1
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
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Super.iter_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
n : ℕ
⊢ (f c)^[n] a = a
Tactic:
induction' n with n h
Proof state after:
case zero
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
⊢ (f c)^[0] a = a

case succ
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
n : ℕ
h : (f c)^[n] a = a
⊢ (f c)^[n + 1] a = a
Theorem: Super.iter_a
Proof state before:
case zero
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
⊢ (f c)^[0] a = a

case succ
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
n : ℕ
h : (f c)^[n] a = a
⊢ (f c)^[n + 1] a = a
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
case succ
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
n : ℕ
h : (f c)^[n] a = a
⊢ (f c)^[n + 1] a = a
Theorem: Super.iter_a
Proof state before:
case succ
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
n : ℕ
h : (f c)^[n] a = a
⊢ (f c)^[n + 1] a = a
Tactic:
simp only [Function.iterate_succ_apply', h, s.f0]
Proof state after:
no goals
Theorem: Super.fla
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 : ℂ
⊢ AnalyticAt ℂ (uncurry s.fl) (c, 0)
Tactic:
rw [@analyticAt_iff_holomorphicAt _ _ (ℂ × ℂ) (ModelProd ℂ ℂ) _ _ _ ℂ ℂ _ _ _ II I]
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (uncurry s.fl) (c, 0)
Theorem: Super.fla
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 : ℂ
⊢ HolomorphicAt (I.prod I) I (uncurry s.fl) (c, 0)
Tactic:
refine (((analyticAt_id _ _).sub analyticAt_const).holomorphicAt I I).comp ?_
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 : ℂ
⊢ 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)
Theorem: Super.fla
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 : ℂ
⊢ 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 ?_
Proof 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)
Theorem: Super.fla
Proof 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]
Proof state after:
no goals
Theorem: Super.fla
Proof 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 ?_
Proof 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)
Theorem: Super.fla
Proof 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 ?_
Proof 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)
Theorem: Super.fla
Proof 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]
Proof state after:
no goals
Theorem: Super.fla
Proof 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 _ _
Proof state after:
no goals
Theorem: Super.holomorphicAt_iter
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
n : ℕ
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h p)) p
Tactic:
induction' n with n h
Proof state after:
case zero
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[0] (h p)) p

case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Theorem: Super.holomorphicAt_iter
Proof state before:
case zero
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[0] (h p)) p

case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Tactic:
simp only [Function.iterate_zero, id]
Proof state after:
case zero
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => h p) p

case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Theorem: Super.holomorphicAt_iter
Proof state before:
case zero
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => h p) p

case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Tactic:
exact ha
Proof state after:
case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Theorem: Super.holomorphicAt_iter
Proof state before:
case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Tactic:
simp_rw [Function.iterate_succ']
Proof state after:
case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p) ∘ (f (g p))^[n]) (h✝ p)) p
Theorem: Super.holomorphicAt_iter
Proof state before:
case succ
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p) ∘ (f (g p))^[n]) (h✝ p)) p
Tactic:
exact (s.fa _).comp₂ ga h
Proof state after:
no goals
Theorem: Super.continuous_iter
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
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
n : ℕ
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => (f (g x))^[n] (h x)
Tactic:
induction' n with n h
Proof state after:
case zero
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
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => (f (g x))^[0] (h x)

case succ
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
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ x)