Algebra · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : Set.powersetCard.compl hm = Set.powersetCard.compl hm := by

Mathlib declaration: Set.powersetCard.compl.congr_simp
Held-out module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 0 / 0

Traces

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

Verified1 model calls · 1 Lean checks · $0.00004

Attempts

sample 0 · round 0Verified1.1 s model time
Proof
```
rfl
```

Verified proof

theorem lg_target {α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : Set.powersetCard.compl hm = Set.powersetCard.compl hm := by
  rfl

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

Reference proof

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