Sets · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {s t : Finset α} : s ⋖ t → s.val ⋖ t.val := by

Mathlib declaration: CovBy.finset_val
Held-out module: Mathlib.Data.Finset.Grade
Banned modules (itself + downstream): 7
Reference proof premises (reachable / held-out): 0 / 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.00004

Attempts

sample 0 · round 0Wrong tactic1.6 s model time

Proof

intro h; constructor; intro x; intro hxs; rw [h]; exact hxs

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

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

case left
α : Type u_1
s t : Finset α
h : s ⋖ t
⊢ s.val < t.val

Reference proof

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

alias ⟨_, _root_.CovBy.finset_val⟩ := val_covBy_val