Sets · medium

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {ι : Type u_2} [Finite ι] {s : ι → Set α} (hs : Pairwise (Function.onFun Disjoint s)) : (⋃ i, s i).encard = ∑ᶠ (i : ι), (s i).encard := by

Mathlib declaration: Set.encard_iUnion_of_finite
Held-out module: Mathlib.Data.Set.Card.Arithmetic
Banned modules (itself + downstream): 6
Reference proof premises (reachable / held-out): 5 / 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 0Syntax error2.0 s model time

Proof

intro i j hneq hdisj,
rw [encard_union_disjoint],
exact hs hneq hdisj,

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✝ : Finite ι
s : ι → Set α
hs : Pairwise (Function.onFun Disjoint s)
⊢ (⋃ i, s i).encard = ∑ᶠ (i : ι), (s i).encard
4:22: error: unexpected token ','; expected command

Reference proof

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

lemma encard_iUnion_of_finite [Finite ι] {s : ι → Set α} (hs : Pairwise (Disjoint on s)) :
    (⋃ i, s i).encard = ∑ᶠ i, (s i).encard := by
  rw [← finsum_mem_univ, ← finite_univ.encard_biUnion (fun a _ b _ hab ↦ hs hab)]
  simp