Theorems / mh_alge_458b8e
Mathlib held-out
Algebra · medium
theorem lg_target {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)} (PresheafOfModules.evaluation R X) := by- Mathlib declaration
- PresheafOfModules.instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation
- Held-out module
- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
- Banned modules (itself + downstream)
- 19
- Reference proof premises (reachable / held-out)
- 2 / 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.00028
Attempts
- sample 0 · round 0Syntax error12.5 s model time
Proof intro n hlim apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves_limit_of_shape apply CategoryTheory.Limits.preserves_limit_of_preserves......
What Lean printed (this is all the model sees on repair) 39:61: 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 (X : Cᵒᵖ) : PreservesLimitsOfSize.{v, v} (evaluation.{v} R X) where