Theorems / mh_cate_b720d5

Mathlib held-out

Category theory · easy

Statement, exactly as the model and Lean see it
theorem lg_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (R : CategoryTheory.ProjectiveResolution X) : R.cochainComplex.IsKProjective := by
Mathlib declaration
CategoryTheory.ProjectiveResolution.instIsKProjectiveCochainComplex
Held-out module
Mathlib.CategoryTheory.Abelian.Projective.Ext
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
4 / 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.00097

Attempts

  1. sample 0 · round 0Syntax error42.1 s model time
    Proof
    constructor
intro M f
let P := R.cochainComplex
let ι : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let h : ι ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let φ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hφ : φ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ψ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hψ : ψ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let χ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hχ : χ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ε : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hε : ε ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let δ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hδ : δ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let θ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hθ : θ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let μ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hμ : μ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ν : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hν : ν ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ξ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hξ : ξ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ζ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hζ : ζ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let η : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hη : η ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let θ' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hθ' : θ' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ρ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hρ : ρ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let σ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hσ : σ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let τ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hτ : τ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let υ : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hυ : υ ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let φ' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hφ' : φ' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ψ' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hψ' : ψ' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let χ' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hχ' : χ' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ε' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hε' : ε' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let δ' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hδ' : δ' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let θ'' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hθ'' : θ'' ≫ P.underlyingModule.map (R.underlyingModule.map f) = 0 :=
  P.underlyingModule.map (R.underlyingModule.map f).comp_right_zero
let ρ' : P ⟶ P.underlyingModule (R.underlyingModule M) :=
  P.underlyingModule.map (R.underlyingModule.map f)
let hρ' : ρ'
    What Lean printed (this is all the model sees on repair)
    7:16: error: Invalid field `underlyingModule`: The environment does not contain `HomologicalComplex.underlyingModule`, so it is not possible to project the field `underlyingModule` from an expression
  P
of type
  HomologicalComplex C (ComplexShape.up ℤ)
8:6: error: Invalid field `underlyingModule`: The environment does not contain `HomologicalComplex.underlyingModule`, so it is not possible to project the field `underlyingModule` from an expression
  P
of type
  HomologicalComplex C (ComplexShape.up ℤ)
9:12: error: expected token

Reference proof

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

instance : R.cochainComplex.IsKProjective := isKProjective_of_projective _ 0