Tactics for a root systems lemma

Stream: general

[Oliver Nash]

The following is a natural lemma which came up this afternoon in the course of some work on root systems:

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    z = y := by
  sorry

Over the integers it is discharged very nicely by omega as follows:

example (x y z : ℤ)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    z = y := by
  omega

but I would like to have the statement as given above.

I suppose if I really had to I'd pass to the fraction field and argue with ratios (after first dispatching the x = y = z = 0 case).

Do we have ideas for tactics that could crush this?

[Michael Stoll]

Can you use injectivity of Int -> R and reduce it to the integral version this way?

[Michael Stoll]

Probably not, as your variables are in R...

[Mario Carneiro]

Oliver Nash said:

The following is a natural lemma which came up this afternoon in the course of some work on root systems:
[...]
Do we have ideas for tactics that could crush this?

How would you prove it on paper? Tactics don't do magic, they implement known decision procedures or heuristics. Is there some generalization of omega that applies in this situation?

[Oliver Nash]

On paper, I'd do what I mentioned above: pass to the fraction field.

[Mario Carneiro]

and then what?

[Mario Carneiro]

that alone I think already exists (ish), field_simp does that

[Oliver Nash]

Er ... some case analysis I guess :)

[Mario Carneiro]

I guess the idea is that a product of 3 numbers x,y,z \in {1/3,1/2,2,3} which is equal to 1 has some... property, it looks impossible to me?

[Oliver Nash]

Wait, are you saying you think this is not provable?

[Mario Carneiro]

no I think you can prove false from those assumptions

[Aaron Liu]

You can prove that they are all 0

[Mario Carneiro]

but keep in mind that this is a very alien looking goal to me and this is gut impressions

[Vasilii Nesterov]

Btw, I thought polyrith should work after a complete cases splitting, but it fails with a strange error:

import Mathlib

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    z = y := by
  rcases hij with (hij | hij | hij) <;> rcases hik with (hik | hik | hik) <;> rcases hjk with (hjk | hjk | hjk)
  · polyrith -- polyrith found the following certificate, but it failed to close the goal:
             -- hij / 2 + -1 * hik / 2Lean
  all_goals sorry

[Mario Carneiro]

Without using fractions, I guess you could prove that there exist (a,b),(c,d),(e,f) \in{(1,3),(1,2),(2,1),(3,1)} such that (a*c*e) * (x*y*z) = (b*d*f) * (x*y*z), and by case analysis on the numbers you can prove that a*c*e != b*d*f so x*y*z = 0

[Oliver Nash]

Indeed the fraction field is a bit of a red herring and the goal is more naturally stated as x = 0 ∧ y = 0 ∧ z = 0.

What I'd really like to get out of this though is an idea for a tactic. Like this is basically fiddling around with case analysis: computers are supposed to be good that this!

[Mario Carneiro]

well the case analysis part is easy :)

[Mario Carneiro]

it's everything after that where it's not clear what to do

[Bhavik Mehta]

Out of curiosity, was there a previous step before this in terms of x,y,z being in some sets? If so, would you mind sharing it: not because I think this is #xy but because it might look similar to other case-analysis-y proofs that show up for me sometimes

[Mario Carneiro]

It seems like this needs some kind of linear arithmetic tactic :)

[Oliver Nash]

I'd need to do some work before I can easily share this but I can share a version from earlier this afternoon: https://github.com/leanprover-community/mathlib4/pull/23007/files#diff-0e76a5835d2c30c2163fcb8db6b655ffb028c62815c6c1c0d2c1fcc1e8eaba4cR240

Perhaps note in particular: https://github.com/leanprover-community/mathlib4/pull/23007/files#diff-0e76a5835d2c30c2163fcb8db6b655ffb028c62815c6c1c0d2c1fcc1e8eaba4cR103

[Mario Carneiro]

Vasilii Nesterov said:

Btw, I thought polyrith should work after a complete cases splitting, but it fails with a strange error:

-- polyrith found the following certificate, but it failed to close the goal:
-- hij / 2 + -1 * hik / 2

Not that strange, polyrith tried to divide and we can't divide in this ring, we can only argue that things are zero because they are zero when multiplied by a constant

[Mario Carneiro]

which sounds an awful lot like division :)

[Mario Carneiro]

linear_combination doesn't have a syntax for proofs using such a method

[Aaron Liu]

It's CharZero and NoZeroDivisors so we can divide equalities by nonzero integers, which would be a great tactic to have

[Mario Carneiro]

what does it mean to divide an equality by an integer though?

[Mario Carneiro]

I guess there is some divisibility constraint here, you have to be able to write the result without fractions

[Mario Carneiro]

and I'm not sure whether you get what you want if you just do that naively on polyrith's certificates. Are we sure that not just (hij - hik) / 2 but also hij / 2 - hik / 2 avoids divisibility obstructions?

[Mario Carneiro]

I guess you could just clear denominators on the certificate first and do it all at the end

[Oliver Nash]

@Bhavik Mehta I'd love to hear ideas for alternative setup.

The bigger picture is that these are lengths of roots in a crystallographic root system. This means they're integers. They're non-negative because they're lengths (in fact non-zero) and a simple Cauchy-Schwarz argument shows they're at most 3.

However a root system naturally has a set of coefficients R and all these values lie most conveniently inside R, and actually the setup to be able to apply Cauchy-Schwarz while not assuming R is ordered is a little delicate. I have some ideas for design tweaks related to this but suggestions are very welcome.

[Mario Carneiro]

embedding in the fraction ring seems like a pretty pragmatic choice here, it will make polyrith work

[Mario Carneiro]

you should be able to just rewrite all your equalities with injectivity of the injection into the fraction ring and then case split and call polyrith on the results

[Oliver Nash]

But won't I then have a giant list of 64 replacements from the self-replacing polyrith?

[Mario Carneiro]

yes you will

[Oliver Nash]

:scream:

[Mario Carneiro]

you asked for a high automation proof, there you have it

[Mario Carneiro]

I think there are better more "conceptual" ways to prove this which avoid the blowup ending up in your proof script

[Mario Carneiro]

like the one about using products of rational numbers

[Oliver Nash]

Having such a proof is indeed useful and I'm grateful for these valuable ideas but I think the bigger job here is to identify a tactic we could write which would crush this on its own.

[Mario Carneiro]

sure I mean you can always call polyrith without self-replacing

[Mario Carneiro]

it is doing it "on its own"

[Aaron Liu]

Oliver Nash said:

Having such a proof is indeed useful and I'm grateful for these valuable ideas but I think the bigger job here is to identify a tactic we could write which would crush this on its own.

I think there's three separate tactics to be extracted here

[Bhavik Mehta]

Here's a proof using Mario's idea from above:

import Mathlib

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    x = 0 ∧ y = 0 ∧ z = 0 := by
  suffices x * y * z = 0 by
    simp only [mul_eq_zero, or_assoc] at this
    obtain rfl | rfl | rfl := this <;>
    simp_all
  obtain ⟨a, b, hab, hxy⟩ : ∃ a b, (a, b) ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Set (ℕ × ℕ)) ∧ a * x = b * y := by
    simpa [exists_or, or_and_right, eq_comm] using hij
  obtain ⟨c, d, hcd, hxz⟩ : ∃ c d, (c, d) ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Set (ℕ × ℕ)) ∧ c * x = d * z := by
    simpa [exists_or, or_and_right, eq_comm] using hik
  obtain ⟨e, f, hef, hyz⟩ : ∃ e f, (e, f) ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Set (ℕ × ℕ)) ∧ e * y = f * z := by
    simpa [exists_or, or_and_right, eq_comm] using hjk
  have h₁ : a * d * e ≠ b * c * f := by
    suffices
        ∀ ab ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)),
        ∀ cd ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)),
        ∀ ef ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)),
        ab.1 * cd.2 * ef.1 ≠ ab.2 * cd.1 * ef.2 by
      exact this (a, b) (by simpa using hab) (c, d) (by simpa using hcd) (e, f) (by simpa using hef)
    decide
  have h₂ : (a * d * e : R) ≠ b * c * f := mod_cast h₁
  have h₃ : (a * d * e) * (x * y * z) = (b * c * f) * (x * y * z) := by
    calc
      (a * d * e) * (x * y * z) = (a * x) * (d * z) * (e * y) := by ring
      _ = (b * y) * (c * x) * (f * z) := by rw [hxy, ← hxz, hyz]
      _ = (b * c * f) * (x * y * z) := by ring
  have h₄ : (a * d * e - b * c * f) * (x * y * z) = 0 := by linear_combination h₃
  simpa [mul_eq_zero, sub_eq_zero, h₂, false_or] using h₄

[Oliver Nash]

Thank you very, very much!

[Mario Carneiro]

I'm sad h3 isn't a one liner

[Oliver Nash]

@Aaron Liu roughly what are the 3 tactics you had in mind?

[Bhavik Mehta]

I think there's a linear_combination which might do h3, but I did this on the web editor and polyrith doesn't work there so I didn't try too hard

[Mario Carneiro]

lol, irony that the internet is the only thing that can't talk to the internet

[Alex Meiburg]

All 64 cases become some of the form m * x = n * x for some distinct constants m and n, right? And that's just by linear combination. And then you can cancel it to (m - n) * x = 0 and so x = 0, and by symmetry the same for y / z?

[Mario Carneiro]

the "and so" part can't currently be done by linear_combination

[Mario Carneiro]

because it can only divide equations when the ring supports division

[Alex Meiburg]

Right, I get that

[Mario Carneiro]

if it wasn't for that, this should indeed be provable using 64 invocations of polyrith

[Bhavik Mehta]

Oliver Nash said:

Bhavik Mehta I'd love to hear ideas for alternative setup.

The bigger picture is that these are lengths of roots in a crystallographic root system. This means they're integers. They're non-negative because they're lengths (in fact non-zero) and a simple Cauchy-Schwarz argument shows they're at most 3.

However a root system naturally has a set of coefficients R and all these values lie most conveniently inside R, and actually the setup to be able to apply Cauchy-Schwarz while not assuming R is ordered is a little delicate. I have some ideas for design tweaks related to this but suggestions are very welcome.

My suspicion - which isn't validated from your file but I'll mention anyway - was that there's some Set.Pairwise on a set of size 3, which when unrolled gives the relations you have here. And this exact situation (Set.Pairwise on a set of size between 3 and 5) has showed up for me a few times, so that's where my instinct suggests to look

[Oliver Nash]

Interesting. I have done some "unrolling" of finite sets but I'm not sure if I can avoid it. However I'll keep these words in mind.

Btw I just polyrith and it does indeed give a one-liner for your h₃:

have h₃ : (a * d * e) * (x * y * z) = (b * c * f) * (x * y * z) := by
    linear_combination x * z * c * f * hxy - a * e * x * y * hxz + a * x ^ 2 * c * hyz

[Bhavik Mehta]

I just did the same, and this shows that I can make the proof a little simpler:

import Mathlib

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    x = 0 ∧ y = 0 ∧ z = 0 := by
  suffices y * z = 0 by
    simp only [mul_eq_zero, or_assoc] at this
    obtain rfl | rfl := this <;>
    simp_all
  obtain ⟨a, b, hab, hxy⟩ : ∃ a b, (a, b) ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)) ∧ a * x = b * y := by
    simpa [exists_or, or_and_right, eq_comm] using hij
  obtain ⟨c, d, hcd, hxz⟩ : ∃ c d, (c, d) ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)) ∧ c * x = d * z := by
    simpa [exists_or, or_and_right, eq_comm] using hik
  obtain ⟨e, f, hef, hyz⟩ : ∃ e f, (e, f) ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)) ∧ e * y = f * z := by
    simpa [exists_or, or_and_right, eq_comm] using hjk
  have h₁ : a * d * e ≠ b * c * f := by
    suffices
        ∀ ab ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)),
        ∀ cd ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)),
        ∀ ef ∈ ({(1, 2), (1, 3), (2, 1), (3, 1)} : Finset (ℕ × ℕ)),
        ab.1 * cd.2 * ef.1 ≠ ab.2 * cd.1 * ef.2 by
      exact this (a, b) hab (c, d) hcd (e, f) hef
    decide
  have h₂ : (a * d * e : R) ≠ b * c * f := mod_cast h₁
  have h₄ : (a * d * e - b * c * f) * (y * z) = 0 := by
    linear_combination z * c * f * hxy - a * e * y * hxz + a * x * c * hyz
  simpa [mul_eq_zero, sub_eq_zero, h₂, false_or] using h₄

First I can combine h3 and h4, but more interestingly I can prove (a * d * e - b * c * f) * (y * z) = 0 (note the absence of x!) and so we deduce the stronger y * z = 0

[Mario Carneiro]

well I guess in the end they are all 0 :)

[Aaron Liu]

Oliver Nash said:

Aaron Liu roughly what are the 3 tactics you had in mind?

A tactic for pulling out common factors, like how cancel_denoms pulls constant factors out of the denominator. Could be extended to factor polynomials.

A tactic to cancel the same number from both sides of an equality when the domain is cancellable enough, like rewriting 12 * x = 10 * y => 6 * x = 5 * y. Could be extended to also support smul, pow, add, or vadd.

A tactic that will be omitted as it did not fit into the margins of my memory

[Bhavik Mehta]

Mario Carneiro said:

well I guess in the end they are all 0 :)

That's true, it's not really stronger! But it does mean that the only place the proof does an explicit case split is now a case split into 2 cases rather than 3

[Mario Carneiro]

does swapping the Sets for Finsets make the second part of the proof any simpler? I guess the simpa will be unaffected

[Mario Carneiro]

lol you just edited it :)

[Bhavik Mehta]

I just made that change, it means the simpa is unnecessary

[Mario Carneiro]

I also suspect that there is a way to write the obtain lines such that the suffices can be replaced by just revert; decide

[Bhavik Mehta]

Ah true, probably saying they exist in Nat x Nat

[Mario Carneiro]

and let S : Finset (ℕ × ℕ) := {(1, 2), (1, 3), (2, 1), (3, 1)} would remove many of the big terms here

[Oliver Nash]

Feel free to push up improvements here: #23007

[Kevin Buzzard]

I had guessed that fieldOfFractionsify was the other tactic.

[Oliver Nash]

cf https://github.com/leanprover-community/mathlib4/pull/23007/files#diff-0e76a5835d2c30c2163fcb8db6b655ffb028c62815c6c1c0d2c1fcc1e8eaba4cR216

[Mario Carneiro]

Oliver Nash said:

Feel free to push up improvements here: #23007

I found this juxtaposition amusing:

Total mess; will return to tidy this up.

No changes to technical debt.

[Mario Carneiro]

Kevin Buzzard said:

I had guessed that fieldOfFractionsify was the other tactic.

We already have qify, maybe we can just extend the job description? (aka "scope creep")

[Bhavik Mehta]

Mario Carneiro said:

I also suspect that there is a way to write the obtain lines such that the suffices can be replaced by just revert; decide

I got it down to clear! R; decide +revert, will post golfs on the PR rather than spamming more code in this thread :)

[Alex Meiburg]

I guess I'm still not convinced this needs anything like field of fractions, consider

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    x = 0 := by
  rcases hij with (hij | hij | hij | hij) <;> rcases hik with (hik | hik | hik | hik) <;> rcases hjk with (hjk | hjk | hjk | hjk)
  · have : 1 * x = 0 := by
      linear_combination -hij + 2*hik - 2*hjk
    simpa using this
  · have : 2 * x = 0 := by
      linear_combination -hij + 3*hik - 2*hjk
    simpa using this
  · have : -1 * x = 0 := by
      linear_combination -2*hij + 1*hik + 2*hjk
    simpa using this
  · have : -2 * x = 0 := by
      linear_combination -3*hij + 1*hik + 2*hjk
    simpa using this
  · have : 1 * x = 0 := by
      linear_combination -3*hij + 4*hik - 6*hjk
    simpa using this
 --etc.
  all_goals sorry

[Alex Meiburg]

(these simpas are basically just using the mul_eq_zero fact)

[Mario Carneiro]

Isn't that what I've been saying? This is completely within polyriths domain of applicability, and it produces a certificate alright, it just can't be handled by linear_combination because of the cancellation step

[Bhavik Mehta]

I think this idea is just a different phrasing of Mario's from above, with the linear_combinations more explicit

[Mario Carneiro]

so if we extended polyrith and/or linear_combination to do cancellation instead of just division then it would be able to autonomously (if not tersely) prove this goal

[Alex Meiburg]

Ah alright, I must've just not fully grokked what Mario was getting at then, my b

[Mario Carneiro]

This still feels like a case bash though. Is there some more mathematics here, is there a generalization which explains why the product of 3 numbers from {1/3,1/2,2,3} can't be 1?

[Aaron Liu]

If you sum up the padicValRat 2 x + padicValRat 3 x is odd for all x ∈ {1/3,1/2,2,3}, so a product of three will also be odd and therefore not 1

[Eric Wieser]

Can you move to {2, 3, 12, 18} and 6^3 and compute factorizarions?

[Eric Wieser]

Maybe that's more case bashy, not less

[Bhavik Mehta]

My idea was to consider the subgroup of Q* generated by {2,3}, and consider the cayley graph by those generators; then it's bipartite; so a path of length 3 starting from 1 can't end at 1; but this is just Aaron's proof in a different language.

[Kevin Buzzard]

Mario Carneiro said:

This still feels like a case bash though. Is there some more mathematics here, is there a generalization which explains why the product of 3 numbers from {1/3,1/2,2,3} can't be 1?

You can define a group homomorphism from $\mathbb{Q}^\times$ to $\pm1$ sending $-1$ to $1$ and all primes to $-1$ (or just work with $\mathbb{Q}_{>0}$ and send all primes to $-1$); this defines the homomorphism uniquely because $\mathbb{Q}^\times/\pm1$ is freely generated as an abelian group by the primes. Then you just observe that all four of your elements map to $-1$ so the product of three of them must also map to $-1$ and hence can't be $1$. This is just what everyone else has been saying but in a group-theoretic way.

[Aaron Liu]

Kevin Buzzard said:

Mario Carneiro said:

This still feels like a case bash though. Is there some more mathematics here, is there a generalization which explains why the product of 3 numbers from {1/3,1/2,2,3} can't be 1?

You can define a group homomorphism from $\mathbb{Q}^\times$ to $\pm1$ sending $-1$ to $1$ and all primes to $-1$ (or just work with $\mathbb{Q}_{>0}$ and send all primes to $-1$);

Should this be in mathlib?

[Bhavik Mehta]

I'd say that the fact that  $\mathbb{Q}^{\times}/\pm1$ is freely generated by primes should be, then that group hom should come out of a theorem about group homs from a freely generated group

[Mario Carneiro]

I would phrase that slightly more explicitly, and have a factorizationEquiv which is a group hom from $\mathbb{Q}^\times/\pm1$ to $\mathbb{P}\to_0 \mathbb{Z}$

[Aaron Liu]

Why do we have docs#FreeGroupBasis but no version for monoids?

[Bhavik Mehta]

Bhavik Mehta said:

My idea was to consider the subgroup of Q* generated by {2,3}, and consider the cayley graph by those generators; then it's bipartite; so a path of length 3 starting from 1 can't end at 1; but this is just Aaron's proof in a different language.

This perspective also works for the original problem actually, a 3-cycle in this graph is the same thing as {x,y,z} in Oliver's question (ie I have a 3-clique - this is why I was thinking of Set.Pairwise), but it's bipartite so there's no odd cycle

[Kevin Buzzard]

Aaron Liu said:

Why do we have docs#FreeGroupBasis but no version for monoids?

