Theorems / mh_alge_740845

Mathlib held-out

Algebra · easy

Statement, exactly as the model and Lean see it
theorem lg_target {R : Type u} [Ring R] : CategoryTheory.Limits.HasFiniteBiproducts (ModuleCat R) := by
Mathlib declaration
ModuleCat.instHasFiniteBiproducts
Held-out module
Mathlib.Algebra.Category.ModuleCat.Biproducts
Banned modules (itself + downstream)
10
Reference proof premises (reachable / held-out)
2 / 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.00011

Attempts

  1. sample 0 · round 0Wrong namespace3.8 s model time
    Proof
    constructor
intro n
induction' n with d hd
case zero => exact ZeroObject.instance
case succ d =>
  obtain ⟨X, Y, i, p, iso⟩ := HasFiniteBiproducts.of_binary_biproduct (hd d)
  let Z := X ⊕ Y
  let i' : Z ⟶ Z := CategoryTheory.Limits.biprod.inl
  let p' : Z ⟶ Z := CategoryTheory.Limits.biprod.inr
  let iso' := CategoryTheory.Limits.biprod.ι₁_iso
  exact { biprod := Z, inl := i', inr := p', ι₁_iso := iso', ι₂_iso := iso' }
    What Lean printed (this is all the model sees on repair)
    7:21: error: Unknown identifier `ZeroObject.instance`
9:32: error: Unknown identifier `HasFiniteBiproducts.of_binary_biproduct`
9:11: error: Tactic `rcases` failed: `x✝ : ?m.22` is not an inductive datatype

Reference proof

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

instance : HasFiniteBiproducts (ModuleCat.{v} R) :=
  HasFiniteBiproducts.of_hasFiniteProducts