Proving an or-statement with nice structure

Stream: new members

[Lauri Oksanen]

Is there a short way to capture the natural structure in

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
  x = 1 ∨ x = 2 ∨ x = 3
:= by
  obtain h2 | _ := mul_eq_zero.mp h1
  · obtain _ | _ := mul_eq_zero.mp h2
    · left
      linarith
    · right
      left
      linarith
  · right
    right
    linarith

[Kevin Buzzard]

What does this question mean? Do you just mean "can someone golf this proof"?

[Lauri Oksanen]

Right, the question is quite vague. The hypothesis can be split in cases systematically by using mul_eq_zero.mp and all the cases are solved by linarith. The pieces in the hypothesis and the goal have the same order, so I wonder if there is a way to repeat this pattern in a way that would generalize in verbatim for longer products as well. Something a bit like

example {x y z : ℝ}
  (_ : 1*x + 2*y + 3*z = 1)
  (_ : 2*x + 4*y + 5*z = 0)
  (_ : 3*x + 5*y + 6*z = 0) :
  x = 1 ∧ y = -3 ∧ z = 2
:= by
  split_ands <;> linarith

[Zhang Qinchuan]

Is this what you want?

import Mathlib

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
    x = 1 ∨ x = 2 ∨ x = 3 := by
  repeat rw [mul_eq_zero] at h1
  repeat rw [sub_eq_zero] at h1
  tauto

[Edward van de Meent]

or even:

import Mathlib

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
    x = 1 ∨ x = 2 ∨ x = 3 := by
  simp_rw [mul_eq_zero,sub_eq_zero] at h1
  tauto

[Zhang Qinchuan]

or even just one line:

import Mathlib

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
    x = 1 ∨ x = 2 ∨ x = 3 := by
  rwa [mul_eq_zero, mul_eq_zero, sub_eq_zero, sub_eq_zero, sub_eq_zero, or_assoc] at h1

[Lauri Oksanen]

Thanks a lot! This is pretty much what I want.