Algebra · easy

Statement, exactly as the model and Lean see it

theorem lg_target (G : Type u) [CommGroup G] [Group.FG G] (hG : IsMulTorsion G) : Finite G := by

Mathlib declaration: CommGroup.finite_of_fg_torsion
Held-out module: Mathlib.GroupTheory.FiniteAbelian.Basic
Banned modules (itself + downstream): 7
Reference proof premises (reachable / held-out): 0 / 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.00009

Attempts

sample 0 · round 0Hallucinated theorem3.1 s model time

Proof

haveI := hG
haveI : IsTorsion G := by apply IsMulTorsion.toIsTorsion
haveI : TorsionGroup G := by apply IsTorsion.toTorsionGroup
haveI : TorsionMultiplicativeGroup G := by apply TorsionGroup.toTorsionMultiplicativeGroup
haveI : FiniteType G := by apply TorsionMultiplicativeGroup.toFiniteType
exact FiniteType.instFinite (inferInstance : Finite G)

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

4:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
5:10: error: Unknown identifier `IsTorsion`
5:34: error: Unknown constant `IsMulTorsion.toIsTorsion`
5:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
6:10: error: Unknown identifier `TorsionGroup`
6:37: error: Unknown identifier `IsTorsion.toTorsionGroup`
6:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
7:10: error: Unknown identifier `TorsionMultiplicativeGroup`
7:51: error: Unknown identifier `TorsionGroup.toTorsionMultiplicativeGroup`
7:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
8:10: error: Unknown identifier `FiniteType`
8:35: error: Unknown identifier `TorsionMultiplicativeGroup.toFiniteType`
8:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
9:8: error: Unknown identifier `FiniteType.instFinite`

Reference proof

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

@[deprecated (since := "2026-07-01")] alias finite_of_fg_torsion := finite_of_fg_isMulTorsion