Theorem: Imo2008P2.subst_abc (Compfiles/Imo2008P2.lean)

State before:
x y z : ℝ
h : x * y * z = 1
⊢ ∃ a b c, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a / b ∧ y = b / c ∧ z = c / a
Tactic:
use x, 1, 1 / y
State after:
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

State before:
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
Tactic:
obtain ⟨⟨hx, hy⟩, _⟩ : (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0 := by
  have := h.symm ▸ one_ne_zero
  simpa [not_or] using this
State after:
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

State before:
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
Tactic:
have : z * (y * x) = 1 := by rw [← h]; ac_rfl
State after:
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
this : z * (y * x) = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x

State before:
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
this : z * (y * x) = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Tactic:
field_simp [*]
State after:
no goals

State before:
x y z : ℝ
h : x * y * z = 1
⊢ (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0
Tactic:
have := h.symm ▸ one_ne_zero
State after:
x y z : ℝ
h : x * y * z = 1
this : x * y * z ≠ 0
⊢ (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0

State before:
x y z : ℝ
h : x * y * z = 1
this : x * y * z ≠ 0
⊢ (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0
Tactic:
simpa [not_or] using this
State after:
no goals

State before:
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ z * (y * x) = 1
Tactic:
rw [← h]
State after:
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ z * (y * x) = x * y * z

State before:
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ z * (y * x) = x * y * z
Tactic:
ac_rfl
State after:
no goals