Sets · medium

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {ι : Type u_2} (t : Finset ι) (s : ι → Set α) : (⋃ i ∈ t, s i).ncard ≤ ∑ i ∈ t, (s i).ncard := by

Mathlib declaration: Finset.set_ncard_biUnion_le
Held-out module: Mathlib.Data.Set.Card.Arithmetic
Banned modules (itself + downstream): 6
Reference proof premises (reachable / held-out): 5 / 0

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

Attempts

sample 0 · round 0Lean 3 syntax3.6 s model time

Proof

induction t with head tail using Finset.induction_on with h_head h_tail
· exact ncard_le_sum (Finset.empty) (Finset.empty) (by simp)
· rw [Union.insert, ncard_union_disjoint]
  have : disjoint (s head) (⋃ i ∈ tail, s i) := by
    intro x hx
    rw [mem_insert_iff] at hx
    cases hx with h1 h2
    · exact (disjoint_left h2).mp h1
    · exact h2
  rw [le_add_right]
  exact ncard_le_sum (Finset.insert head tail) (s head) (⋃ i ∈ tail, s i) (by simp) (h_tail _)

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

4:20: error: unknown tactic
4:14: error: Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `head`.

Reference proof

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

lemma set_ncard_biUnion_le (t : Finset ι) (s : ι → Set α) :
    (⋃ i ∈ t, s i).ncard ≤ ∑ i ∈ t, (s i).ncard :=
  t.apply_union_le_sum (by simp) (Set.ncard_union_le _ _)