Theorems / mh_func_7a8899

Mathlib held-out

Functions · easy

Statement, exactly as the model and Lean see it
theorem lg_target : Function.Injective not := by
Mathlib declaration
Bool.not_injective
Held-out module
Mathlib.Logic.Equiv.Bool
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
1 / 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

  1. 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
  Bool
is not definitionally equal to the right-hand side
  not

⊢ Function.Injective not
  2. attempt 2Verified
    Proof
    decide

Verified proof

theorem lg_target : Function.Injective 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_injective : Injective not := Equiv.boolNot.injective