Inequalities · hard

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_2} [Field α] [ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α] : Archimedean α := by

Mathlib declaration: ConditionallyCompleteLinearOrderedField.to_archimedean
Held-out module: Mathlib.Algebra.Order.CompleteField
Banned modules (itself + downstream): 6
Reference proof premises (reachable / held-out): 46 / 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

sample 0 · round 0Wrong namespace1.8 s model time

Proof

constructor
intro x
apply le_Inf
intro h
use 0
exact le_zero (le_of_neg_le_zero h)

What Lean printed (this is all the model sees on repair)

6:8: error: Unknown identifier `le_Inf`
7:8: error: No goals to be solved

Reference proof

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

/-- Any conditionally complete linearly ordered field is archimedean. -/
scoped instance (priority := 100) ConditionallyCompleteLinearOrderedField.to_archimedean
    [Field α] [ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α] : Archimedean α :=
  archimedean_iff_nat_lt.2 <| by
    by_contra! ⟨x, h⟩
    have := csSup_le (range_nonempty Nat.cast)
      (forall_mem_range.2 fun m =>
        le_sub_iff_add_le.2 <| le_csSup ⟨x, forall_mem_range.2 h⟩ ⟨m+1, Nat.cast_succ m⟩)
    linarith