Category theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda := by

Mathlib declaration: CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda
Held-out module: Mathlib.CategoryTheory.Sites.Subcanonical
Banned modules (itself + downstream): 14
Reference proof premises (reachable / held-out): 7 / 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.00006

Attempts

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

Proof

intro J
apply CategoryTheory.Limits.preserves_limits_of_yoneda
apply CategoryTheory.Limits.preserves_limits_of_essential_surjectivity
apply CategoryTheory.Limits.preserves_limits_of_subcanonical
exact J.Subcanonical

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
J : CategoryTheory.GrothendieckTopology C
inst✝ : J.Subcanonical
⊢ CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda

Reference proof

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

instance preservesLimitsOfSize_yoneda : PreservesLimitsOfSize J.yoneda := by
  refine ⟨fun {I} _ ↦ ?_⟩
  have : PreservesLimitsOfShape I (J.yoneda ⋙ sheafToPresheaf J _) :=
    inferInstanceAs <| PreservesLimitsOfShape I CategoryTheory.yoneda
  exact preservesLimitsOfShape_of_reflects_of_preserves _ (sheafToPresheaf J _)