Mechanics of Proof 1.4.4

Stream: new members

[JK]

I'm stuck on why the following is not a complete proof, and how to complete it (note the only interesting bit is in the final line):

example {u v x y A B : ℝ} (h1 : 0 < A) (h2 : A ≤ 1) (h3 : 1 ≤ B) (h4 : x ≤ B)
    (h5 : y ≤ B) (h6 : 0 ≤ u) (h7 : 0 ≤ v) (h8 : u < A) (h9 : v < A) :
    u * y + v * x + u * v < 3 * A * B :=
  calc
    u * y + v * x + u * v
      ≤ u * B + v * B + u * v := by rel [h5, h4]
    _ ≤ A * B + A * B + A * v := by rel [h8, h9]
    _ ≤ A * B + A * B + 1 * v := by rel [h2]
    _ ≤ A * B + A * B + B * v := by rel [h3]
    _ < A * B + A * B + B * A := by rel [h9]
    _ = 3 * A * B := by ring

[Kenny Lau]

Please use 3 #backticks in a newline before and after the codeblock and include enough imports to make it an #mwe

[Kenny Lau]

what do you mean by not a complete proof? what does the error message say?

[JK]

I don't get an error, but I also don't get checkmarks by the result

[Aaron Liu]

What happens when you change the example to a theorem foo?

[JK]

Still doesn't verify

[JK]

OK, the proof does verify; I didn't get checkmarks because the linter was warning me that h1 was not being used. When I added

set_option linter.unusedVariables false

beforehand, I saw the expected checkmarks

[Kenny Lau]

who would have known we don't need h1 (really??)

[Kenny Lau]

oh, right, we don't need h1 because it's implied by h6 and h8

[Kenny Lau]

(as well as h7 + h9, and the HoTT people can comment on whether these two proofs are the same)