Sets · medium

Statement, exactly as the model and Lean see it

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

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

Traces

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

Verified0 model calls · 3 Lean checks · $0.00000

Attempts

attempt 1Wrong tactic

Proof

rfl

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

4:2: error: Tactic `rfl` failed: The left-hand side
  A ⊆ B
is not definitionally equal to the right-hand side
  A ∩ B = A

α : Type u_1
A B : Set α
⊢ A ⊆ B ↔ A ∩ B = A

attempt 2Other

Proof

decide

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

4:2: error: Expected type must not contain free variables
  A ⊆ B ↔ A ∩ B = A

Hint: Use the `+revert` option to automatically clean up and revert free variables

attempt 3Verified
Proof
```
norm_num
```

Verified proof

theorem lg_target {α : Type*} (A B : Set α) : A ⊆ B ↔ A ∩ B = A := by
  norm_num

Axioms used: propext, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

constructor
· intro h; exact Set.inter_eq_left.mpr h
· intro h; rw [← h]; exact Set.inter_subset_right