Getting rid of erw

Stream: general

[Michał Mrugała]

I wrote the following proof (in https://github.com/YaelDillies/Toric/blob/be838b226bb00b97bbde4a75c99d2e07fd56fec3/Toric/GroupScheme/YonedaCommMon.lean)

import Mathlib.CategoryTheory.Monoidal.Yoneda
import Mathlib.CategoryTheory.Monoidal.CommMon_

open CategoryTheory ChosenFiniteProducts MonoidalCategory Mon_Class Opposite

universe w v u

variable {C : Type*} [Category.{v} C] [ChosenFiniteProducts C]
variable (X : C)

class IsCommMon (X : C) [Mon_Class X] where
  mul_comm' : (β_ X X).hom ≫ μ = μ := by aesop_cat

def IsCommMon.ofRepresentableBy (F : Cᵒᵖ ⥤ CommMonCat.{w})
    (α : (F ⋙ forget _).RepresentableBy X) :
    letI := Mon_ClassOfRepresentableBy X (F ⋙ (forget₂ CommMonCat MonCat)) α
    IsCommMon X := by
  letI := Mon_ClassOfRepresentableBy X (F ⋙ (forget₂ CommMonCat MonCat)) α
  refine ⟨?_⟩
  change _ ≫ α.homEquiv.symm _ = α.homEquiv.symm _
  apply α.homEquiv.injective
  simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
  simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]
  simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map]
  erw? [← α.homEquiv_comp]
  sorry

Currently the erw can't be replaced because (F ⋙ forget CommMonCat) and ((F ⋙ forget₂ CommMonCat MonCat) ⋙ forget MonCat) are not syntactically equal. Is there a good way to systematically deal with this?

[Kevin Buzzard]

Can you make this a #mwe ?

[Michał Mrugała]

Changed the original message to a mwe

[Michał Mrugała]

cc @Anne Baanen (@Yaël Dillies's suggestion)

[Kevin Buzzard]

Equality of functors is evil so the principled way to do it would be to write down the natural isomorphism I guess :-/

[Anne Baanen]

Thanks for the CC! I'm not sure if there is currently an easy way to solve this. But I'm away from the computer for a couple hours so can't test it...

[Michał Mrugała]

Kevin Buzzard said:

Equality of functors is evil so the principled way to do it would be to write down the natural isomorphism I guess :-/

They are defeq, but rw isn't smart enough to see through it.

[Kevin Buzzard]

Yes that's what erw does, there are various levels of defeq and erw blasts through more. You used change before, you could just use it again. But you might want to ask how you ended up needing equality of functors in the first place.

[Andrew Yang]

If you just write the whole goal instead of including holes in change then it will work.
(i.e. change (β_ X X).hom ≫ α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X)) = α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X)))

[Michał Mrugała]

Thanks this works! I still don't fully understand this fix though.

[Kevin Buzzard]

change X just checks that the goal is defeq to X and then changes the goal to X and proves this is valid with rfl

[Kevin Buzzard]

So it's a very powerful way to do arbitrary definitional rewrites in the goal.

[Michał Mrugała]

What confuses me in this case is that the part we need to change (forgetful functor vs composition of forgetful functors) is not mentioned explicitly anywhere when using change. I don't know how lean makes the choice.

[Kevin Buzzard]

If X is defeq to Y then f(X) is defeq to f(Y). Is this what's confusing you?

[Kevin Buzzard]

Lean is not making any decisions itself, if the goal is Y then Lean knows Y, and if you write change X then Lean knows X too, so all it has to do is to check that X and Y are defeq.