# Zulip Chat Archive

## Stream: new members

### Topic: Help with rw and simp and (x.fst, x.snd)

#### Miguel Negrão (Mar 31 2023 at 11:38):

I'm having trouble getting either rw or simp to substitute (x.fst, x.snd) by x. The goal I have is

```
(fun state => (fun x => pure (x.fst, x.snd)) <=< f state) = f
```

This is where I got from using simp, but simp doesn't appear to be able to go any further. If I was able then substitute (x.fst, x.snd) with x, then I can remove the lambda, and then I have pure <=< f state which should be easy to prove is f state, and then I would get f. But at the moment I'm stuck on rewriting (x.fst, x.snd) to x.

I've proved the following without issue with simp

```
have h : ∀x : Prod α β, (x.fst, x.snd) = x := by simp
```

But if I try to use that in the goal above with rw or simp it fails. For instance below is what happens with `rw [h]`

```
Main.lean:384:18
Tactic state
case cell.mk
bc: Type (u + 1)
m: Type (u + 1) → Type (u + 1)
inst✝¹: Monad m
inst✝: LawfulMonad m
h: ∀ {α β : Type} (x : α × β), (x.fst, x.snd) = x
s✝: Type u
s: s✝
f: s✝ → b → m (c × s✝)
⊢ (fun state => (fun x => pure (x.fst, x.snd)) <=< f state) = f
Messages (1)
Main.lean:384:16
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(?x.fst, ?x.snd)
case cell.mk
m: Type (u + 1) → Type (u + 1)
h: ∀ {α β : Type} (x : α × β), (x.fst, x.snd) = x
s: s✝
f: s✝ → b → m (c × s✝)
⊢ (fun state => (fun x => pure (x.fst, x.snd)) <=< f state) = f
```

The type of x in fun x is `c × s✝`

so it should be a normal Prod.

I think I'm probably missing something...

#### Miguel Negrão (Mar 31 2023 at 11:46):

full code here.

#### Jireh Loreaux (Mar 31 2023 at 12:40):

`rw`

can't see under the binder, try using `simp_rw`

. Or just forget the `have h`

and instead of `rw [h]`

you can just use `simp only [Prod.mk.eta]`

#### Miguel Negrão (Mar 31 2023 at 13:01):

simp_rw is from Mathlib, but if I import Mahtlib suddenly simp doesn't get hung up in the same place, it finishes the whole goal in one go. So it appears with Mathlib simp becomes more powerful !

```
theorem cell_id_comp {m : Type (u+1) -> Type (u+1)} [Monad m] [LawfulMonad m] (cell : Cell m b c) : cellCatCompose cellCatId cell = cell := by
cases cell with
| arrm f => simp [cellCatCompose, cellCatId, Bind.kleisliLeft]
| cell p => simp [cellCatCompose, cellCatId, Bind.kleisliLeft]
```

Thanks for letting me know about simp_rw, it might come in handy in another situation where I need to do substitutions under binders.

#### Jireh Loreaux (Mar 31 2023 at 13:14):

You don't need `simp_rw`

, `simp only [h]`

should work (or whatever lemma `simp`

calls to solve your `have h`

). This should avoid you needing to make mathlib a dependency if you would prefer to avoid it.

It's not surprising that `simp`

becomes more powerful with mathlib though: mathlib adds lots of `@[simp]`

tagged lemmas.

#### Miguel Negrão (Mar 31 2023 at 14:20):

Without `import Mathlib`

`simp only [h]`

does not do anything to the goal...

#### Kevin Buzzard (Mar 31 2023 at 14:29):

You can use `squeeze_simp`

to find out which lemmas are being used.

#### Jireh Loreaux (Mar 31 2023 at 14:30):

Kevin, this is Lean 4. I think it's `simp?`

now.

#### Miguel Negrão (Mar 31 2023 at 14:33):

There is some subtle issue with my `h`

, actually without using Mathlib `simp only [Prod.eta]`

works.

#### Jireh Loreaux (Mar 31 2023 at 14:34):

The issue with your `h`

is that you gave it for `α β : Type`

not `α β : Type _`

.

#### Jireh Loreaux (Mar 31 2023 at 14:35):

But docs4#Prod.eta is the right thing to use

#### Miguel Negrão (Mar 31 2023 at 14:41):

Ok, so after `simp only [Prod.eta]`

, simp doesn't do the eta reduction in

```
(p.fst, fun state => (fun x => pure x) <=< Prod.snd p state) = p
```

I mean changing `(fun x => pure x) `

to `pure`

. Should I pass an explicit eta reduction theorem to simp ? Btw, ading `Prod.eta`

to the list of theorems I'm passing to simp also works, I don't need to use `simp only`

apparently.

#### Miguel Negrão (Mar 31 2023 at 14:42):

But ok, the important thing here is that I got stuck because my version of Prod.eta didn't have the right universes.

#### Miguel Negrão (Mar 31 2023 at 14:44):

But even with the following version of h it doesn't work with simp:

```
have h {α : Type _} {β : Type _} (p : α × β) : (p.1, p.2) = p := rfl
```

#### Miguel Negrão (Mar 31 2023 at 14:44):

while `Prod.eta`

does...

#### Miguel Negrão (Mar 31 2023 at 14:47):

Similarly the following also doesn't manage to get simp to do the eta reduction...

```
have h2 {α : Type _} {β : Type _} (f : α → β) : (λ x ↦ f x) = f := rfl
```

I'm a bit lost here...

#### Miguel Negrão (Mar 31 2023 at 15:05):

Jireh Loreaux disse:

Kevin, this is Lean 4. I think it's

`simp?`

now.

Right, in lean 4 it's simp?. With that I can see what else I needed to add to make it work only in Lean 4 without Mathlib:

```
simp only [cellCatCompose, cellCatId, Bind.kleisliLeft, map_pure, Prod.eta, bind_pure]
```

Last updated: Dec 20 2023 at 11:08 UTC