internlm/Lean-Github huggingface dataset:
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
h : 1 ≤ t33 - 1
⊢ (1 - (t33 - 1)⁻¹) * t11 ≥ (1 - (33 - 1)⁻¹) * 11
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
h : 1 ≤ t33 - 1
⊢ (1 - (33 - 1)⁻¹) * 11 ≥ 10.65
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 3 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0 ≤ 0.565
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0 ≤ 0.512
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 3 ≤ 33
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0 < 3 ^ (d - 1) - 1
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0 < 1 - (((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3 - 1)⁻¹
Tactic:
exact sub_pos.mpr (inv_lt_one (by linarith))
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 1 < ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3 - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0.699 + 0.565 / (3 ^ (d - 1) - 1) +
      0.512 /
        ((1 - (((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3 - 1)⁻¹) * ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1)) ≤
    1.03
Tactic:
simp only [hb2, hb3, hb11, hb33] at b2 b3 b6 b11 b33 ⊢
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0.699 + 0.565 / t2 + 0.512 / ((1 - (t33 - 1)⁻¹) * t11) ≤ 1.03
Theorem: iter_error_le_of_z3
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0.699 + 0.565 / t2 + 0.512 / ((1 - (t33 - 1)⁻¹) * t11) ≤ 1.03
Tactic:
exact le_trans (add_le_add (add_le_add_left
  (div_le_div_of_nonneg_left (by norm_num) (by norm_num) b2) _)
  (div_le_div_of_nonneg_left (by norm_num) (by norm_num) b10)) (by norm_num)
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 ≤ 0.565
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 ≤ 0.512
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 < 10.65
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0.699 + 0.565 / 2 + 0.512 / 10.65 ≤ 1.03
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b3 : (4:ℝ) ≤ 4^(d-1) := by
  calc (4:ℝ)^(d-1)
    _ ≥ 4^(2-1) := by bound
    _ = 4 := by norm_num
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b3 : 4 ≤ 4 ^ (d - 1)
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b3 : 4 ≤ 4 ^ (d - 1)
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb3 : (4:ℝ)^(d-1) = t3 at b3
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b2 : (3:ℝ) ≤ t3 - 1 := by linarith
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
b2 : 3 ≤ t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
b2 : 3 ≤ t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb2 : t3 - 1 = t2 at b2
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have t2p : 0 ≤ t2 := by positivity
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b6 : (12:ℝ) ≤ t2 * 4 := by linarith
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b11 : (35:ℝ) ≤ t2^d * t3 - 1 := by
  calc t2^d * t3 - 1
    _ ≥ 3^d * 4 - 1 := by bound
    _ ≥ 3^2 * 4 - 1 := by bound
    _ = 35 := by norm_num
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t2 ^ d * t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t2 ^ d * t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb11 : t2^d * t3 - 1 = t11 at b11
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b33 : (140:ℝ) ≤ t11 * 4 := by linarith
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
b33 : 140 ≤ t11 * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
b33 : 140 ≤ t11 * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb33 : t11 * 4 = t33 at b33
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11 := by
  have h : 1 ≤ t33 - 1 := by linarith
  calc (1 - (t33 - 1)⁻¹) * t11
    _ ≥ (1 - (140 - 1)⁻¹) * 35 := by bound
    _ ≥ 34.748 := by norm_num
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [←hb2, ←hb3, ←hb11, ←hb33] at b2 b6 b11 b33
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine iter_error_le _ (by norm_num) (by norm_num) (by norm_num)
  (bs0 := f_error_le_of_z4 d)
  (bs1 := fun {_} bz ↦ f_error_le_of_z12 d (le_trans b6 bz))
  (bs2 := fun {_} bz ↦ f_error_le_of_z140 d (le_trans b33 bz))
  (le_trans (by norm_num) b11) (le_trans (by norm_num) b33) (by positivity) ?_ ?_ z4 cz
Proof state after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0 < 1 - (((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4 - 1)⁻¹

case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0.619 + 0.528 / (4 ^ (d - 1) - 1) +
      0.5023 /
        ((1 - (((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4 - 1)⁻¹) * ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1)) ≤
    0.8095
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 4 ≤ 4 ^ (d - 1)
Tactic:
calc (4:ℝ)^(d-1)
  _ ≥ 4^(2-1) := by bound
  _ = 4 := by norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 4 ^ (d - 1) ≥ 4 ^ (2 - 1)
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 4 ^ (2 - 1) = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
⊢ 3 ≤ t3 - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
⊢ 0 ≤ t2
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
⊢ 12 ≤ t2 * 4
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
⊢ 35 ≤ t2 ^ d * t3 - 1
Tactic:
calc t2^d * t3 - 1
  _ ≥ 3^d * 4 - 1 := by bound
  _ ≥ 3^2 * 4 - 1 := by bound
  _ = 35 := by norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
⊢ t2 ^ d * t3 - 1 ≥ 3 ^ d * 4 - 1
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
⊢ 3 ^ d * 4 - 1 ≥ 3 ^ 2 * 4 - 1
Tactic:
bound
Proof state after:
no goals