Category theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) : Nonempty (CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)) ↔ CategoryTheory.Presieve.IsSheafFor F E.presieve₀ := by

Mathlib declaration: CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff
Held-out module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Banned modules (itself + downstream): 16
Reference proof premises (reachable / held-out): 4 / 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 tactic5.7 s model time

Proof

intro h
split
· intro hlim
  haveI : IsLimit (E.toPreOneHypercover.multifork F) := hlim
  haveI : IsSheafFor F E.presieve₀ := CategoryTheory.Presieve.isSheafForOfIsLimit hlim
  exact this

· intro hsheaf
  haveI : IsSheafFor F E.presieve₀ := hsheaf
  haveI : IsLimit (E.toPreOneHypercover.multifork F) := CategoryTheory.Presieve.isLimitOfIsSheafFor hsheaf
  exact this

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_1
inst✝¹ : CategoryTheory.Category.{v_1, u_1} C
S : C
E : CategoryTheory.PreZeroHypercover S
inst✝ : E.HasPullbacks
F : CategoryTheory.Functor Cᵒᵖ (Type u_2)
⊢ Nonempty (CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)) ↔
    CategoryTheory.Presieve.IsSheafFor F E.presieve₀

Reference proof

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

lemma isLimit_toPreOneHypercover_type_iff (E : PreZeroHypercover.{w} S) [E.HasPullbacks]
    (F : Cᵒᵖ ⥤ Type*) :
    Nonempty (IsLimit <| E.toPreOneHypercover.multifork F) ↔ E.presieve₀.IsSheafFor F := by
  rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsEquivOfHasPullbacks F).symm.bijective]
  rfl