internlm/Lean-Github huggingface dataset:
Theorem: test_rpow_le_rpow_of_exponent_le
Proof state before:
a b c : ℝ
n m : ℕ
a1 : 1 ≤ a
h : b ≤ c
⊢ a ^ b ≤ a ^ c
Tactic:
bound
Proof state after:
no goals
Theorem: test_rpow_le_rpow_of_exponent_ge
Proof state before:
a b c : ℝ
n m : ℕ
a0 : 0 < a
a1 : a ≤ 1
h : c ≤ b
⊢ a ^ b ≤ a ^ c
Tactic:
bound
Proof state after:
no goals
Theorem: test_with_context
Proof state before:
s : Set ℂ
o : IsOpen s
z : ℂ
h : z ∈ s
⊢ ∃ r, r > 0
Tactic:
rw [Metric.isOpen_iff] at o
Proof state after:
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
⊢ ∃ r, r > 0
Theorem: test_with_context
Proof state before:
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
⊢ ∃ r, r > 0
Tactic:
rcases o z h with ⟨t, tp, bs⟩
Proof state after:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ ∃ r, r > 0
Theorem: test_with_context
Proof state before:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ ∃ r, r > 0
Tactic:
exists t/2
Proof state after:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ t / 2 > 0
Theorem: test_with_context
Proof state before:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ t / 2 > 0
Tactic:
clear o h bs z s
Proof state after:
case intro.intro
t : ℝ
tp : t > 0
⊢ t / 2 > 0
Theorem: test_with_context
Proof state before:
case intro.intro
t : ℝ
tp : t > 0
⊢ t / 2 > 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_try_elab
Proof state before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs w + e
Tactic:
calc abs (f z) = abs (f w - (f w - f z)) := by ring_nf
  _ ≤ abs (f w) + abs (f w - f z) := by bound
  _ ≤ c * abs w + e := by bound [h w wr, sc wz]
Proof state after:
no goals
Theorem: test_try_elab
Proof state before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f z) = Complex.abs (f w - (f w - f z))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: test_try_elab
Proof state before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f w - (f w - f z)) ≤ Complex.abs (f w) + Complex.abs (f w - f z)
Tactic:
bound
Proof state after:
no goals
Theorem: test_try_elab
Proof state before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f w) + Complex.abs (f w - f z) ≤ c * Complex.abs w + e
Tactic:
bound [h w wr, sc wz]
Proof state after:
no goals
Theorem: test_fun_inference
Proof state before:
α : Type
s : Finset α
f g : α → ℂ
⊢ ‖s.sum fun x => f x + g x‖ ≤ s.sum fun x => ‖f x + g x‖
Tactic:
bound
Proof state after:
no goals
Theorem: test_whnf
Proof state before:
x y : ℝ
h : x < y ∧ True
⊢ x ≤ y
Tactic:
bound [h.1]
Proof state after:
no goals
Theorem: test_unknown_identifier
Proof state before:
f : ℕ → ℝ
le : ∀ (n : ℕ), f n ≤ ↑n
⊢ ∀ (n : ℕ), f n ≤ ↑n
Tactic:
intro n
Proof state after:
f : ℕ → ℝ
le : ∀ (n : ℕ), f n ≤ ↑n
n : ℕ
⊢ f n ≤ ↑n
Theorem: test_unknown_identifier
Proof state before:
f : ℕ → ℝ
le : ∀ (n : ℕ), f n ≤ ↑n
n : ℕ
⊢ f n ≤ ↑n
Tactic:
bound [le n]
Proof state after:
no goals
Theorem: le_sqr_add
Proof state before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 2 * Complex.abs z ≤ Complex.abs (z ^ 2 + c)
Tactic:
calc Complex.abs (z^2 + c)
  _ ≥ Complex.abs (z^2) - abs c := by bound
  _ ≥ Complex.abs (z^2) - abs z := by bound
  _ ≥ (abs z - 1) * abs z := by rw [mul_comm, mul_sub_one, ←pow_two, ←Complex.abs.map_pow]
  _ ≥ 2 * abs z := by bound