Do we have ℕ+ ≃* (ℙ →₀ ℕ) (we don't even have ℙ for primes I guess)

[Mario Carneiro]

I'm pretty sure we have docs#Nat.Primes

[Aaron Liu]

We have docs#Nat.Primes but no notation

[Kevin Buzzard]

This is the main reason why "the naturals start at 1" is an idea with so much traction (at least in the UK, which traditionally was a centre for number theory); in this kind of number theory it's very natural to start at 1. For example $\zeta(s)=1^{-s}+2^{-s}+\cdots=\prod_p(1-p^{-s})^{-1}$ (and more generally https://en.wikipedia.org/wiki/Euler_product , these are big in Langlands)

[Bhavik Mehta]

Kevin Buzzard said:

Aaron Liu said:

Why do we have docs#FreeGroupBasis but no version for monoids?

Do we have ℕ+ ≃* (ℙ →₀ ℕ) (we don't even have ℙ for primes I guess)

Loogle is giving me nothing for Nat.Primes, MulEquiv, and the only equiv is docs#Nat.Primes.prodNatEquiv

[Notification Bot]

93 messages were moved here from #general > "Missing Tactics" list by Ruben Van de Velde.

[Jz Pan]

Mario Carneiro said:

I'm sad h3 isn't a one liner

Another one-liner proof:

  have h₃ : (a * d * e) * (x * y * z) = (b * c * f) * (x * y * z) := by
    convert congr($hxy * $hxz.symm * $hyz) using 1 <;> ring

[Jz Pan]

Or just linear_combination congr($hxy * $hxz.symm * $hyz)

[Alex J. Best]

Regarding the bad certificate above; If possible polyrith should be changed to query sage over Z[xyz] so that it doesn't return a certificate with division here (or in other situations). I made a pr to ensure that sage supports this a long time ago but never had time to finish the job (the main thing would be ensuring there are no regressions, there shouldn't be but you never know).

[Johan Commelin]

  obtain ⟨ab, hab, hxy⟩ : ∃ ab ∈ S, ab.1 * x = ab.2 * y := by simp_all [eq_comm, S]
  obtain ⟨cd, hcd, hxz⟩ : ∃ cd ∈ S, cd.1 * x = cd.2 * z := by simp_all [eq_comm, S]
  obtain ⟨ef, hef, hyz⟩ : ∃ ef ∈ S, ef.1 * y = ef.2 * z := by simp_all [eq_comm, S]

[Johan Commelin]

import Mathlib

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    x = 0 ∧ y = 0 ∧ z = 0 := by
  suffices y = 0 ∨ z = 0 by apply this.elim <;> rintro rfl <;> simp_all
  let S : Finset (ℕ × ℕ) := {(1, 2), (1, 3), (2, 1), (3, 1)}
  obtain ⟨ab, hab, hxy⟩ : ∃ ab ∈ S, ab.1 * x = ab.2 * y := by simp_all [eq_comm, S]
  obtain ⟨cd, hcd, hxz⟩ : ∃ cd ∈ S, cd.1 * x = cd.2 * z := by simp_all [eq_comm, S]
  obtain ⟨ef, hef, hyz⟩ : ∃ ef ∈ S, ef.1 * y = ef.2 * z := by simp_all [eq_comm, S]
  have : (ab.1 * cd.2 * ef.1 : R) ≠ ab.2 * cd.1 * ef.2 := by norm_cast; clear! R; decide +revert
  have : (ab.1 * cd.2 * ef.1 - ab.2 * cd.1 * ef.2) * (y * z) = 0 := by
    linear_combination z * cd.1 * ef.2 * hxy - ab.1 * ef.1 * y * hxz + ab.1 * x * cd.1 * hyz
  simp_all [sub_eq_zero]

[Wang Jingting]

Well, in this specific case, the following code can be used

import Mathlib

theorem extracted (R : Type*) [CommRing R] [CharZero R] [NoZeroDivisors R] (x y z : R)
    (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x)
    (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x)
    (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) :
    x = 0 ∧ y = 0 ∧ z = 0 := by
  rcases hij with (_ | _ | _ | _) <;> (
    rcases hjk with (_ | _ | _ | _) <;> (
      rcases hik with (_ | _ | _ | _) <;> (
        subst_vars
        rename_i h
        rw [← sub_eq_zero] at h
        ring_nf at h
        simp_all
      )
    )
  )