Sets · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) : (f <*> s).Finite := by

Mathlib declaration: Set.Finite.seq'
Held-out module: Mathlib.Data.Set.Finite.Monad
Banned modules (itself + downstream): 1
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.

Verified2 model calls · 2 Lean checks · $0.00024

Retrieved lemmas

1. Set.Finite.map
2. Set.Finite.image
3. Set.Finite.preimage'
4. Set.Finite.of_surjOn
5. Set.finite_of_finite_preimage
6. Set.Finite.image2
7. Set.Finite.of_preimage
8. Set.BijOn.finite_iff_finite

Attempts

sample 0 · round 0Valid but mathematically wrong1.9 s model time

Proof

apply Set.Finite.image2; assumption

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

3:117: error: unsolved goals
case ht
α β : Type u
f : Set (α → β)
s : Set α
hf : f.Finite
hs : s.Finite
⊢ ((fun x => s) ()).Finite

sample 0 · round 1Verified2.5 s model time

Proof

have := Set.Finite.image2 (fun f => f) hf hs
exact this

Verified proof

theorem lg_target {α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) : (f <*> s).Finite := by
  have := Set.Finite.image2 (fun f => f) hf hs
  exact this

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

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

theorem Finite.seq' {α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) :
    (f <*> s).Finite :=
  hf.seq hs