Theorems / mh_alge_862f71
Mathlib held-out
Algebra · hard
theorem lg_target {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (HomotopyCategory.plus C).IsVerdierRightLocalizing (HomotopyCategory.subcategoryAcyclic C) := by- Mathlib declaration
- DerivedCategory.Plus.instIsVerdierRightLocalizingHomotopyCategoryIntUpPlusSubcategoryAcyclic
- Held-out module
- Mathlib.Algebra.Homology.DerivedCategory.Plus
- Banned modules (itself + downstream)
- 3
- Reference proof premises (reachable / held-out)
- 23 / 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.00031
Attempts
- sample 0 · round 0Syntax error11.5 s model time
Proof intro H apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal''' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal'' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal' apply CategoryTheory.HomotopyCategory.IsVerdierRightLocalizing.of_ideal apply Category......
What Lean printed (this is all the model sees on repair) 36:19: 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 : (HomotopyCategory.plus C).IsVerdierRightLocalizing
(HomotopyCategory.subcategoryAcyclic C) where
fac {K L} φ hK hL := by
obtain ⟨K : CochainComplex _ _, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
obtain ⟨L : CochainComplex _ _, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
simp only [HomotopyCategory.plus_quotient_obj_iff] at hL
obtain ⟨n, hn⟩ := hL
obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective φ
rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK
refine ⟨(HomotopyCategory.quotient _ _).obj (K.truncGE n),
(HomotopyCategory.quotient _ _).map (K.πTruncGE n),
(HomotopyCategory.quotient _ _).map (CochainComplex.truncGEMap φ n ≫ inv (L.πTruncGE n)),
?_, ?_, by simp [← Functor.map_comp]⟩
· simp only [HomotopyCategory.plus_quotient_obj_iff]
exact ⟨n, inferInstance⟩
· rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic]
exact hK.truncGE _