Theorems / mh_ineq_be9cc2

Mathlib held-out

Inequalities · easy

Statement, exactly as the model and Lean see it
theorem lg_target {R : Type u_1} [CommRing R] {P₁ P₂ : RingPreordering R} : ↑P₁ < ↑P₂ ↔ P₁ < P₂ := by
Mathlib declaration
RingPreordering.toSubsemiring_lt_toSubsemiring
Held-out module
Mathlib.Algebra.Order.Ring.Ordering.Basic
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
0 / 0

Traces

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

Verified2 model calls · 2 Lean checks · $0.00013

Attempts

  1. sample 0 · round 0Wrong tactic1.4 s model time
    Proof
    intros; split; intro h
· exact h
· exact h
    What Lean printed (this is all the model sees on repair)
    4:10: error: Tactic `split` failed: Could not split an `if` or `match` expression in the goal

Hint: If you meant to destruct this structure, use the `cases` tactic instead

Hint: Use `set_option trace.split.failure true` to display additional diagnostic information

R : Type u_1
inst✝ : CommRing R
P₁ P₂ : RingPreordering R
⊢ P₁ < P₂ ↔ P₁ < P₂
  2. sample 0 · round 1Verified3.2 s model time
    Proof
    intros
constructor
· intro h
  exact h
· intro h
  exact h

Verified proof

theorem lg_target {R : Type u_1} [CommRing R] {P₁ P₂ : RingPreordering R} : ↑P₁ < ↑P₂ ↔ P₁ < P₂ := by
  intros
  constructor
  · intro h
    exact h
  · intro h
    exact h

Axioms used: propext, Quot.sound

Reference proof

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

@[gcongr]
theorem toSubsemiring_lt_toSubsemiring {P₁ P₂ : RingPreordering R} :
    P₁.toSubsemiring < P₂.toSubsemiring ↔ P₁ < P₂ := .rfl