Sets · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by

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

Attempts

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

Proof

intros h
obtain ⟨a, H⟩ := h
constructor
exact H
exact t.erase a

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

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

α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∈ t, t.erase a = s

Reference proof

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

lemma _root_.CovBy.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by
  simpa only [← coe_inj, coe_erase] using! h.finset_coe.exists_set_sdiff_singleton