simp'ing lets in proof

Stream: general

[Bernd Losert]

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]

try tidy

[Adam Topaz]

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

[Bernd Losert]

Let me try...

[Adam Topaz]

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

[Bernd Losert]

tidy works marvelously.

[Adam Topaz]

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

[Bernd Losert]

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]

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

[Adam Topaz]

Use tidy? to see what tidy does

[Adam Topaz]

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

[Bernd Losert]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

act_def

[Bernd Losert]

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

[Bernd Losert]

Nice.

[Bernd Losert]

Thanks guys.