# Zulip Chat Archive

## Stream: new members

### Topic: Help with proof syntax

#### Mike (Oct 19 2023 at 14:04):

Trying to work out my own proof from an exercise in *Mathematics in Lean*

```
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import MIL.Common
variable (a b c d e : ℝ)
open Real
example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h₁ : 0 ≤ a^2 - 2 * a * b + b^2
calc
a^2 - 2*a*b + b^2 = (a-b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
have h₂ : a*b ≤ (a^2 + b^2)/2
calc
a*b ≤ (a^2 + b^2)/2 := by linarith
have h₃ : -a*b ≤ (a^2 + b^2)/2
calc
```

The book recommends using `abs_le'.mpr`

, so I wanted to apply that with `h₂`

and `h₃`

.

Could someone show me how to finish the proof without using `constructor`

(is it even possible)? The book's solution uses it:

```
theorem fact1 : a * b * 2 ≤ a ^ 2 + b ^ 2 := by
have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
calc
a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
linarith
theorem fact2 : -(a * b) * 2 ≤ a ^ 2 + b ^ 2 := by
have h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
calc
a ^ 2 + 2 * a * b + b ^ 2 = (a + b) ^ 2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
linarith
example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h : (0 : ℝ) < 2 := by norm_num
apply abs_le'.mpr
constructor
· rw [le_div_iff h]
apply fact1
rw [le_div_iff h]
apply fact2
```

Edit: This works. It's mostly based on the book's solution

```
example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h₁ : 0 ≤ a^2 -2*a*b + b^2
calc
a^2 -2*a*b + b^2 = (a-b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
have h₂ : 0 ≤ a^2 + 2*a*b + b^2
calc
a^2 + 2*a*b + b^2 = (a+b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
have g₁ : a*b ≤ (a ^ 2 + b ^ 2)/2 := by
rw [le_div_iff]
linarith
norm_num
have g₂ : -(a * b) ≤ (a^2 + b^2)/2 := by
rw [le_div_iff]
linarith
norm_num
apply abs_le'.mpr
constructor
apply g₁
apply g₂
```

It seems like `constructor`

is necessary because `abs_le'.mpr`

has an `∧`

that has to be satisfied, and I can't figure out how to use `case`

here (maybe because it's not possible).

#### Ruben Van de Velde (Oct 19 2023 at 15:47):

You could cheat with

```
apply abs_le'.mpr ⟨?_, ?_⟩
```

but I'm not sure what makes you want to avoid `constructor`

#### Alex J. Best (Oct 19 2023 at 15:54):

You can use `show_term constructor`

to see what a tactic did, in this case `constructor`

is equivalent to `refine { left := ?left, right := ?right }`

, so you could use that instead

#### Mike (Oct 19 2023 at 16:33):

@Ruben Van de Velde @Alex J. Best The pdf *Mathematics in Lean* didn't introduce `constructor`

, so I have no idea what it's doing. I was just hoping that there was a way to solve it that just used `apply`

, `linarith`

, and `have`

(even if it's a clunky proof).

Right now I'm stuck on an even simpler problem.

```
example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h₁ : 0 ≤ 1/2*a^2 -a*b + 1/2*b^2
calc
1/2*a^2 -a*b + 1/2*b^2 = ((a-b)^2)/2 := by ring
_ ≥ 0 := by
rw [le_div_iff norm_num]
have h₂ : a*b ≤ (a ^ 2 + b ^ 2) / 2
calc
a*b ≤ (a ^ 2 + b ^ 2) / 2 := by linarith [h₁]
have h₃ : 0 ≤ 1/2*a^2 + a*b + 1/2*b^2
calc -- This is underlined in red, and there's an error message: expected '|' Lean 4
1/2*a^2 + a*b + 1/2*b^2 = (a+b)^2/2 := by ring
_ ≥ 0 := by
rw [le_div_iff norm_num]
have h₄ : -a*b ≤ (a ^ 2 + b ^ 2) / 2
calc
a*b ≤ (a ^ 2 + b ^ 2) / 2 := by linarith [h₃]
apply
abs_le'.mpr h₂ h₄
```

It looks like the proof of `h₃`

doesn't work, but Lean Infoview doesn't show any error messages.

#### Kyle Miller (Oct 19 2023 at 20:26):

@Mike It looks like `constructor`

is introduced in the next chapter: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html#index-18

#### Patrick Massot (Oct 19 2023 at 22:41):

If the solution uses a tactic that was not explained at this stage then it's a clear bug. Could you open a GitHub issue about it?

#### Kyle Miller (Oct 20 2023 at 04:09):

Sure: https://github.com/avigad/mathematics_in_lean_source/issues/138

Last updated: Dec 20 2023 at 11:08 UTC