Theorems / mh_alge_ccfab2

Mathlib held-out

Algebra · easy

Statement, exactly as the model and Lean see it
theorem lg_target {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [Semiring R] [PartialOrder R] [IsOrderedRing R] [SubsemiringClass S R] : IsOrderedRing ↥s := by
Mathlib declaration
SubsemiringClass.toIsOrderedRing
Held-out module
Mathlib.Algebra.Ring.Subsemiring.Order
Banned modules (itself + downstream)
3
Reference proof premises (reachable / held-out)
1 / 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.00037

Attempts

  1. sample 0 · round 0Lean 3 syntax37.5 s model time
    Proof
    intro a b
constructor
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (lt_or_eq_of_le h1)
  · exact (lt_or_eq_of_le h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (lt_or_eq_of_le h1)
  · exact (lt_or_eq_of_le h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (lt_or_eq_of_le h1)
  · exact (lt_or_eq_of_le h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (lt_or_eq_of_le h1)
  · exact (lt_or_eq_of_le h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (lt_or_eq_of_le h1)
  · exact (lt_or_eq_of_le h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (lt_or_eq_of_le h1)
  · exact (lt_or_eq_of_le h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
  cases this with h1 h2
  · exact (le_of_lt_or_eq h1)
  · exact (le_of_lt_or_eq h2)
· intro h
  have : a ≤ b ∨ b ≤ a := le_total a b
 ......
    What Lean printed (this is all the model sees on repair)
    8:21: error: unknown tactic

Reference proof

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

/-- A subsemiring of an ordered semiring is an ordered semiring. -/
instance toIsOrderedRing [Semiring R] [PartialOrder R] [IsOrderedRing R] [SubsemiringClass S R] :
    IsOrderedRing s :=
  Function.Injective.isOrderedRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl