Sets · medium

Statement, exactly as the model and Lean see it

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

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

Attempts

sample 0 · round 0Wrong tactic9.9 s model time

Proof

intro h
split
· intro s a ha
  rw [Finset.cons_eq_insert]
  exact h _ (Finset.insert_subset.2 ⟨ha, rfl⟩)
· intro h'
  intros s a ha
  rw [Finset.cons_eq_insert]
  exact h' _ (Finset.insert_subset.2 ⟨ha, rfl⟩)

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (Finset.cons a s ha)

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 (cons a s ha)` for all `s`
and `a ∉ s`. -/
lemma monotone_iff_forall_le_cons : Monotone f ↔ ∀ s, ∀ ⦃a⦄ (ha), f s ≤ f (cons a s ha) := by
  classical simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]