Theorems / mh_ineq_7f6f03

Mathlib held-out

Inequalities · easy

Statement, exactly as the model and Lean see it
theorem lg_target {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α) : f = OrderRingHom.id α := by
Mathlib declaration
OrderRingHom.eq_id
Held-out module
Mathlib.Algebra.Order.Archimedean.Hom
Banned modules (itself + downstream)
7
Reference proof premises (reachable / held-out)
0 / 1

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.00033

Attempts

  1. sample 0 · round 0Syntax error15.7 s model time
    Proof
    intro h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toOrderPreserving) at h
apply_fun (OrderRingHom.toAddMonoidHom) at h
apply_fun (OrderRingHom.toMonoidHom) at h
apply_fun (OrderRingHom.toGroupHom) at h
apply_fun (OrderRingHom.toAddGroupHom) at h
apply_fun (OrderRingHom.toAddCommGroupHom) at h
apply_fun (OrderRingHom.toCommGroupHom) at h
apply_fun (OrderRingHom.toCommRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom.toRingHom) at h
apply_fun (OrderRingHom......
    What Lean printed (this is all the model sees on repair)
    53:28: error: unexpected token '...'; expected term

Reference proof

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

theorem OrderRingHom.eq_id [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α) : f = .id _ :=
  Subsingleton.elim ..