Theorems / mh_ineq_8c7304

Mathlib held-out

Inequalities · hard

Statement, exactly as the model and Lean see it
theorem lg_target {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {x : K} {m n : ℕ} (hx : 0 ≤ x) (h'x : x < 1) : ∑ i ∈ Finset.Ico m n, x ^ i ≤ x ^ m / (1 - x) := by
Mathlib declaration
geom_sum_Ico_le_of_lt_one
Held-out module
Mathlib.Algebra.Order.Field.GeomSum
Banned modules (itself + downstream)
4
Reference proof premises (reachable / held-out)
34 / 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00042

Attempts

  1. sample 0 · round 0Syntax error23.3 s model time
    Proof
    induction' n with d hd using Nat.strong_induction_on
· exact (le_refl (x ^ m / (1 - x)))
· rw [Finset.Ico_eq_Ico]
  have h1 : 0 ≤ x := hx
  have h2 : x < 1 := h'x
  have h3 : 1 - x > 0 := by simp only [sub_pos_iff, h2]
  have h4 : x ^ m / (1 - x) = x ^ m / (1 - x) := rfl
  have h5 : ∑ i ∈ Finset.Ico d (d + 1), x ^ i = ∑ i ∈ Finset.Ico d (d + 1), x ^ i := rfl
  have h6 : ∑ i ∈ Finset.Ico d (d + 1), x ^ i = (x ^ d - 1) / (1 - x) := by
    rw [Finset.Ico_eq_Ico]
    let S := Finset.range d
    have h7 : ∑ i ∈ S, x ^ i = (x ^ d - 1) / (1 - x) := by
      induction' d with k hk using Nat.strong_induction_on
      · exact (le_refl ((x ^ 0 - 1) / (1 - x)))
      · rw [Finset.range_succ, Finset.sum_insert, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Finset.sum_range_right, Finset.sum_range_right]
        rw [Fin......
    What Lean printed (this is all the model sees on repair)
    3:179: error: unsolved goals
case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m : ℕ
hx : 0 ≤ x
h'x : x < 1
⊢ ∑ i ∈ Finset.Ico m 0, x ^ i ≤ x ^ m / (1 - x)

case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m : ℕ
hx : 0 ≤ x
h'x : x < 1
d : ℕ
hd : ∑ i ∈ Finset.Ico m d, x ^ i ≤ x ^ m / (1 - x)
⊢ ∑ i ∈ Finset.Ico m (d + 1), x ^ i ≤ x ^ m / (1 - x)
4:25: error: unexpected token 'using'; expected command

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

lemma geom_sum_Ico_le_of_lt_one (hx : 0 ≤ x) (h'x : x < 1) :
    ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x) := by
  rcases le_or_gt m n with (hmn | hmn)
  · rw [geom_sum_Ico' h'x.ne hmn]
    apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
    simpa using pow_nonneg hx _
  · rw [Ico_eq_empty, sum_empty]
    · apply div_nonneg (pow_nonneg hx _)
      simpa using h'x.le
    · simpa using hmn.le