Functions · hard

Statement, exactly as the model and Lean see it

theorem lg_target {G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : MonotoneOn f (Set.Ici 0)) : Monotone f := by

Mathlib declaration: monotone_of_odd_of_monotoneOn_nonneg
Held-out module: Mathlib.Order.Monotone.Odd
Banned modules (itself + downstream): 21
Reference proof premises (reachable / held-out): 6 / 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.00008

Attempts

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

Proof

intro x y
cases le_total x y with hxy hxy'
· exact (h₂ (Set.Ici 0) x y hxy).mpr (le_antisymm _ _ hxy hxy')
· exact (h₂ (Set.Ici 0) y x hxy').mpr (le_antisymm _ _ hxy' hxy)

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

5:27: error: unknown tactic
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 `hxy`.

Reference proof

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

/-- An odd function on a linear ordered additive commutative group is monotone on the whole group
provided that it is monotone on `Set.Ici 0`. -/
theorem monotone_of_odd_of_monotoneOn_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x)
    (h₂ : MonotoneOn f (Ici 0)) : Monotone f := by
  refine MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂
  rw [← h₁, ← h₁]
  exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)