Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] {A B I Z : C} (i : A ⟶ B) [CategoryTheory.Mono i] [CategoryTheory.Injective I] (p : I ⟶ Z) (hZ : CategoryTheory.Limits.IsZero Z) : CategoryTheory.HasLiftingProperty i p := by

Mathlib declaration: CategoryTheory.Injective.hasLiftingProperty_of_isZero
Held-out module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
Banned modules (itself + downstream): 15
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.00007

Attempts

sample 0 · round 0Syntax error3.4 s model time

Proof

constructor
intro f h
rcases hZ (p ≫ f) with ⟨g, hg⟩
use [g, hg]
exact (CategoryTheory.Mono.map_injective i).mp (h.trans (i ≫ p ≫ f))

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

6:15: error: expected token
6:9: error: Function expected at
  hZ
but this term has type
  CategoryTheory.Limits.IsZero Z

Note: Expected a function because this term is being applied to the argument
  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)

Reference proof

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

lemma hasLiftingProperty_of_isZero
    {A B I Z : C} (i : A ⟶ B) [Mono i] [Injective I] (p : I ⟶ Z) (hZ : IsZero Z) :
    HasLiftingProperty i p where
  sq_hasLift {f g} sq := ⟨⟨{
    l := Injective.factorThru f i
    fac_right := hZ.eq_of_tgt _ _ }⟩⟩