proof terms for "use" and "cases" tactics

Stream: new members

[Jia Ming Lim]

Hello! I'm halfway through chapter 3 of mathematics_in_lean and was wondering how prove something like the example below in proof term mode. It is straightforward with tactics but I don't think the tutorials teaches you the proof term alternatives for these two tactics.

example {x : ℝ} (h : ∃a, x < a) : ∃b, x < b * 2 :=
begin
    cases h with a h,
    use a / 2,
    linarith,
end

[Sebastien Gouezel]

example {x : ℝ} (h : ∃a, x < a) : ∃b, x < b * 2 :=
let ⟨a, ha⟩ := h in ⟨a/2, by linarith⟩

[Jia Ming Lim]

Thank you so much!

[Johan Commelin]

Jia Ming Lim said:

but I don't think the tutorials teaches you the proof term alternatives for these two tactics.

Note that this is by design.

[Jia Ming Lim]

ahh right, thanks

[Kevin Buzzard]

There's no term mode equivalent for linarith, it does hard work in general. You might well be able to find the lemma saying that if d isn't 0 then a/d*d=a using library_search and then you could use that -- but the whole linarith philosophy is that this gets pretty boring very quickly

[Jia Ming Lim]

yeah hahah it's fun to search for the lemmas at first but then linarith starts to look too good to avoid

[Bryan Gin-ge Chen]

For cases, 7.6 of #tpil gives a decent explanation of what's going on. (If you find yourself wondering how things work under the hood, TPIL is a good place to start looking).

[Jia Ming Lim]

Coool now I have something to look forward to in that book. Thank you!