Algebra · hard

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {I : C} [CategoryTheory.Injective I] {L : CochainComplex C ℤ} {i : ℤ} (ι : (CochainComplex.singleFunctor C i).obj I ⟶ L) [L.IsStrictlyGE i] [QuasiIsoAt ι i] : CategoryTheory.IsSplitMono ι := by

Mathlib declaration: CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
Held-out module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Banned modules (itself + downstream): 15
Reference proof premises (reachable / held-out): 46 / 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.00010

Attempts

sample 0 · round 0Wrong tactic3.5 s model time

Proof

intro h
apply CategoryTheory.IsSplitMono.of_exists_right_inverse
use (L.isStrictlyGE i).homological_lemma ι
constructor
· exact (L.isStrictlyGE i).homological_lemma_is_morphism ι
· intro j
  cases j
  · exact (L.isStrictlyGE i).homological_lemma_is_zero ι
  · rw [CategoryTheory.CochainComplex.gradedAt, CategoryTheory.CochainComplex.gradedAt]
    exact (L.isStrictlyGE i).homological_lemma_is_zero ι

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

C : Type u
inst✝⁴ : CategoryTheory.Category.{v, u} C
inst✝³ : CategoryTheory.Abelian C
I : C
inst✝² : CategoryTheory.Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ CategoryTheory.IsSplitMono ι

Reference proof

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

lemma isSplitMono_from_singleFunctor_obj_of_injective
    {I : C} [Injective I] {L : CochainComplex C ℤ} {i : ℤ}
    (ι : (CochainComplex.singleFunctor C i).obj I ⟶ L) [L.IsStrictlyGE i] [QuasiIsoAt ι i] :
    IsSplitMono ι := by
  let e := L.pOpcyclesIso (i - 1) i (by simp)
    ((L.isZero_of_isStrictlyGE i (i - 1) (by simp)).eq_of_src _ _)
  let α := (singleObjHomologySelfIso _ _ _).inv ≫ homologyMap ι i ≫ L.homologyι i ≫ e.inv
  have : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α := by
    rw [← cancel_mono e.hom]
    dsimp [α, e]
    rw [assoc, assoc, assoc, assoc, pOpcyclesIso_inv_hom_id, comp_id, homologyι_naturality]
    dsimp [singleFunctor, singleFunctors]
    rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]
  exact ⟨⟨{
    retraction := mkHomToSingle (Injective.factorThru (𝟙 I) α) (by
      rintro j rfl
      apply (L.isZero_of_isStrictlyGE (j + 1) j (by simp)).eq_of_src)
    id := by
      apply HomologicalComplex.to_single_hom_ext
      rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id] }⟩⟩