How to use let?

Stream: new members

[tsuki hao]

Does any know how to apply the y?

import Mathlib
import LeanCopilot

open Real
example {x : ℝ} (hx : 0 < x) (hx' : x < π) :
    12 ≤ (9 * x ^ 2 * sin x ^ 2 + 4) / (x * sin x) := by
  let y := x * sin x
  have hy : 0 < y := by
    have t1 : sin x > 0 := by
      exact sin_pos_of_pos_of_lt_pi hx hx'
    exact Real.mul_pos hx t1
  have h1: 12 ≤ (9 * y ^ 2 + 4) / y := by
    rw [le_div_iff hy]
    sorry
  sorry

[Mitchell Lee]

One option is to use

rw [(by rfl : y = x * sin x)] at h1

This will replace every occurrence of y in the hypothesis h1 with x * sin x.

Slightly easier is to replace the line let y := x * sin x with set! y := x * sin x with y_eq. Then, you will have a hypothesis y_eq : y = x * sin x, and you can instead write

rw [y_eq] at h1

Regardless of which option you choose, you can finish the goal using

convert h1 using 2
ring

[Kyle Miller]

dsimp only [y] at h1 should unfold y at h1

[Kyle Miller]

Depending on what you're doing, that might not be necessary, since y is x * sin x by definition.