LFTCM2020 category theory

Stream: general

[Sebastien Gouezel]

I had fixed LFTCM2020 yesterday, but it is again broken today :-( But this is because of category theory, where a nonterminal simp is not doing anything anymore, in

def functor.preadditive.preserves_biproducts (F : C ⥤ D) (P : F.preadditive) (X Y : C) :
  F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y :=
-- sorry
{ hom := biprod.lift (F.map biprod.fst) (F.map biprod.snd),
  inv := biprod.desc (F.map biprod.inl) (F.map biprod.inr),
  hom_inv_id' := begin simp, simp_rw [←F.map_comp, ←P.map_add'], simp, end,
  inv_hom_id' := begin ext; simp; simp_rw [←F.map_comp]; simp [P.map_zero'], end, }
-- This proof is not yet "mathlib-ready", because it uses "nonterminal" `simp`s.
-- Can you fix it?
-- sorry

(the first simp in hom_inv_id' does not simplify). @Scott Morrison , could you have a look?

[Jireh Loreaux]

I think this is just evidence that non-terminal simps are so evil they can't even be discussed in teaching materials. :rofl:

[Sebastien Gouezel]

And my answer to the question can you fix it? is clearly no, I can't :grinning_face_with_smiling_eyes:

[Scott Morrison]

Sorry, I can't reproduce. In lftcm2020, that proof was sorried out in master, and when I restore the proof given above it compiles fine.

[Scott Morrison]

I guess I can do the simps anyway.

[Scott Morrison]

I restored the proof with the non-terminal simps expanded.

[Sebastien Gouezel]

Thanks. I guess you didn't reproduce because you didn't try to update mathlib: the proof used to build fine with mathlib from two days ago, but not with yesterday's.

[Sebastien Gouezel]

But with the explicit lemmas you provided and the amazing https://mathlib-changelog.org/, I was able to fix it myself.