Category theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.HasLeftCalculusOfFractions := by

Mathlib declaration: CategoryTheory.ObjectProperty.SerreClassLocalization.instHasLeftCalculusOfFractionsIsoModSerre
Held-out module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 21 / 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.00005

Attempts

sample 0 · round 0Hallucinated theorem2.5 s model time

Proof

constructor
intro f
apply P.isoModSerre.leftCalculusOfFractions
exact f

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

6:22: error: Invalid field `leftCalculusOfFractions`: The environment does not contain `Function.leftCalculusOfFractions`, so it is not possible to project the field `leftCalculusOfFractions` from an expression
  P.isoModSerre
of type `⦃X Y : C⦄ → (X ⟶ Y) → Prop`
7:8: error: Unknown identifier `f`

Reference proof

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

instance : P.isoModSerre.HasLeftCalculusOfFractions where
  exists_leftFraction X Y φ :=
    ⟨{s := pushout.inl φ.f φ.s
      f := pushout.inr φ.f φ.s,
      hs := MorphismProperty.pushout_inl _ _ φ.hs}, pushout.condition⟩
  ext X' X Y f₁ f₂ s hs eq := by
    refine ⟨_, cokernel.π (f₁ - f₂), ?_, ?_⟩
    · rw [isoModSerre_iff_of_epi]
      exact (exists_isoModSerre_comp_eq_zero_iff P _).1 ⟨_, s, hs, by simpa [sub_eq_zero]⟩
    · simpa only [Preadditive.sub_comp, sub_eq_zero] using cokernel.condition (f₁ - f₂)