Theorems / mh_cate_63c919

Mathlib held-out

Category theory · hard

Statement, exactly as the model and Lean see it
theorem lg_target {X : Type u} {κ : Cardinal.{u}} (hX : HasCardinalLT X κ) [Fact κ.IsRegular] : CategoryTheory.IsCardinalPresentable X κ := by
Mathlib declaration
HasCardinalLT.isCardinalPresentable
Held-out module
Mathlib.CategoryTheory.Presentable.Type
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
12 / 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.00097

Attempts

  1. sample 0 · round 0Lean 3 syntax47.6 s model time
    Proof
    ```lean
intro hX
apply CategoryTheory.IsCardinalPresentable.ofLimitPreservingOfHasCardinalLT
· exact hX
· intro F
  obtain ⟨I, f, lim⟩ := CategoryTheory.Limits.hasLimit (CategoryTheory.Limits.limitFunctor _)
  have : ∀ (i : I), Cardinal.mk (f i) < κ := by
    intro i
    apply hX
    exact (CategoryTheory.Limits.isLimitLimitFunctor _ _).limitIsLimit
  let χ : ℕ → Cardinal := λ n, Cardinal.mk (f (I.natCast n))
  let χ' : ℕ → Cardinal := λ n, χ n
  have : ∃ n : ℕ, χ' n ≥ κ := by
    rw [Cardinal.mk_injective]
    exact (κ.IsRegular.cardinal_regular_cardinal_lt_ω).lt_omega_iff_exists
  obtain ⟨n, h⟩ := this
  let χ'' : ℕ → Cardinal := λ m, if m < n then χ m else κ
  let χ''' : ℕ → Cardinal := λ m, χ'' m
  let χ'''' : ℕ → Cardinal := λ m, χ''' m
  let χ''''' : ℕ → Cardinal := λ m, χ'''' m
  let χ'''''' : ℕ → Cardinal := λ m, χ''''' m
  let χ''''''' : ℕ → Cardinal := λ m, χ'''''' m
  let χ'''''''' : ℕ → Cardinal := λ m, χ''''''' m
  let χ''''''''' : ℕ → Cardinal := λ m, χ'''''''' m
  let χ'''''''''' : ℕ → Cardinal := λ m, χ''''''''' m
  let χ''''''''''' : ℕ → Cardinal := λ m, χ'''''''''' m
  let χ'''''''''''' : ℕ → Cardinal := λ m, χ''''''''''' m
  let χ''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''' m
  let χ'''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''' m
  let χ''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''' m
  let χ'''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''' m
  let χ''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''' m
  let χ'''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''' m
  let χ''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''' m
  let χ'''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''' m
  let χ''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''' m
  let χ'''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''' m
  let χ''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''' m
  let χ'''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''''''''''''' m
  let χ'''''''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ''''''''''''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''''''''''''''''''''''' : ℕ → Cardinal := λ m, χ'''''''''''''''''''''''''''''''''''''''''''''' m
  let χ''''''''''''''''''''''''''
    What Lean printed (this is all the model sees on repair)
    3:140: error: unsolved goals
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
⊢ CategoryTheory.IsCardinalPresentable X κ
4:2: error: unexpected token '`'; expected command

Reference proof

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

lemma isCardinalPresentable (hX : HasCardinalLT X κ) [Fact κ.IsRegular] :
    IsCardinalPresentable X κ where
  preservesColimitOfShape J _ _ :=
    ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨by
      have := isFiltered_of_isCardinalFiltered J κ
      refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_)
      · dsimp at f
        choose j g hg using fun x ↦ Types.jointly_surjective_of_isColimit hc (f x)
        refine ⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩
        dsimp
        ext x
        dsimp at j g hg x ⊢
        rw [← hg]
        exact congr_hom (c.w (IsCardinalFiltered.toMax j hX x)).symm (g x)
      · choose k a hk using fun x ↦
          (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (congr_hom h x)
        dsimp at f g h k a hk ⊢
        replace hk : ∀ x, F.map (a x) (f x) = F.map (a x) (g x) := by assumption
        obtain ⟨l, b, c, hl⟩ : ∃ (l : J) (c : j ⟶ l) (b : ∀ x, k x ⟶ l),
            ∀ x, a x ≫ b x = c := by
          let φ (x : X) : j ⟶ IsCardinalFiltered.max k hX :=
            a x ≫ IsCardinalFiltered.toMax k hX x
          exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩
        refine ⟨l, b, by ext x; simp [← hl x, hk]⟩⟩⟩⟩