Stuck in algebra proof

Stream: new members

[Alex Gu]

Hi,

I am trying to formalize this problem and solution but am a bit stuck on lemma3 and lemma5. Could anyone please give me some helpful pointers? Thanks!

import Mathlib

theorem problem1 (a b c d : ℝ)
  (h1 : a * b * c - d = 1)
  (h2 : b * c * d - a = 2)
  (h3 : c * d * a - b = 3)
  (h4 : d * a * b - c = -6) : a + b + c + d ≠ 0 := by
  intro h
  have lemma1 : a*b*c + b*c*d + c*d*a + d*a*b = 0 := by
    linarith
  have lemma2 : a*b*c*d ≠ 0 := by
    intro h_contra
    have wlog_d : d = 0 := by
      -- WLOG
      sorry
    have abc_0 : a = 0 ∨ b = 0 ∨ c = 0 := by
      rw [wlog_d] at lemma1
      simp at lemma1
      exact or_assoc.mp lemma1
    have wlog_a : a = 0 := by
      -- WLOG
      sorry
    rw [wlog_a, wlog_d] at h1
    simp at h1
  have lemma3: 1/a + 1/b + 1/c + 1/d = 0 := by
    -- divide lemma1 by lemma2
    sorry
  have lemma4: 1/a + 1/b + 1/c = 1/(a+b+c) := by
    have h' : d = -(a+b+c) := by
      linarith
    rw [h'] at lemma3
    linarith
  have lemma5: (a+b)*(b+c)*(c+a)=0 := by
    -- expand lemma4 to show equivalence
    sorry
  have lemma6: False := by
    have a_plus_b_zero : a + b = 0 := by
      -- WLOG
      sorry
    have b_neg : b = -a := by
      linarith
    rw [b_neg] at h2
    rw [b_neg] at h3
    simp at h2
    simp at h3
    have h_contra : 0 = 5 := by
      linarith
    linarith
  exact lemma6

[Luke P]

Have you looked at using the following lemmas?

one_div_add_one_div, div_add_div

I have done a proof for your lemma3 and it seems as though you can use those lemmas along with the cancel_denoms, field_simp, simp_all, ring_nf and linarith tactics.

  have : a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ d ≠ 0 := by simp_all [lemma2]  -- show they are non-zero

  have lemma3: 1/a + 1/b + 1/c + 1/d = 0 := by
    -- divide lemma1 by lemma2
    rw [add_assoc, one_div_add_one_div, one_div_add_one_div, div_add_div] -- doing the maniuplation to the addition of the four fractions
    cancel_denoms -- canceling the denominators
    simp_all  -- simplification
    ring_nf -- rearrangement
    linarith  -- dealing with some cases
    field_simp
    repeat simp_all [this]  -- closing all of the subgoals

Then having a little look at a proof for lemma5 it seems as though it'll go along the same lines as the one for lemma3.

[Ilmārs Cīrulis]

My try...

import Mathlib

theorem problem1 (a b c d : ℝ)
  (h1 : a * b * c - d = 1)
  (h2 : b * c * d - a = 2)
  (h3 : c * d * a - b = 3)
  (h4 : d * a * b - c = -6) : a + b + c + d ≠ 0 := by
  intro h
  have lemma1 : a*b*c + b*c*d + c*d*a + d*a*b = 0 := by
    linarith
  have lemma2a : a ≠ 0 := by sorry
  have lemma2b : b ≠ 0 := by sorry
  have lemma2c : c ≠ 0 := by sorry
  have lemma2d : d ≠ 0 := by sorry
  have lemma3: 1/a + 1/b + 1/c + 1/d = 0 := by
    field_simp; linarith
  have lemma4: 1/a + 1/b + 1/c = 1/(a+b+c) := by
    have h' : d = -(a+b+c) := by linarith
    rw [h'] at lemma3
    linarith
  have lemma5: (a+b)*(b+c)*(c+a)=0 := by
    have aux: a + b + c ≠ 0 := by
      intro H; rw [H] at h; simp at h; tauto
    field_simp at lemma4; linarith
  sorry