Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target (G : Type u) [Group G] [Finite G] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat := by

Mathlib declaration: CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite
Held-out module: Mathlib.CategoryTheory.Galois.Examples
Banned modules (itself + downstream): 5
Reference proof premises (reachable / held-out): 3 / 0

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 0Syntax error3.2 s model time

Proof

apply CategoryTheory.Limits.hasColimitsOfShape_of_hasBinaryProducts_of_hasInitialObject;
  · apply FintypeCat.hasBinaryProducts
  · apply FintypeCat.hasInitialObject

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

4:8: error: Unknown identifier `CategoryTheory.Limits.hasColimitsOfShape_of_hasBinaryProducts_of_hasInitialObject`
5:4: error: No goals to be solved
6:4: error: unexpected token '·'; expected command

Reference proof

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

/-- The category of finite sets has quotients by finite groups in arbitrary universes. -/
instance [Finite G] : HasColimitsOfShape (SingleObj G) FintypeCat.{w} := by
  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm