Theorem: Imo2001P2.imo2001_p2' (Compfiles/Imo2001P2.lean)

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
H : a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
⊢ a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) + b ^ 4 / (b ^ 4 + c ^ 4 + a ^ 4) + c ^ 4 / (c ^ 4 + a ^ 4 + b ^ 4) = 1
Tactic:
ring_nf at H ⊢
State after:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
H : a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
⊢ a ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + b ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + c ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ = 1

State before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
H : a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
⊢ a ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + b ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + c ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ = 1
Tactic:
field_simp
State after:
no goals