Algebra · hard

Statement, exactly as the model and Lean see it

theorem lg_target : (CategoryTheory.forget₂ RingCat AddCommGrpCat).IsRightAdjoint := by

Mathlib declaration: AlgCat.instIsRightAdjointAddCommGrpCatRingCatForget₂RingHomCarrierAddMonoidHomCarrier
Held-out module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra
Banned modules (itself + downstream): 19
Reference proof premises (reachable / held-out): 8 / 1

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

Attempts

sample 0 · round 0Hallucinated theorem1.7 s model time

Proof

apply CategoryTheory.functor_is_right_adjoint;
  exact (CategoryTheory.isRightAdjoint_of_forget₂_ring_add_comm_group)

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

4:8: error: Unknown identifier `CategoryTheory.functor_is_right_adjoint`
5:4: error: No goals to be solved

Reference proof

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

instance : (forget₂ RingCat.{u} AddCommGrpCat.{u}).IsRightAdjoint := by
  rw [← Functor.isRightAdjoint_comp_iff_right (forget₂ (AlgCat.{u} ℤ) RingCat.{u})]
  have heq : forget₂ (AlgCat.{u} ℤ) _ ⋙ forget₂ (ModuleCat.{u} ℤ) AddCommGrpCat.{u} =
      forget₂ (AlgCat.{u} ℤ) RingCat.{u} ⋙ forget₂ RingCat.{u} AddCommGrpCat.{u} :=
    rfl
  rw [← heq]
  infer_instance