Proving (a - b) / (c - d) = (b - a) / (d - c)

Stream: new members

[Isak Colboubrani]

While working on some very simple examples for some fellow undergraduates, I came up with the following.

Is there a higher-level tactic that could handle the second step (possibly after guidance with additional lemma annotations)? Which higher-level tactic would be the most likely candidate in this situation?

Is there any way to refine this example to make it more readable or idiomatic, or otherwise enhance it?

example {R : Type*} [Field R] (a b c d : R) : (a - b) / (c - d) = (b - a) / (d - c) := by
  calc
    (a - b) / (c - d) = -(b - a) / -(d - c) := by ring
    _ = (b - a) / (d - c) := by exact neg_div_neg_eq (b - a) (d - c)

[Chris Bailey]

Not an expert on the mathlib tactics, but fwiw by apply? finds the right lemma.

[Walter Moreira]

For the second case in calc, the tactic cancel_denoms helps to normalize the denominators, and then ring works:

import Mathlib

example {R : Type*} [Field R] (a b c d : R) : (a - b) / (c - d) = (b - a) / (d - c) := by
  calc
    (a - b) / (c - d) = -(b - a) / -(d - c) := by ring
    _ = (b - a) / (d - c) := by cancel_denoms; ring

An alternative shorter proof (but maybe more obscure) is:

import Mathlib

example {R : Type*} [Field R] (a b c d : R) : (a - b) / (c - d) = (b - a) / (d - c) := by
  rw [<- neg_div_neg_eq, neg_sub, neg_sub]

[Isak Colboubrani]

@Walter Moreira Thank you! Indeed, it's cancel_denoms. For some reason, I confused it with field_simp. Thanks!

[Isak Colboubrani]

I don't think the golfed rw solution will resonate with my audience. The loss in readability isn’t worth the minor thrill they might feel from seeing one line of code being trimmed off :)

I could include it as a contrasting example on the pros/cons of golfing however, so thanks for providing it.

[Isak Colboubrani]

I’ve settled on these three examples demonstrating different approaches. Any fourth alternative worth adding for pedagogical reasons?

import Mathlib
variable {K : Type*} [Field K]
theorem sub_div_sub_a (a b c d : K) : (a - b) / (c - d) = (b - a) / (d - c) := by
  calc
    (a - b) / (c - d) = -(b - a) / -(d - c) := by ring
    _ = (b - a) / (d - c) := by cancel_denoms; ring

theorem sub_div_sub_b (a b c d : K) : (a - b) / (c - d) = (b - a) / (d - c) := by
  calc
    (a - b) / (c - d) = -(b - a) / -(d - c) := by rw [neg_sub, neg_sub]
    _ = (b - a) / (d - c) := by rw [neg_div_neg_eq]

theorem sub_div_sub_c (a b c d : K) : (a - b) / (c - d) = (b - a) / (d - c) := by
  rw [← neg_div_neg_eq, neg_sub, neg_sub]

[Walter Moreira]

I agree with you that the calc proof is much more illustrative. You might be interested in this other thread where people are talking about the trade-offs you mention: #new members > ✔ How can I finish off this proof? So close...

[Ilmārs Cīrulis]

Dunno if this is worth of adding, but this was my approach. :sweat_smile:

import Mathlib
variable {K : Type*} [Field K]

theorem sub_div_sub_d (a b c d : K) : (a - b) / (c - d) = (b - a) / (d - c) := by
  obtain H | H := em (c - d = 0)
  . rw [sub_eq_zero] at H
    subst H
    simp
  . have t: ¬ d - c = 0 := by rw [sub_eq_zero] at *; tauto
    field_simp; ring

[Edit: simplified a bit]

[Ilmārs Cīrulis]

I like it because, err, it looks at the case of division by zero and at "normal" situation. Smth like that.

[Isak Colboubrani]

Previously while browsing Mathlib/Algebra/Field/Basic.lean looking for something similar to sub_div_sub lemma (if it existed), I came across two oddly specific lemmas that do not seem to be referenced anywhere:

theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a * (a + b) * (1 / b) = 1 / a + 1 / b := by […]
theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a * (b - a) * (1 / b) = 1 / a - 1 / b := by […]

All of this has made me wonder about the general criteria for including "trivial lemmas": particularly those that cannot demonstrate any "immediate demand" by being applied in another proof for example. Since there is effectively an unlimited number of statements that Lean could be taught, I’m curious about how one decides where to draw the line—especially for trivial lemmas that, by definition, aren’t mathematically significant on their own. I realize it’s a broad question, but I remain intrigued nonetheless.

As an example: would a lemma like sub_div_sub (see above) meet the bar for potential inclusion (not that I’m advocating for it, but just out of curiosity)?

[Ruben Van de Velde]

Probably these would be added when someone needs them

[Kevin Buzzard]

We already have neg_div_neg_eq and the result follows easily from that:

import Mathlib

variable {K : Type*} [DivisionRing K]

theorem sub_div_sub_eq (a b c d : K) : (a - b) / (c - d) = (b - a) / (d - c) := by
  simp [← neg_div_neg_eq (a - b)]