obtain ⟨⟨hx, hy⟩, _⟩ : (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0 := by
  have := h.symm ▸ one_ne_zero
  simpa [not_or] using this
case h
x y z : ℝ
h : x * y * z = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x