learned the difference between two different ways to unwrap an Exists (∃) in Lean: destructuring and choice. this was kind of unintuitive at first but kind people from Lean Zulip helped me see the light. turns out they are actually very different https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreihvgrxikwbj5ilzju6r4qeix6tbb7mmjk7ezcj6evwgffo47kn4zy

another nice lllm learning technique: take something i struggle with, ask it to create a minimal example demonstrating the same issue for me to practice, then after i figure it out, ask it to make a slightly more complex one etc. still requires a lot of direction from my side but genuinely helpful