Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : (CategoryTheory.MorphismProperty.coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp := by

Mathlib declaration: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp
Held-out module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Banned modules (itself + downstream): 21
Reference proof premises (reachable / held-out): 2 / 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 0Wrong tactic1.3 s model time

Proof

intro h
apply le_rfl

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

5:2: error: Tactic `apply` failed: could not unify the type of `@le_rfl`
  ∀ {α : Type ?u.26} [inst : Preorder α] {a : α}, a ≤ a
with the goal
  ∀ ⦃Y : C⦄ (f : h ⟶ Y),
    (CategoryTheory.MorphismProperty.coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J f → W.rlp.llp f

C : Type u
inst✝⁴ : CategoryTheory.Category.{v, u} C
W : CategoryTheory.MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
h : C
⊢ ∀ ⦃Y : C⦄ (f : h ⟶ Y),
    (CategoryTheory.MorphismProperty.coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J f → W.rlp.llp f

Reference proof

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

lemma transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp :
    (coproducts.{t} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp := by
  simpa using transfiniteCompositionsOfShape_le_llp_rlp (coproducts.{t} W).pushouts J