Category theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target (w : CategoryTheory.uliftFunctor.{u, v}.EssSurj) : UnivLE.{max u v, v} := by

Mathlib declaration: UnivLE.ofEssSurj
Held-out module: Mathlib.CategoryTheory.UnivLE
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 1 / 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.00004

Attempts

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

Proof

intros w
apply (UnivLE.of_ess_surj w)

What Lean printed (this is all the model sees on repair)

4:2: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

w : CategoryTheory.uliftFunctor.{u, v}.EssSurj
⊢ UnivLE.{max u v, v}

Reference proof

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

theorem UnivLE.ofEssSurj (w : (uliftFunctor.{u, v} : Type v ⥤ Type max u v).EssSurj) :
    UnivLE.{max u v, v} where
  small α := by
    obtain ⟨a', m⟩ := w.mem_essImage α
    obtain ⟨m'⟩ := m
    exact ⟨a', ⟨(Iso.toEquiv m').symm.trans Equiv.ulift⟩⟩