internlm/Lean-Github huggingface dataset:
Theorem: Super.continuous_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
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)
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
g : T → ℂ
h : T → S
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => 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)
Theorem: Super.continuous_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
g : T → ℂ
h : T → S
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => 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)
Tactic:
exact hc
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
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)
Theorem: Super.continuous_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
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)
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
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) ∘ (f (g x))^[n]) (h✝ x)
Theorem: Super.continuous_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
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) ∘ (f (g x))^[n]) (h✝ x)
Tactic:
exact s.fa.continuous.comp (gc.prod_mk h)
Proof state after:
no goals
Theorem: Super.continuousOn_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
t : Set T
n : ℕ
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => (f (g x))^[n] (h x)) t
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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => (f (g x))^[0] (h x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
Theorem: Super.continuousOn_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
g : T → ℂ
h : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => (f (g x))^[0] (h x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
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
g : T → ℂ
h : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => h x) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
Theorem: Super.continuousOn_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
g : T → ℂ
h : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => h x) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
Tactic:
exact hc
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
g : T → ℂ
h✝ : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
Theorem: Super.continuousOn_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
g : T → ℂ
h✝ : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
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
g : T → ℂ
h✝ : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) t
Theorem: Super.continuousOn_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
g : T → ℂ
h✝ : T → S
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) t
Tactic:
exact s.fa.continuous.comp_continuousOn (gc.prod h)
Proof state after:
no goals
Theorem: Super.continuousAt_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
x : T
n : ℕ
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => (f (g x))^[n] (h x)) 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
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => (f (g x))^[0] (h x)) 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
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Theorem: Super.continuousAt_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
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => (f (g x))^[0] (h x)) 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
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
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
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => h x) 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
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Theorem: Super.continuousAt_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
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => h x) 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
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Tactic:
exact hc
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
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Theorem: Super.continuousAt_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
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
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
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) x
Theorem: Super.continuousAt_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
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) x
Tactic:
exact (s.fa _).continuousAt.comp (gc.prod h)
Proof state after:
no goals
Theorem: Super.holomorphic_prod_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
n : ℕ
⊢ Holomorphic (I.prod I) (I.prod I) fun p => (p.1, (f p.1)^[n] p.2)
Tactic:
intro p
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
n : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, (f p.1)^[n] p.2)) p
Theorem: Super.holomorphic_prod_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
n : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, (f p.1)^[n] p.2)) p
Tactic:
apply holomorphicAt_fst.prod
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
n : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun x => (f x.1)^[n] x.2) p
Theorem: Super.holomorphic_prod_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
n : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun x => (f x.1)^[n] x.2) p
Tactic:
apply s.holomorphic_iter
Proof state after:
no goals
Theorem: Super.fl0
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 : ℂ
⊢ s.fl c 0 = 0
Tactic:
simp only [Super.fl, _root_.fl, s.f0, Function.comp_apply, zero_add, PartialEquiv.left_inv,
  mem_extChartAt_source, sub_self]
Proof state after:
no goals
Theorem: Super.critical_0
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 : ℂ
⊢ Critical (s.fl c) 0
Tactic:
simp only [Critical, mfderiv_eq_fderiv, Super.fl]
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 : ℂ
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Theorem: Super.critical_0
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 : ℂ
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Tactic:
have p := (s.fla c).along_snd.leading_approx
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 : ℂ
p :
  (fun z =>
      uncurry s.fl ((c, 0).1, z) -
        (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 •
          leadingCoeff (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2) =o[𝓝 (c, 0).2]
    fun z => (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Theorem: Super.critical_0
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 :
  (fun z =>
      uncurry s.fl ((c, 0).1, z) -
        (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 •
          leadingCoeff (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2) =o[𝓝 (c, 0).2]
    fun z => (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Tactic:
simp only [sub_zero, Algebra.id.smul_eq_mul, Super.fl, s.fd, s.fc, mul_one, uncurry] at p
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 : ℂ
p : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Theorem: Super.critical_0
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 : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Tactic:
generalize hg : _root_.fl f a c = g
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 : ℂ
p : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
g : ℂ → ℂ
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0
Theorem: Super.critical_0
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 : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
g : ℂ → ℂ
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0
Tactic:
rw [hg] at p
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0
Theorem: Super.critical_0
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0
Tactic:
have g0 : g 0 = 0 := by rw [← hg]; exact s.fl0
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ fderiv ℂ g 0 = 0
Theorem: Super.critical_0
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ fderiv ℂ g 0 = 0
Tactic:
apply HasFDerivAt.fderiv
Proof state after:
case h
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ HasFDerivAt g 0 0
Theorem: Super.critical_0
Proof state before:
case h
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ HasFDerivAt g 0 0
Tactic:
simp only [hasFDerivAt_iff_isLittleO_nhds_zero, ContinuousLinearMap.zero_apply, sub_zero,
  zero_add, g0]
Proof state after:
case h
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h