Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (h : sq.IsPullback) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback := by

Mathlib declaration: CategoryTheory.Square.IsPullback.map
Held-out module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Banned modules (itself + downstream): 6
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.

Verified3 model calls · 2 Lean checks · $0.00060

Retrieved lemmas

1. CategoryTheory.Square.IsPullback.mono_f₁₂
2. CategoryTheory.IsPullback.preservesLimit_cospan_iff
3. CategoryTheory.IsPullback.map
4. CategoryTheory.Functor.map_isPullback
5. CategoryTheory.Square.IsPullback.mk
6. CategoryTheory.Square.IsPullback.mono_f₁₃
7. CategoryTheory.Square.isPullback_iff
8. CategoryTheory.Square.IsPullback.flip

Plan

To prove the theorem `lg_target`, we need to show that if a square is a pullback in category `C` and a functor `F` preserves the limit of the corresponding cospan, then the image of the square under `F` is a pullback in category `D`. The key idea is to use the fact that `F` preserves limits. Specifically, since the original square is a pullback (i.e., its pullback cone is a limit), and `F` preserves this limit (as given by the assumption `[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F]`), then the image of the pullback cone under `F` is also a limit in `D`. This implies that the image of the square under `F` is a pullback in `D`, as required. In more detail, the square being a pullback means its pullback cone is a limit. The assumption that `F` preserves this limit ensures that the image of the cone under `F` is a limit in `D`, which is precisely what it means for the mapped square to be a pullback. Thus, the conclusion follows directly from the preservation of limits by `F`.

Attempts

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

Proof

intro hF
apply CategoryTheory.IsPullback.map F h
exact hF

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

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

C : Type u
inst✝² : CategoryTheory.Category.{v, u} C
D : Type u'
inst✝¹ : CategoryTheory.Category.{v', u'} D
sq : CategoryTheory.Square C
h : sq.IsPullback
F : CategoryTheory.Functor C D
inst✝ : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F
⊢ (sq.map F).IsPullback

sample 0 · round 1Verified1.6 s model time
Proof
```
apply CategoryTheory.IsPullback.map F h
```

Verified proof

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (h : sq.IsPullback) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback := by
  apply CategoryTheory.IsPullback.map F h

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

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

lemma IsPullback.map (h : sq.IsPullback) (F : C ⥤ D) [PreservesLimit (cospan sq.f₂₄ sq.f₃₄) F] :
    (sq.map F).IsPullback :=
  Square.IsPullback.mk _ (isLimitPullbackConeMapOfIsLimit F sq.fac h.isLimit)