internlm/Lean-Github huggingface dataset:
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
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
have od : (fun z : ℂ ↦ z ^ d) =o[𝓝 0] (fun z ↦ z) := by
  rw [Asymptotics.isLittleO_iff]; intro e ep
  apply ((@Metric.isOpen_ball ℂ _ 0 (min 1 e)).eventually_mem (mem_ball_self (by bound))).mp
  refine eventually_of_forall fun z b ↦ ?_
  simp only at b; rw [mem_ball_zero_iff, Complex.norm_eq_abs, lt_min_iff] at b
  simp only [Complex.norm_eq_abs, Complex.abs.map_pow]
  rw [← Nat.sub_add_cancel s.d2, pow_add, pow_two]
  calc abs z ^ (d - 2) * (abs z * abs z)
    _ ≤ (1:ℝ) ^ (d - 2) * (abs z * abs z) := by bound
    _ = abs z * abs z := by simp only [one_pow, one_mul]
    _ ≤ e * abs z := by bound
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
have p' := (p.trans od).add od
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x - x ^ d + x ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x - x ^ d + x ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
simp only [sub_add_cancel] at p'
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
refine p'.congr_left ?_
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ ∀ (x : ℂ), g x = g x - 0 x
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ ∀ (x : ℂ), g x = g x - 0 x
Tactic:
intro z
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
z : ℂ
⊢ g z = g z - 0 z
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
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
z : ℂ
⊢ g z = g z - 0 z
Tactic:
exact (sub_zero _).symm
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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ g 0 = 0
Tactic:
rw [← hg]
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
⊢ _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 : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ _root_.fl f a c 0 = 0
Tactic:
exact s.fl0
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 : ℂ
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 z => z ^ d) =o[𝓝 0] fun z => z
Tactic:
rw [Asymptotics.isLittleO_iff]
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
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ c * ‖x‖
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
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ c * ‖x‖
Tactic:
intro e ep
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
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ e * ‖x‖
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
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ e * ‖x‖
Tactic:
apply ((@Metric.isOpen_ball ℂ _ 0 (min 1 e)).eventually_mem (mem_ball_self (by bound))).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 : ℂ
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
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ ball 0 (min 1 e) → ‖x ^ d‖ ≤ e * ‖x‖
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
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ ball 0 (min 1 e) → ‖x ^ d‖ ≤ e * ‖x‖
Tactic:
refine eventually_of_forall fun z b ↦ ?_
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
e : ℝ
ep : 0 < e
z : ℂ
b : z ∈ ball 0 (min 1 e)
⊢ ‖z ^ d‖ ≤ e * ‖z‖
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
e : ℝ
ep : 0 < e
z : ℂ
b : z ∈ ball 0 (min 1 e)
⊢ ‖z ^ d‖ ≤ e * ‖z‖
Tactic:
rw [mem_ball_zero_iff, Complex.norm_eq_abs, lt_min_iff] at b
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ ‖z ^ d‖ ≤ e * ‖z‖
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ ‖z ^ d‖ ≤ e * ‖z‖
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs.map_pow]
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ d ≤ e * Complex.abs z
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ d ≤ e * Complex.abs z
Tactic:
rw [← Nat.sub_add_cancel s.d2, pow_add, pow_two]
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ (d - 2) * (Complex.abs z * Complex.abs z) ≤ e * Complex.abs z
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ (d - 2) * (Complex.abs z * Complex.abs z) ≤ e * Complex.abs z
Tactic:
calc abs z ^ (d - 2) * (abs z * abs z)
  _ ≤ (1:ℝ) ^ (d - 2) * (abs z * abs z) := by bound
  _ = abs z * abs z := by simp only [one_pow, one_mul]
  _ ≤ e * abs z := by bound
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 : ℂ
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
e : ℝ
ep : 0 < e
⊢ 0 < min 1 e
Tactic:
bound
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 : ℂ
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ (d - 2) * (Complex.abs z * Complex.abs z) ≤ 1 ^ (d - 2) * (Complex.abs z * Complex.abs z)
Tactic:
bound
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 : ℂ
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ 1 ^ (d - 2) * (Complex.abs z * Complex.abs z) = Complex.abs z * Complex.abs z
Tactic:
simp only [one_pow, one_mul]
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 : ℂ
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
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z * Complex.abs z ≤ e * Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: Super.critical_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 : ℂ
⊢ Critical (f c) a
Tactic:
have h := s.critical_0 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 : Critical (s.fl c) 0
⊢ Critical (f c) a
Theorem: Super.critical_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 : ℂ
h : Critical (s.fl c) 0
⊢ Critical (f c) a
Tactic:
have e := PartialEquiv.left_inv _ (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 : ℂ
h : Critical (s.fl c) 0
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
⊢ Critical (f c) a
Theorem: Super.critical_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 : ℂ
h : Critical (s.fl c) 0
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
⊢ Critical (f c) a
Tactic:
contrapose 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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : ¬Critical (f c) a
⊢ ¬Critical (s.fl c) 0
Theorem: Super.critical_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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : ¬Critical (f c) a
⊢ ¬Critical (s.fl c) 0
Tactic:
simp only [Critical, Super.fl, fl, ← ne_eq] 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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (_root_.fl f a c) 0 ≠ 0
Theorem: Super.critical_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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (_root_.fl f a c) 0 ≠ 0
Tactic:
simp only [mfderiv_eq_fderiv, _root_.fl, Function.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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ fderiv ℂ (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) - ↑(extChartAt I a) a)
      0 ≠
    0
Theorem: Super.critical_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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ fderiv ℂ (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) - ↑(extChartAt I a) a)
      0 ≠
    0
Tactic:
rw [fderiv_sub_const, ←mfderiv_eq_fderiv]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)))) 0 ≠ 0
Theorem: Super.critical_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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)))) 0 ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (extChartAt_mderiv_ne_zero' ?_)
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) 0 ≠ 0

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ f c (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ∈ (extChartAt I a).source
Theorem: Super.critical_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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) 0 ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (f := f c)
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) (↑(extChartAt I a).symm (0 + ↑(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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0 ≠ 0
Theorem: Super.critical_a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ≠ 0
Tactic:
rw [zero_add, e]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) a ≠ 0
Theorem: Super.critical_a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) a ≠ 0
Tactic:
exact h
Proof state after:
no goals