Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd := by

Mathlib declaration: CategoryTheory.mono_iff_isIso_snd
Held-out module: Mathlib.CategoryTheory.Limits.EpiMono
Banned modules (itself + downstream): 10
Reference proof premises (reachable / held-out): 0 / 1

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.00011

Attempts

sample 0 · round 0Wrong tactic3.3 s model time

Proof

intro h_mono
split
· intro h_iso
  have h : CategoryTheory.IsIso c.snd := h_iso
  have h' : CategoryTheory.IsIso c.fst := by
    rw [CategoryTheory.Limits.PullbackCone.π_app]
    exact (h_iso.trans (CategoryTheory.Limits.PullbackCone.π_app _ _)).symm
  exact CategoryTheory.Mono.of_isIso h'
· intro h_mono
  have h : CategoryTheory.IsIso c.snd := by
    apply CategoryTheory.IsIso.of_injective
    rw [CategoryTheory.Limits.PullbackCone.π_app]
    exact h_mono
  exact h

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_1
inst✝ : CategoryTheory.Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CategoryTheory.Limits.PullbackCone f f
hc : CategoryTheory.Limits.IsLimit c
⊢ CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd

Reference proof

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

lemma mono_iff_isIso_snd (hc : IsLimit c) : Mono f ↔ IsIso c.snd :=
  mono_iff_isIso_fst (PullbackCone.flipIsLimit hc)