how do I get rid of an erw?

Stream: new members

[Emily Riehl]

In PR #31101 the reviewer (@Joël Riou) helped me get rid of an erw in a construction as follows.

The homEquiv_id field below used to read

 homEquiv_id {X} := by
    simp only [Equiv.trans_apply, eHomEquiv_id]
    erw [h]
    rw [← @eId_eq]

but this has been replaced by one line by simpa using h _ (eId V _):

def TransportEnrichment.enrichedOrdinaryCategory
  (e : ∀ v : V, (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v))
  (h : ∀ v : V, ∀ f : 𝟙_ V ⟶ v, e v f = Functor.LaxMonoidal.ε F ≫ F.map f) :
    EnrichedOrdinaryCategory W (TransportEnrichment F C) where
  homEquiv {X Y} := (eHomEquiv V (C := C)).trans (e (Hom (C := C) X Y))
  homEquiv_id {X} := by simpa using h _ (eId V _)
  homEquiv_comp f g := by
    simp only [Equiv.trans_apply]
    erw [h]
    erw [h]
    erw [h]
    simp [← tensorHom_comp_tensorHom, eHomEquiv_comp, eComp_eq,
      tensorHom_def (Functor.LaxMonoidal.ε F), unitors_inv_equal]

A few questions:
(i) How should I understand a proof by simpa using ...?
(ii) How do I discover my own proofs of the form by simpa using ...?
(iii) When I have to use a erw what is the likely culprit?
(iv) What are some tricks to try to get rid of further erws such as in the homEquiv_comp field?

[Emily Riehl]

Also this PR is currently failing because of something to do with the lean version I don't understand. I tried running a lake update and committing but now there's a mismatch with the proofwidgets toolchain. (I don't know what proofwidgets is or how to fix this.)

[Ruben Van de Velde]

Try merging master into your branch. You should not be running lake update inside mathlib

[Kevin Buzzard]

A good first approximation to simpa is that simpa means simp; assumption. More accurately simpa using h means simp; simp at h; exact h.

When you have to use erw you can ask lean what the culprit is with erw?. If this isn't documented when you hover over erw then it should be! [Edit: and indeed it is not!]

[Yaël Dillies]

If you want some jargon to look up, simpa using ... roughly does paramodulation, i.e. unification of metavariables up to equalities (here the equalities are given by the simp lemmas)

[Yaël Dillies]

I read by simpa using h as "And now we are done thanks to h, up to simplification"

[Yaël Dillies]

This is possibly the proof technique I use the most in Lean, and I find it incredibly powerful. I therefore encourage you further in your quest of understanding it.

[Kevin Buzzard]

Oh curses, erw is in core and erw? is in Mathlib so the core people probably are not interested in mentioning erw? in the erw docstring. The correct thing to do here would be to persuade core people to take on erw? but this would probably be a slow process.

[Yaël Dillies]

Unfortunately it is currently unergonomic to create a simpa using ... proof. My usual setting is stuffing more and more stuff in the simpa call below until it works:

simpa? using h

If simp goes too far or loops, I painfully switch to

simp? [stuff] at h
simp? [stuff]
exact h

(I wish a failing simpa? using h reported the lemmas it used instead of failing with no explanation :bangbang:)
If I don't have h yet, I do

simpa using _

and work inside the hole as you usually would, possibly adding another by simpa using ... in there!

[Emily Riehl]

Is there always just a single term after the simpa using because this is the thing you are supposed to exact at the end?

[Eric Wieser]

Yaël Dillies said:

I read by simpa using h as "And now we are done thanks to h, up to simplification"

and defeq; essentially using h can hide a defeq abuse that erw was previously making visible.

[Emily Riehl]

Unfortunately none of these techniques are helping me write the proof. erw? did return something but I can't parse it.

[Emily Riehl]

I think I understand the confusion. Above I have
instance : Category (TransportEnrichment F C) := inferInstanceAs (Category C).

My hypothesis h refers to some structure borne by the type C. My goal involves morphisms in the category structure on the type TransportEnrichment F C.

[Emily Riehl]

So I have h _ (eHomEquiv V (C := C) (f ≫ g)) : (e (X ⟶[V] Z)) ((eHomEquiv V) (f ≫ g)) = Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) while the LHS of my goal is
(e (X ⟶[V] Z)) ((eHomEquiv V) (f ≫ g)) = (λ_ (𝟙_ W)).inv ≫ ((e (X ⟶[V] Y)) ((eHomEquiv V) f) ⊗ₘ (e (Y ⟶[V] Z)) ((eHomEquiv V) g)) ≫ eComp W X Y Z.

rw [h] or even rw [h with all the arguments] still fails while erw [h] succeeds.

[Jakob von Raumer]

There's probably some hidden implicit arguments that use C instead of TransportEnrichment F C or so :thinking: I think in my PR I also needed to add some explicit annotations to get it to work without erw.