Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target : StrictMonoOn Int.natAbs (Set.Ici 0) := by

Mathlib declaration: Int.strictMonoOn_natAbs
Held-out module: Mathlib.Data.Int.Lemmas
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.

Not verified1 model calls · 1 Lean checks · $0.00010

Attempts

sample 0 · round 0Syntax error3.7 s model time

Proof

intro x y
cases le_total x y with h1 h2
· have h3 : Int.natAbs x ≤ Int.natAbs y :=
    by rw [Int.natAbs_eq_iff, Int.natAbs_eq_iff] at h1; exact h1
· have h3 : Int.natAbs x ≤ Int.natAbs y :=
    by rw [Int.natAbs_eq_iff, Int.natAbs_eq_iff] at h2; exact h2
constructor
· exact h3
· exact le_antisymm (Int.natAbs x) (Int.natAbs y) h3 rfl

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

5:27: error: unknown tactic
5:19: error: Application type mismatch: The argument
  y
has type
  x ∈ Set.Ici 0
of sort `Prop` but is expected to have type
  ℤ
of sort `Type` in the application
  le_total x y
5:21: error: Invalid syntax for case analysis tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `h1`.

Reference proof

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

theorem strictMonoOn_natAbs : StrictMonoOn natAbs (Ici 0) := fun _ ha _ _ hab =>
  natAbs_lt_natAbs_of_nonneg_of_lt ha hab