Sets · easy

Statement, exactly as the model and Lean see it

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

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 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.00027

Retrieved lemmas

1. Set.compl_union
2. Set.compl_inter
3. Set.inter_subset
4. Set.union_eq_compl_compl_inter_compl
5. Set.inter_eq_compl_compl_union_compl
6. Set.bihimp_def
7. Set.inter_union_compl
8. Set.Iio_union_Ioi

Plan

### Explanation of the Proof: The theorem `lg_target` states that the complement of the union of two sets is equal to the intersection of their complements. This is a well-known identity in set theory called **De Morgan's Law**. To prove this, we can directly use the lemma `Set.compl_union`, which states exactly that: This lemma is already available in Mathlib, so we can apply it directly by instantiating `s` with `A` and `t` with `B`. --- ### Lean Proof Skeleton: This proof uses the existing lemma `Set.compl_union` directly, making the proof very concise.

Skeleton — Lean accepts it with only sorry steps left

have : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := Set.compl_union A B
exact this

Attempts

sample 0 · round 0Verified1.2 s model time
Proof
```
exact Set.compl_union A B
```

Verified proof

theorem lg_target {α : Type*} (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
  exact Set.compl_union A B

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

Reference proof

The proof we wrote and certified before any model ran.

exact Set.compl_union A B