Commit 2023-06-21 03:58 aa7f5e19

feat: lift_lets tactic (#3893) This tactic was suggested by @eric-wieser in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Pulling.20.60let.60s.20to.20the.20outside.20of.20a.20statement/near/315581119 The tactic tries to take all lets in an expression and lift them out as far as possible. For example, if the goal is (let x := 1; x) = 1 then lift_lets turns the goal into let x := 1; x = 1. This then allows the user to do intro x to create a local let binding.