Mechanics of Proof 1.3.11 exercise 15

Stream: lean4

[Alex Sweeney]

I'm working on exercise 15 here.
https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#id29

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  sorry

Here's where I got stuck

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  calc
    y = 0 + y := by ring
    _ = (2 * x - y * x) + y := by rw [h2]
    _ = (x + 3) * (2 - y) - 6 + 4 * y := by ring
    _ = 5 * (2 - y) - 6 + 4 * y := by rw [h1]
    _ = 4 - y := by ring -- I get stuck here

I don't know how to approach this problem. I thought maybe y = (2 * x - y * x) / -x + 2 := by ring would be a good start but ring apparently can't deal with ⊢ y = 2 + (x * y * x⁻¹ - x * x⁻¹ * 2). I'm also trying to stay away from anything other than calc, rw, and ring because only these were mentioned in the book so far. I had to use linarith a few times but I can't even get that to work here.

[Ruben Van de Velde]

You seem to have a correct proof that $y=4-y$, but that isn't what you set out to prove

[Ruben Van de Velde]

ring won't help you because it doesn't do division

[Ruben Van de Velde]

Did you have a proof of example 1.3.8?

[Utensil Song]

Hint: 0 / 2 at the beginning is all you need. (I've checked locally, but I can't spoil for your exercise.)

[Utensil Song]

However, there seems to be a Lean bug handling the indentation of calc:

import Mathlib

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  have h3 : y = 4 - y := by calc
      y = 0 + y := by ring
      _ = (2 * x - y * x) + y := by rw [h2]
      _ = (x + 3) * (2 - y) - 6 + 4 * y := by ring
      _ = 5 * (2 - y) - 6 + 4 * y := by rw [h1]
      _ = 4 - y := by ring
  /-
  x y : ℝ
  h1 : x + 3 = 5
  h2 : 2 * x - y * x = 0
  ⊢ y = 2
  -/
  done

No matter how I move the cursor on that line, I can't see h3 in inforview.

[Utensil Song]

Furthermore, if I put some rw on that line, Lean complains unknown identifier 'rw', and if I put linarith there, Lean complains

function expected at
  linarith
term has type
  Lean.ParserDescr

This can be reproduced both locally in VSCode and on live.lean-lang.org .

[Ruben Van de Velde]

No, the problem is that there's no by on the line that starts with example, so you're actually using term mode have

[Ruben Van de Velde]

Took me a minute to notice that :sweat_smile:

[Utensil Song]

Aha, sorry, I modified the code by just adding have before calc, without noticing there is no by before calc.

[Alex Sweeney]

Utensil Song said:

Hint: 0 / 2 at the beginning is all you need. (I've checked locally, but I can't spoil for your exercise.)

Thanks for the hint! But how do I start with 0 / 2? Was that a typo? Seems like I can only start with y = (2 * y) / 2 but I'm still having trouble cancelling out that y on the RHS. Could you give another small hint?

[Alex Sweeney]

Ruben Van de Velde said:

Did you have a proof of example 1.3.8?

Yes I do, but they still seem like different problems and I can't solve it the same way because there is no x * y term
1.3.8:

example {x y : ℝ} (h1 : x + y = 4) (h2 : 5 * x - 3 * y = 4) : x = 2 :=
  calc
    x = (3 * (x + y) + (5 * x - 3 * y)) / 8 := by ring
    _ = (3 * 4 + 4) / 8 := by rw [h1, h2]
    _ = 2 := by ring

[Utensil Song]

You can start with:

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  calc
    y = 0 / 2 + y := by ring

and you'll end up with _ = 2 with no y on the RHS.

[Alex Sweeney]

Thanks I got it!
I probably spent an hour on this over the last 2 days. How did you know to start with 0 / 2 + y? Intuition, trial and error, working backwards?

I love how many exercises there are in this book and I haven't really had much trouble until this one.

[Utensil Song]

I don't know if this is the intended way to do it. But this is the natural way to make y on RHS go away, the downside is that it implicitly used the fact that x=2. And I just find out starting wih 0 / x + y also works.