Theorems / mh_ineq_04b8ca

Mathlib held-out

Inequalities · medium

Statement, exactly as the model and Lean see it
theorem lg_target {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {b : α} (hb : ¬IsMin b) : Set.Iic (b - 1) = Set.Iio b := by
Mathlib declaration
Set.Iic_sub_one_eq_Iio_of_not_isMin
Held-out module
Mathlib.Algebra.Order.Interval.Set.SuccPred
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
2 / 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.00005

Attempts

  1. sample 0 · round 0Other1.7 s model time
    Proof
    rw [Set.Iic, Set.Iio]
apply_fun (fun x => x - 1) at hb
exact hb
    What Lean printed (this is all the model sees on repair)
    5:2: error: apply_fun can only handle negations of equality.

Reference proof

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

lemma Iic_sub_one_eq_Iio_of_not_isMin (hb : ¬ IsMin b) : Iic (b - 1) = Iio b := by
  simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb