regarding "let"

Stream: new members

[Shange Tang]

I have written the following lean code:

import Mathlib

example (x y : ℕ) (h₀ : 0 < x ∧ 0 < y) (h₁ : x * y + (x + y) = 71)
  (h₂ : x ^ 2 * y + x * y ^ 2 = 880) : x ^ 2 + y ^ 2 = 146 := by
  let S := x + y
  let P := x * y
  have h₃ : P + S = 71 := by linarith
sorry

This is only part of my code. I want to introduce to variables first, and then first claim some trivial result. However linarith fails to prove h₃ . It seems that the "let" is very strange. Does anyone know how to prove such a trivial problem? Or is my usage of "let" wrong?

[Kyle Miller]

linarith doesn't unfold let bindings. If you do have h₃ : P + S = 71 := by unfold S P; linarith then it works.

[Kyle Miller]

Or, since these are natural numbers, you can do by omega

[Shange Tang]

Thanks for your reply. However when I do the unfold as the following, it says "unknown constant 'S'".

example (x y : ℕ) (h₀ : 0 < x ∧ 0 < y) (h₁ : x * y + (x + y) = 71)
  (h₂ : x ^ 2 * y + x * y ^ 2 = 880) : x ^ 2 + y ^ 2 = 146 := by
  let S := x + y
  let P := x * y
  have h₃ : P + S = 71 := by unfold S P; linarith
sorry

[Ruben Van de Velde]

Maybe simp only [S, P]

[Ruben Van de Velde]

But please keep the imports in all code you post

[Shange Tang]

Thanks for the reply. The following is the code with import:

import Mathlib

set_option maxHeartbeats 0

open BigOperators Real Nat

example (x y : ℕ) (h₀ : 0 < x ∧ 0 < y) (h₁ : x * y + (x + y) = 71)
  (h₂ : x ^ 2 * y + x * y ^ 2 = 880) : x ^ 2 + y ^ 2 = 146 := by
  let S := x + y
  let P := x * y
  have h₃ : P + S = 71 := by sorry
  sorry

[Kyle Miller]

If simp only [S, P] doesn't work as a replacement for the newer unfold S P, then you must have an older mathlib. Maybe you have unfold_lets S P?

[Shange Tang]

I am using lean4 web, and I believe I select the latest Mathlib.

import Mathlib

set_option maxHeartbeats 0

open BigOperators Real Nat

example (x y : ℕ) (h₀ : 0 < x ∧ 0 < y) (h₁ : x * y + (x + y) = 71)
  (h₂ : x ^ 2 * y + x * y ^ 2 = 880) : x ^ 2 + y ^ 2 = 146 := by
  let S := x + y
  let P := x * y
  have h₃ : P + S = 71 := by simp only [S, P]; exact h₁
  sorry

Now h_3 is proved.

[Kyle Miller]

I just tested

import Mathlib

open BigOperators Real Nat

example (x y : ℕ) (h₀ : 0 < x ∧ 0 < y) (h₁ : x * y + (x + y) = 71)
  (h₂ : x ^ 2 * y + x * y ^ 2 = 880) : x ^ 2 + y ^ 2 = 146 := by
  let S := x + y
  let P := x * y
  have h₃ : P + S = 71 := by unfold S P; exact h₁
  sorry

on the web Lean 4, and it works fine. I'm getting to it using the "view in Lean 4 playground" button that appears in the upper-right corner of the code block.

[Shange Tang]

It seems that in my local VScode, unfold does not work, but simp only works.