Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nat.card (MulChar M R) = Nat.card Mˣ := by

Mathlib declaration: MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity
Held-out module: Mathlib.NumberTheory.MulChar.Duality
Banned modules (itself + downstream): 4
Reference proof premises (reachable / held-out): 1 / 1

Traces

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

Not verified1 model calls · 1 Lean checks · $0.00005

Attempts

sample 0 · round 0Wrong tactic1.4 s model time

Proof

intro M R
apply eq_card_of_injective
apply MulChar.injective

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
⊢ Nat.card (MulChar M R) = Nat.card Mˣ

Reference proof

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

/-- The cardinality of the group of `R`-valued multiplicative characters on a finite commutative
monoid `M` is the same as that of its unit group `Mˣ` when `R` is a ring that has enough roots
of unity. -/
lemma card_eq_card_units_of_hasEnoughRootsOfUnity : Nat.card (MulChar M R) = Nat.card Mˣ :=
  Nat.card_congr (mulEquiv_units M R).some.toEquiv