Lean Kernel Arena / tenet / corner-cases/alg-conv-trans-quot

Checker: tenet · Version: 0.11.3 · 📄 Declaration · 🔗 Source

Test: corner-cases/alg-conv-trans-quot · Expected: 🤷 either · Size: 8.5 KB · Lines: 169 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 132 ms · instructions: 825.8 M · max rss memory: 45.0 MB · run 2026-10-24 16:42:18 UTC

stdout:

FAIL thm trans (0.01s)
    declaration type mismatch for 'trans'
      expected: ∀ {P : Prop}, ∀ {r : P → P → Prop}, ∀ {α : Type}, ∀ (f : P → α), ∀ (h : ∀ (x : P), ∀ (y : P), r x y → Eq.{1} α (f x) (f y)), ∀ (q : Quot.{0} P r), ∀ (z : P), Eq.{1} α (Quot.lift.{0, 1} P r α f h q) (f z)
      inferred: ∀ {P : Prop}, ∀ {r : P → P → Prop}, ∀ {α : Type}, ∀ (f : P → α), ∀ (h : ∀ (x : P), ∀ (y : P), r x y → Eq.{1} α (f x) (f y)), ∀ (q : Quot.{0} P r), P → Eq.{1} α (Quot.lift.{0, 1} P r α f h q) (Quot.lift.{0, 1} P r α f h q)
FAILED: 5 checked, 1 failed, 0 skipped, 8 constants, 0.1s, 4 jobs