Algebra · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Epi f] (X : Cᵒᵖ) : CategoryTheory.Epi (f.app X) := by

Mathlib declaration: PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp
Held-out module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
Banned modules (itself + downstream): 8
Reference proof premises (reachable / held-out): 9 / 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.00008

Attempts

sample 0 · round 0Lean 3 syntax13.5 s model time

Proof

intro X
apply CategoryTheory.Epi.of_isEpi
apply CategoryTheory.isEpi_of_compEpi
intros Y g h
rw [CategoryTheory.comp_app]
apply CategoryTheory.isEpi_iff.1
assume k : f.app X ∘ g = h
apply (CategoryTheory.isEpi_iff.2 _ _ _).1
exact k

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
R : CategoryTheory.Functor Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : CategoryTheory.Epi f
X : Cᵒᵖ
⊢ CategoryTheory.Epi (f.app X)
10:11: error: unexpected token ':'; expected command

Reference proof

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

instance [Epi f] (X : Cᵒᵖ) : Epi (f.app X) :=
  inferInstanceAs (Epi ((evaluation R X).map f))