## Stream: general

### Topic: simp'ing lets in proof

#### Bernd Losert (Feb 09 2022 at 22:46):

MWE:

import data.prod
import order.filter.basic

open filter
open_locale filter

universe u
variables {α β γ : Type*}
variables [has_mul α]

lemma bar (baz : α) (qux : β) : 1 = 1 := begin
let act : α × (α × β) → α × β := λ ⟨a, b, x⟩, (a * b, x),
let mul : α × α → α := function.uncurry (*),
let rlassoc := (equiv.prod_assoc α α β).inv_fun,
have : act = prod.map mul id ∘ rlassoc, begin
funext,
simp,
end,
end


This is clearly not working out since simp doesn't know about the let bound variables. I can use dsimpbefore simp, but that doesn't get me anywhere. Is there a way to make this work, or will I have to extract everything out into defs?

#### Adam Topaz (Feb 09 2022 at 22:49):

try tidy

#### Adam Topaz (Feb 09 2022 at 22:50):

And then tidy? to see what it did, so you can golf it away.

Let me try...

#### Adam Topaz (Feb 09 2022 at 22:51):

hint: ext ⟨_,_,_⟩; refl closes the goal

#### Bernd Losert (Feb 09 2022 at 22:52):

tidy works marvelously.

#### Adam Topaz (Feb 09 2022 at 22:54):

If you really want to unfold your lets, you can use tactic#unfold or, e.g., dsimp [mul].

#### Bernd Losert (Feb 09 2022 at 22:55):

I was using dsimp to unfold the let bound variables, but calling simp afterwards did not have an effect. Is tidy a more powerful simp?

#### Adam Topaz (Feb 09 2022 at 22:55):

You can also replace let with tactic#set using set ... with ...

#### Adam Topaz (Feb 09 2022 at 22:55):

Use tidy? to see what tidy does

#### Adam Topaz (Feb 09 2022 at 22:56):

You were missing an ext and some case splits. It had nothing to do with the lets.

#### Bernd Losert (Feb 09 2022 at 22:57):

Try this: cases a, cases hk, cases hk_right, cases a_snd, refl <-- that's what it says it does. No clue what's going on.

#### Kevin Buzzard (Feb 09 2022 at 22:57):

You can use set ... with h rather than let ... and then throw in h into the simp set (oops, missed that Adam said this already)

#### Bernd Losert (Feb 09 2022 at 22:58):

I'm not sure how set with would work here. Never used it before.

#### Kevin Buzzard (Feb 09 2022 at 23:01):

Type set in tactic mode and then hover over it to see the documentation, or send a message to yourself on Zulip saying tactic#set and click on the link

#### Bernd Losert (Feb 09 2022 at 23:01):

set act : α × (α × β) → α × β := λ ⟨a, b, x⟩, (a * b, x) with <what do I put here?>

#### Kevin Buzzard (Feb 09 2022 at 23:01):

act_def

#### Bernd Losert (Feb 09 2022 at 23:02):

Ah, so it's the name of the equality hypothesis.

Nice.

#### Bernd Losert (Feb 09 2022 at 23:02):

Thanks guys.

Last updated: Dec 20 2023 at 11:08 UTC