Theorems / mh_cate_f827c0
Mathlib held-out
Category theory · easy
theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] : CategoryTheory.HasProjectiveResolutions C := by- Mathlib declaration
- CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions
- Held-out module
- Mathlib.CategoryTheory.Abelian.Projective.Resolution
- Banned modules (itself + downstream)
- 20
- 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.00031
Attempts
- sample 0 · round 0Syntax error13.2 s model time
Proof intro X use (0 : CategoryTheory.Object C) ⟶ X apply CategoryTheory.HasProjectiveResolution.mk constructor apply CategoryTheory.ProjectiveResolution.of_zero_complex apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution'' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective_resolution''' apply CategoryTheory.ProjectiveResolution.zero_complex_is_projective......
What Lean printed (this is all the model sees on repair) 51:73: error: unexpected token '...'; expected term
Reference proof
Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.
instance (priority := 100) : HasProjectiveResolutions C where out _ := inferInstance