Theorems / mh_cate_a4e517
Mathlib held-out
Category theory · medium
theorem lg_target {G : Type v} [Group G] [Finite G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat.incl := by- Mathlib declaration
- CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite
- Held-out module
- Mathlib.CategoryTheory.Galois.GaloisObjects
- Banned modules (itself + downstream)
- 9
- Reference proof premises (reachable / held-out)
- 4 / 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.00027
Attempts
- sample 0 · round 0Syntax error9.7 s model time
Proof apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape; apply......
What Lean printed (this is all the model sees on repair) 31:7: error: unexpected token '...'; expected '(', '+', '-' or term 4:8: error: Unknown identifier `CategoryTheory.Limits.preserves_colimits_of_shape_of_preserves_colimits_of_shape`
Reference proof
Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.
noncomputable instance {G : Type v} [Group G] [Finite G] :
PreservesColimitsOfShape (SingleObj G) FintypeCat.incl.{w} := by
choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G
exact Limits.preservesColimitsOfShape_of_equiv (Classical.choice e).toSingleObjEquiv.symm _