lean_workbook_plus_16454
ProvedAlternatively, you can notice that the sum or product of an odd number of negatives is a negative. All squares must be non-negative. So we know is always positive (or zero, but that would make it false), so we only have to worry about . is positive if and negative if , and is positive if and negative if . We want one of them will be positive and the other will be negative to get a negative quotient. This happens if , or .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16454 (x : ℝ) (h₀ : 0 < (x - 1)^2) (h₁ : (x - 2) / (x - 3) < 0) : 2 < x ∧ x < 3 := by sorry
Source