Theorems / mh_cate_a78895

Mathlib held-out

Category theory · easy

Statement, exactly as the model and Lean see it
theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : CategoryTheory.HasSubobjectClassifier (CategoryTheory.Functor Cᵒᵖ (Type w)) := by
Mathlib declaration
CategoryTheory.instHasSubobjectClassifierFunctorOppositeTypeOfEssentiallySmall
Held-out module
Mathlib.CategoryTheory.Topos.Sheaf
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
0 / 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

  1. sample 0 · round 0Lean 3 syntax3.5 s model time
    Proof
    apply_instance
obtain {subobject_classifier} := CategoryTheory.EssentiallySmall.hasSubobjectClassifier_of_essentially_small C
apply (CategoryTheory.Functor.map_subobject_classifier subobject_classifier)
    What Lean printed (this is all the model sees on repair)
    4:3: error: unknown tactic
3:193: error: unsolved goals
C : Type u
inst✝¹ : CategoryTheory.Category.{v, u} C
inst✝ : CategoryTheory.EssentiallySmall.{w, v, u} C
⊢ CategoryTheory.HasSubobjectClassifier (CategoryTheory.Functor Cᵒᵖ (Type w))

Reference proof

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

/-- Presheaf categories on an essentially small domain have a subobject classifier. -/
instance [EssentiallySmall.{w} C] : HasSubobjectClassifier (Cᵒᵖ ⥤ Type w) where
  exists_classifier := ⟨(Presheaf.classifier (SmallModel C)).ofEquivalence
    (Equivalence.congrLeft (E := Type w) (equivSmallModel C).op).symm⟩