Sets · medium

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset α → β} [DecidableEq α] : Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s) := by

Mathlib declaration: Finset.monotone_iff_forall_le_insert
Held-out module: Mathlib.Data.Finset.Interval
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 1 / 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.00008

Attempts

sample 0 · round 0Lean 3 syntax4.3 s model time

Proof

intro h
split
· intro s a ha
  have : a ∉ s ∨ a ∈ s := Or.inl ha
  cases this with h1 h2
  · exact h s a h1
  · rw [insert_eq_self at h2]
    exact h s a h2
· intro h'
  intro s a ha
  refine le_antisymm (h' s a ha) _
  rwa [insert_eq_insert]

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 function `f` from `Finset α` is monotone if and only if `f s ≤ f (insert a s)` for all `s` and
`a ∉ s`. -/
lemma monotone_iff_forall_le_insert : Monotone f ↔ ∀ s ⦃a⦄, a ∉ s → f s ≤ f (insert a s) := by
  simp [monotone_iff_forall_le_cons]