Proof state after:
no goals
Theorem: le_sqr_add
Proof state before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ 2 + c) ≥ Complex.abs (z ^ 2) - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: le_sqr_add
Proof state before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ 2) - Complex.abs c ≥ Complex.abs (z ^ 2) - Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: le_sqr_add
Proof state before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ 2) - Complex.abs z ≥ (Complex.abs z - 1) * Complex.abs z
Tactic:
rw [mul_comm, mul_sub_one, ←pow_two, ←Complex.abs.map_pow]
Proof state after:
no goals
Theorem: le_sqr_add
Proof state before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ (Complex.abs z - 1) * Complex.abs z ≥ 2 * Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
⊢ ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
Tactic:
clear n0s n1s n0 n1
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 : ℂ
z : S
⊢ ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
Theorem: Super.potential_eq'
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 : ℂ
z : S
⊢ ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
Tactic:
intro n0 n1 n01 n0s _
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z n1
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
rw [← Nat.sub_add_cancel n01]
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)
Tactic:
have m : ∀ k, (c, (f c)^[n0 + k] z) ∈ s.near := by
  intro k; rw [Nat.add_comm]
  simp only [Function.iterate_add, s.iter_stays_near n0s k, 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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)
Tactic:
generalize hk : n1 - n0 = k
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (k + n0)
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (k + n0)
Tactic:
rw [Nat.add_comm]
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)
Tactic:
clear hk
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)
Tactic:
induction' k with k 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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n0 + 0)

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ s.potential' c z n0 = s.potential' c z (n0 + (k + 1))
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
by_cases n01 : n0 ≤ n1
Proof state after:
case pos
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 : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1

case neg
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 : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : ¬n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1
Theorem: Super.potential_eq'
Proof state before:
case pos
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 : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
exact h n01 n0s n1s
Proof state after:
no goals
Theorem: Super.potential_eq'
Proof state before:
case neg
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 : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : ¬n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
exact (h (not_le.mp n01).le n1s n0s).symm
Proof state after:
no goals
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
Tactic:
intro k
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[n0 + k] z) ∈ s.near
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[n0 + k] z) ∈ s.near
Tactic:
rw [Nat.add_comm]
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[k + n0] z) ∈ s.near
Theorem: Super.potential_eq'
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[k + n0] z) ∈ s.near
Tactic:
simp only [Function.iterate_add, s.iter_stays_near n0s k, Function.comp]
Proof state after:
no goals
Theorem: Super.potential_eq'
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n0 + 0)
Tactic:
simp only [Nat.zero_eq, add_zero]
Proof state after:
no goals
Theorem: Super.potential_eq'
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ s.potential' c z n0 = s.potential' c z (n0 + (k + 1))
Tactic:
simp only [Nat.add_succ, Function.iterate_succ', Super.potential', Function.comp]
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c (f c ((f c)^[n0 + k] z))) ^ (↑d ^ (n0 + k).succ)⁻¹
Theorem: Super.potential_eq'
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c (f c ((f c)^[n0 + k] z))) ^ (↑d ^ (n0 + k).succ)⁻¹
Tactic:
rw [s.bottcherNear_eqn (m k)]
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z) ^ d) ^ (↑d ^ (n0 + k).succ)⁻¹
Theorem: Super.potential_eq'
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z) ^ d) ^ (↑d ^ (n0 + k).succ)⁻¹
Tactic:
rw [pow_succ' _ (n0 + k), mul_inv, Complex.abs.map_pow, Real.rpow_mul, ← Real.rpow_natCast _ d]
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    ((Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ ↑d) ^ (↑d)⁻¹) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d
Theorem: Super.potential_eq'
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    ((Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ ↑d) ^ (↑d)⁻¹) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d
Tactic:
rw [← Real.rpow_mul (Complex.abs.nonneg _) _ d⁻¹,
  mul_inv_cancel (s.superAtC.s (Set.mem_univ c)).drz, Real.rpow_one]
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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 : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d