Sets · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type*} (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 3

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified2 model calls · 1 Lean checks · $0.00023

Retrieved lemmas

1. Set.inter_assoc
2. Set.inter_subset
3. Set.union_assoc
4. Set.inter_comm
5. Set.inter_union_distrib_left
6. Set.inter_union_distrib_right
7. Set.union_inter_distrib_right
8. Set.union_inter_distrib_left

Plan

To prove the theorem `lg_target`, which states that `A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)`, we can use the distributive property of intersection over union. Specifically, the lemma `Set.inter_union_distrib_left` directly expresses this equality: it states that for any sets `s`, `t`, and `u`, `s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u`. In this case, we let `s = A`, `t = B`, and `u = C`. Applying the lemma directly gives the desired result. Therefore, the proof is straightforward—just apply the relevant distributive law from Mathlib.

Attempts

sample 0 · round 0Verified1.4 s model time
Proof
```
apply Set.inter_union_distrib_left
```

Verified proof

theorem lg_target {α : Type*} (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
  apply Set.inter_union_distrib_left

Axioms used: propext, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

ext x
simp only [Set.mem_inter_iff, Set.mem_union]
tauto