Theorems / mh_cate_7a05c0

Mathlib held-out

Category theory · hard

Statement, exactly as the model and Lean see it
theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [CategoryTheory.IsCardinalAccessibleCategory C κ] (X : C) : CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow (CategoryTheory.isCardinalPresentable C κ).ι X) κ := by
Mathlib declaration
CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι
Held-out module
Mathlib.CategoryTheory.Presentable.Dense
Banned modules (itself + downstream)
4
Reference proof premises (reachable / held-out)
6 / 2

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.00036

Attempts

  1. sample 0 · round 0Syntax error11.5 s model time
    Proof
    intro κ'
obtain ⟨κ'', h⟩ := CategoryTheory.isCardinalPresentable.exists_cardinal_le κ
have := CategoryTheory.IsCardinalAccessibleCategory.isCardinalFiltered_iff _ _ _
apply this
constructor
· exact h
· intro f
  haveI := CategoryTheory.IsCardinalAccessibleCategory.isCardinalAccessible C κ
  haveI := CategoryTheory.isCardinalPresentable.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresentable.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresentable.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresentable.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresentable.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresentable.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinalPresented C κ
  haveI := CategoryTheory.isCardinalPresented.isCardinal......
    What Lean printed (this is all the model sees on repair)
    44: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 [IsCardinalAccessibleCategory C κ] (X : C) :
    IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C κ).ι X) κ := by
  obtain ⟨J, _, _, ⟨p⟩⟩ :=
    (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X
  exact IsCardinalFiltered.of_final p.toCostructuredArrow κ