Category theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target : (CategoryTheory.MorphismProperty.monomorphisms (Type u)).IsStableUnderCobaseChange := by

Mathlib declaration: CategoryTheory.Types.instIsStableUnderCobaseChangeMonomorphismsType
Held-out module: Mathlib.CategoryTheory.Types.Monomorphisms
Banned modules (itself + downstream): 15
Reference proof premises (reachable / held-out): 3 / 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.00006

Attempts

sample 0 · round 0Wrong tactic2.5 s model time

Proof

intros X Y f g h H₁ H₂
apply CategoryTheory.MorphismProperty.monomorphisms.IsStableUnderCobaseChange'
constructor
apply CategoryTheory.Limits.isMono_of_pullback_of_isMono
apply H₁
apply H₂

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

⊢ (CategoryTheory.MorphismProperty.monomorphisms (Type u)).IsStableUnderCobaseChange

Reference proof

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

instance : (monomorphisms (Type u)).IsStableUnderCobaseChange where
  of_isPushout {X₁ X₂ X₃ X₄ t l r b} sq ht := by
    simp only [monomorphisms.iff] at ht ⊢
    exact Limits.Types.pushoutCocone_inr_mono_of_isColimit sq.flip.isColimit