Theorems / mh_cate_097148
Mathlib held-out
Category theory · medium
theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYoneda.obj X) := by- Mathlib declaration
- CategoryTheory.preservesLimits_preadditiveYoneda_obj
- Held-out module
- Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
- Banned modules (itself + downstream)
- 7
- 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 error9.9 s model time
Proof intro κ τ φ; apply CategoryTheory.Limits.preserves_limits_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of_adequate; intros F; apply CategoryTheory.Limits.preserves_limit_of......
What Lean printed (this is all the model sees on repair) 69:51: 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 preservesLimits_preadditiveYoneda_obj (X : C) :
PreservesLimits (preadditiveYoneda.obj X) :=
show PreservesLimits (preadditiveYonedaObj X ⋙ forget₂ _ _) from inferInstance