Theorem: Imo2000P2.lemma2 (Compfiles/Imo2000P2.lean)

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ ∃ x y z, 0 < x ∧ 0 < y ∧ 0 < z ∧ a = x / y ∧ b = y / z ∧ c = z / x
Tactic:
refine ⟨a, 1, (1/b), ha, zero_lt_one, ?_, ?_, ?_, ?_⟩
State after:
case refine_1
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ 0 < 1 / b

case refine_2
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ a = a / 1

case refine_3
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ b = 1 / (1 / b)

case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c = 1 / b / a

State before:
case refine_1
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ 0 < 1 / b
Tactic:
exact one_div_pos.mpr hb
State after:
no goals

State before:
case refine_2
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ a = a / 1
Tactic:
exact (div_one a).symm
State after:
no goals

State before:
case refine_3
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ b = 1 / (1 / b)
Tactic:
exact (one_div_one_div b).symm
State after:
no goals

State before:
case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c = 1 / b / a
Tactic:
field_simp
State after:
case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c * (b * a) = 1

State before:
case refine_4
a b c : ℝ
ha : 0 < a
hb : 0 < b
habc : a * b * c = 1
⊢ c * (b * a) = 1
Tactic:
linarith
State after:
no goals