Sets · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {s t : Finset α} (h : s ⋖ t) : s.card ⋖ t.card := by

Mathlib declaration: CovBy.card_finset
Held-out module: Mathlib.Data.Finset.Grade
Banned modules (itself + downstream): 7
Reference proof premises (reachable / held-out): 0 / 2

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.00006

Attempts

sample 0 · round 0Incorrect rewrite2.1 s model time

Proof

rw [lt_iff_le_and_ne]
constructor
· exact (le_card_subset_right h).trans (le_trans (le_card_subset_left h) (le_refl _))
· rintro rfl
  exact h.not_le rfl

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

4:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?m.10 < ?m.11
in the target expression
  s.card ⋖ t.card

α : Type u_1
s t : Finset α
h : s ⋖ t
⊢ s.card ⋖ t.card

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.card_finset (h : s ⋖ t) : s.card ⋖ t.card := (val_covBy_val.2 h).card_multiset