Functions · easy

Statement, exactly as the model and Lean see it

theorem lg_target : Function.RightInverse not not := by

Mathlib declaration: Bool.not_rightInverse
Held-out module: Mathlib.Logic.Equiv.Bool
Banned modules (itself + downstream): 1
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.

Verified0 model calls · 2 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: No `[refl]` lemma registered for relation
  Function.RightInverse

Hint: Add the `[refl]` attribute to reflexivity lemmas for `Function.RightInverse` to use this tactic

⊢ Function.RightInverse not not

attempt 2Verified
Proof
```
decide
```

Verified proof

theorem lg_target : Function.RightInverse not not := by
  decide

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.

theorem not_rightInverse : RightInverse not not := not_not