0 < x.sin → 0 < x and x.sin ≤ 0 → x ≤ 0 (x ∈ Set.Ioc (-π) π)

Stream: new members

[Ilmārs Cīrulis]

How should I approach these two tiny problems? :thinking:
Big thanks for any hints.

import Mathlib

theorem thm1 (x : ℝ) (H : x ≤ Real.pi) (H0 : -Real.pi < x) (H1 : 0 < Real.sin x) : 0 < x := by
  sorry

theorem thm2 (x : ℝ) (H : x ≤ Real.pi) (H0 : -Real.pi < x) (H1 : Real.sin x ≤ 0) : x ≤ 0 := by
  sorry

[Ilmārs Cīrulis]

It feels like I'm missing something simple.

[Ilmārs Cīrulis]

One done.

import Mathlib

theorem thm1 (x : ℝ) (H0 : -Real.pi < x) (H1 : 0 < Real.sin x) :
    0 < x := by
  by_contra H2
  simp at H2
  have H3 := Real.sin_nonpos_of_nonpos_of_neg_pi_le H2 (by linarith)
  linarith

[Ilmārs Cīrulis]

And the second is false in its current form, because in the case of x = Real.pi the sine is equal to 0 and the x is strictly positive.