On repeated rewrites

Stream: new members

[Lauri Oksanen]

Is there a way to repeat an implication in the same way as the equivalence is repeated in

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

Clearly this example can be proven using mul_eq_zero.mp only. The first step is

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
  (x - 1) * (x - 2) = 0 ∨ x - 3 = 0
:= mul_eq_zero.mp h1

Can I repeat this somehow?

[Bjørn Kjos-Hanssen]

Well, yes...

import Mathlib

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
  (x - 1 = 0 ∨ x - 2 = 0) ∨ x - 3 = 0 :=
    (mul_eq_zero.mp h1).elim (.inl ∘ mul_eq_zero.mp) .inr

[Aaron Liu]

A bit shorter:

import Mathlib

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) = 0) :
  (x - 1 = 0 ∨ x - 2 = 0) ∨ x - 3 = 0 :=
    (mul_eq_zero.mp h1).imp_left mul_eq_zero.mp

[Jz Pan]

simp_rw? Or just simpa only [mul_eq_zero] using h1

[Lauri Oksanen]

Thanks a lot for the fast replies, and sorry for the delay from my part. The repeat/simp based solutions generalize easily. For example,

example {x : ℝ} (h1 : (x - 1) * (x - 2) * (x - 3) * (x - 4) = 0) :
  ((x - 1 = 0 ∨ x - 2 = 0) ∨ x - 3 = 0) ∨ x - 4 = 0
:= by
  simp only [mul_eq_zero] at h1
  assumption

But is it possible to make these work with only the implication mul_eq_zero.mp instead of the equivalence mul_eq_zero? On the other hand, it seems to me that the solutions that use mul_eq_zero.mp more directly don't generalize so easily for longer products.

[Robin Arnez]

Generalization using Aaron's method:

example {x : ℝ} (h : (x - 1) * (x - 2) * (x - 3) * (x - 4) * (x - 5) * (x - 6) = 0) :
    ((((x - 1 = 0 ∨ x - 2 = 0) ∨ x - 3 = 0) ∨ x - 4 = 0) ∨ x - 5 = 0) ∨ x - 6 = 0 :=
  (mul_eq_zero.mp h).imp_left fun h =>
  (mul_eq_zero.mp h).imp_left fun h =>
  (mul_eq_zero.mp h).imp_left fun h =>
  (mul_eq_zero.mp h).imp_left mul_eq_zero.mp

[Lauri Oksanen]

Thanks a lot! Is there a way to say repeat (mul_eq_zero.mp h).imp_left fun h => four times?

[Robin Arnez]

if you mean as a tactic:

import Mathlib.Analysis.Normed.Field.Basic

example {x : ℝ} (h : (x - 1) * (x - 2) * (x - 3) * (x - 4) * (x - 5) * (x - 6) = 0) :
    ((((x - 1 = 0 ∨ x - 2 = 0) ∨ x - 3 = 0) ∨ x - 4 = 0) ∨ x - 5 = 0) ∨ x - 6 = 0 := by
  repeat refine (mul_eq_zero.mp h).imp_left fun h => ?_
  assumption

[Lauri Oksanen]

This is exactly what I was wondering about. Thanks a lot! Here is the same thing, written in a slightly different way.

example {x : ℝ} (h : (x - 1) * (x - 2) * (x - 3) * (x - 4) * (x - 5) * (x - 6) = 0) :
    ((((x - 1 = 0 ∨ x - 2 = 0) ∨ x - 3 = 0) ∨ x - 4 = 0) ∨ x - 5 = 0) ∨ x - 6 = 0 := by
  repeat (
    refine (mul_eq_zero.mp h).imp_left ?_
    intro h
  )
  assumption