Theorems / novel_cat_04

Authored

Category theory · hard

Statement, exactly as the model and Lean see it
open CategoryTheory in
theorem lg_target {C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] : Mono (f ≫ g) := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
2

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified0 model calls · 12 Lean checks · $0.00000

Attempts

  1. attempt 1Wrong tactic
    Proof
    rfl
    What Lean printed (this is all the model sees on repair)
    5:2: error: Tactic `rfl` failed: The left-hand side
  Z
is not definitionally equal to the right-hand side
  f ≫ g

C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
⊢ Mono (f ≫ g)
  2. attempt 2Other
    Proof
    decide
    What Lean printed (this is all the model sees on repair)
    5:2: error: Expected type must not contain free variables
  Mono (f ≫ g)

Hint: Use the `+revert` option to automatically clean up and revert free variables
  3. attempt 3Valid but mathematically wrong
    Proof
    norm_num
    What Lean printed (this is all the model sees on repair)
    4:115: error: unsolved goals
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
⊢ Mono f
  4. attempt 4Valid but mathematically wrong
    Proof
    simp
    What Lean printed (this is all the model sees on repair)
    4:115: error: unsolved goals
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
⊢ Mono f
  5. attempt 5Wrong tactic
    Proof
    ring
    What Lean printed (this is all the model sees on repair)
    5:2: error: `ring_nf` made no progress on the goal
  6. attempt 6Wrong tactic
    Proof
    linarith
    What Lean printed (this is all the model sees on repair)
    5:2: error: linarith failed to find a contradiction
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
⊢ False
failed
  7. attempt 7Wrong tactic
    Proof
    nlinarith
    What Lean printed (this is all the model sees on repair)
    5:2: error: linarith failed to find a contradiction
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
⊢ False
failed
  8. attempt 8Wrong tactic
    Proof
    positivity
    What Lean printed (this is all the model sees on repair)
    5:2: error: not a positivity goal
  9. attempt 9Wrong tactic
    Proof
    omega
    What Lean printed (this is all the model sees on repair)
    5:2: error: omega could not prove the goal:
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
  10. attempt 10Wrong tactic
    Proof
    field_simp
    What Lean printed (this is all the model sees on repair)
    5:2: error: `field_simp` made no progress on the goal
  11. attempt 11Wrong tactic
    Proof
    tauto
    What Lean printed (this is all the model sees on repair)
    5:2: error: Tactic `tauto` failed

C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
⊢ Mono (f ≫ g)
  12. attempt 12Verified
    Proof
    simp_all

Verified proof

open CategoryTheory in
theorem lg_target {C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] : Mono (f ≫ g) := by
  simp_all

Axioms used: propext

Reference proof

The proof we wrote and certified before any model ran.

constructor
intro W a b h
simp only [← Category.assoc] at h
exact (cancel_mono f).mp ((cancel_mono g).mp h)