Theorems / mh_alge_d53cea

Mathlib held-out

Algebra · easy

Statement, exactly as the model and Lean see it
theorem lg_target {G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) : IsFreeGroup ↥H := by
Mathlib declaration
subgroupIsFreeOfIsFree
Held-out module
Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
4 / 1

Traces

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

No configuration has attempted this theorem yet.

Reference proof

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

/-- The Nielsen-Schreier theorem: a subgroup of a free group is free. -/
instance subgroupIsFreeOfIsFree {G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) :
    IsFreeGroup H :=
  IsFreeGroup.ofMulEquiv (endMulEquivSubgroup H)