internlm/Lean-Github huggingface dataset:
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0
Tactic:
apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).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 : ℂ
p : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      mfderiv I I (fun y => s.bottcherNear c y) x ≠ 0 → (c, x) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) x ≠ 0
Tactic:
refine eventually_of_forall fun z m nc ↦ ?_
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 : ℝ
p1 : p < 1
op : OnePreimage s
z : S
m : z ∈ {b | (c, b) ∈ s.near}
nc : mfderiv I I (fun y => s.bottcherNear c y) z ≠ 0
⊢ (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
z : S
m : z ∈ {b | (c, b) ∈ s.near}
nc : mfderiv I I (fun y => s.bottcherNear c y) z ≠ 0
⊢ (c, z) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) z ≠ 0
Tactic:
use m, nc
Proof state after:
no goals
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
⊢ ∀ (k : ℕ), n ≤ k → s.potential c ((f c)^[k] z) < q
Tactic:
intro k nk
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) < q
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) < q
Tactic:
refine lt_of_le_of_lt ?_ pq
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) ≤ p ^ n
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c ((f c)^[k] z) ≤ p ^ n
Tactic:
simp only [s.potential_eqn_iter]
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n
Tactic:
have dn := (Nat.lt_pow_self s.d1 k).le
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ d ^ k ≤ p ^ n
Tactic:
apply _root_.trans (pow_le_pow_of_le_one s.potential_nonneg s.potential_le_one dn)
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ k ≤ p ^ n
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ s.potential c z ^ k ≤ p ^ n
Tactic:
refine _root_.trans (pow_le_pow_left s.potential_nonneg m _) ?_
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ p ^ k ≤ p ^ n
Theorem: Super.has_nice_n
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 : ℝ
p1 : p < 1
op : OnePreimage s
t : Set S
h : ∀ y ∈ t, (c, y) ∈ s.near ∧ mfderiv I I (s.bottcherNear c) y ≠ 0
q : ℝ
qp : 0 < q
qt : {z | s.potential c z < q} ⊆ t
n : ℕ
pq : p ^ n < q
z : S
m : s.potential c z ≤ p
k : ℕ
nk : n ≤ k
dn : k ≤ d ^ k
⊢ p ^ k ≤ p ^ n
Tactic:
exact pow_le_pow_of_le_one (_root_.trans s.potential_nonneg m) p1.le nk
Proof state after:
no goals
Theorem: Super.nice_np
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 : ℝ
p1 : p < 1
op : OnePreimage s
⊢ s.IsNiceN c p (s.np c p)
Tactic:
have q : p < 1 ∧ OnePreimage s := ⟨p1, op⟩
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 : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (s.np c p)
Theorem: Super.nice_np
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 : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (s.np c p)
Tactic:
simp only [Super.np, q, true_and_iff, dif_pos]
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 : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (Nat.find ⋯)
Theorem: Super.nice_np
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 : ℝ
p1 : p < 1
op : OnePreimage s
q : p < 1 ∧ OnePreimage s
⊢ s.IsNiceN c p (Nat.find ⋯)
Tactic:
exact Nat.find_spec (s.has_nice_n c p1)
Proof state after:
no goals
Theorem: Super.np_zero
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 : ℂ
op : OnePreimage s
⊢ s.np c 0 = 0
Tactic:
simp only [Super.np, zero_lt_one, op, true_and_iff, dif_pos, Nat.find_eq_zero, Super.isNice_zero]
Proof state after:
no goals
Theorem: Super.np_mono
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
⊢ s.np c p0 ≤ s.np c p1
Tactic:
have p01 : p0 < 1 := lt_of_le_of_lt le p11
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
⊢ s.np c p0 ≤ s.np c p1
Theorem: Super.np_mono
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
⊢ s.np c p0 ≤ s.np c p1
Tactic:
have e : s.np c p0 = Nat.find (s.has_nice_n c p01) := by
  simp only [Super.np, p01, op, true_and_iff, dif_pos]
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.np c p0 ≤ s.np c p1
Theorem: Super.np_mono
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.np c p0 ≤ s.np c p1
Tactic:
rw [e]
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ Nat.find ⋯ ≤ s.np c p1
Theorem: Super.np_mono
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ Nat.find ⋯ ≤ s.np c p1
Tactic:
apply Nat.find_min'
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.IsNiceN c p0 (s.np c p1)
Theorem: Super.np_mono
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
e : s.np c p0 = Nat.find ⋯
⊢ s.IsNiceN c p0 (s.np c p1)
Tactic:
exact fun z zp ↦ s.nice_np c p11 _ (_root_.trans zp le)
Proof state after:
no goals
Theorem: Super.np_mono
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 : ℂ
p0 p1 : ℝ
le : p0 ≤ p1
p11 : p1 < 1
op : OnePreimage s
p01 : p0 < 1
⊢ s.np c p0 = Nat.find ⋯
Tactic:
simp only [Super.np, p01, op, true_and_iff, dif_pos]
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.orderAt_unique
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
⊢ orderAt f c = p.order
Tactic:
have fa : AnalyticAt 𝕜 f c := ⟨p, fp⟩
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
⊢ orderAt f c = p.order
Theorem: HasFPowerSeriesAt.orderAt_unique
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
⊢ orderAt f c = p.order
Tactic:
simp only [orderAt, fa, dif_pos]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
⊢ (choose ⋯).order = p.order
Theorem: HasFPowerSeriesAt.orderAt_unique
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
⊢ (choose ⋯).order = p.order
Tactic:
have s := choose_spec fa
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
s : HasFPowerSeriesAt f (choose fa) c
⊢ (choose ⋯).order = p.order
Theorem: HasFPowerSeriesAt.orderAt_unique
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
s : HasFPowerSeriesAt f (choose fa) c
⊢ (choose ⋯).order = p.order
Tactic:
generalize hq : choose fa = q
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
s : HasFPowerSeriesAt f (choose fa) c
q : FormalMultilinearSeries 𝕜 𝕜 E
hq : choose fa = q
⊢ q.order = p.order
Theorem: HasFPowerSeriesAt.orderAt_unique
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
s : HasFPowerSeriesAt f (choose fa) c
q : FormalMultilinearSeries 𝕜 𝕜 E
hq : choose fa = q
⊢ q.order = p.order
Tactic:
simp_rw [hq] at s
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
q : FormalMultilinearSeries 𝕜 𝕜 E
hq : choose fa = q
s : HasFPowerSeriesAt f q c
⊢ q.order = p.order
Theorem: HasFPowerSeriesAt.orderAt_unique
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
p : FormalMultilinearSeries 𝕜 𝕜 E
c : 𝕜
fp : HasFPowerSeriesAt f p c
fa : AnalyticAt 𝕜 f c
q : FormalMultilinearSeries 𝕜 𝕜 E
hq : choose fa = q
s : HasFPowerSeriesAt f q c
⊢ q.order = p.order
Tactic:
rw [fp.eq_formalMultilinearSeries s]
Proof state after:
no goals
Theorem: orderAt_eq_zero
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
f0 : f c ≠ 0
⊢ orderAt f c = 0
Tactic:
by_cases fp : AnalyticAt 𝕜 f c
Proof state after:
case pos
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
f0 : f c ≠ 0
fp : AnalyticAt 𝕜 f c
⊢ orderAt f c = 0

case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
f0 : f c ≠ 0
fp : ¬AnalyticAt 𝕜 f c
⊢ orderAt f c = 0