Sum of equal ratios

Stream: Is there code for X?

[spamegg]

https://proofwiki.org/wiki/Sum_of_Components_of_Equal_Ratios

I tried searching for div_eq_div or div_of_add but could not find anything.

[spamegg]

Version for 2 fractions

import Mathlib

example (a b c d r : ℝ) (hb : b ≠ 0) (hd : d ≠ 0) (hbd : b + d ≠ 0)
    (h1 : a/b = r) (h2 : c/d = r) : (a+c) / (b+d) = r := by
  have arb : a = r*b := (mul_inv_eq_iff_eq_mul₀ hb).mp h1
  have crd : c = r*d := (mul_inv_eq_iff_eq_mul₀ hd).mp h2
  calc (a+c) / (b+d)
    _ = (r*b + c) / (b+d)   := by congr
    _ = (r*b + r*d) / (b+d) := by congr
    _ = r*(b + d) / (b+d)   := by ring
    _ = r                   := by field_simp

[Ruben Van de Velde]

You could write:

import Mathlib

example (a b c d : ℝ) (hb : b ≠ 0) (hd : d ≠ 0) (hbd : b + d ≠ 0)
    (h : a/b = c/d) : (a+c) / (b+d) = a/b := by
  field_simp at *
  linarith
  -- Or: rw [mul_add, h, add_mul]

[spamegg]

Yes I can get rid of r entirely but this is better for educational purposes.

[Eric Wieser]

Another one:

import Mathlib

example (a b c d r : ℝ) (hb : b ≠ 0) (hd : d ≠ 0) (hbd : b + d ≠ 0)
    (h1 : a/b = r) (h2 : c/d = r) : (a+c) / (b+d) = r := by
  rw [div_eq_iff ‹_›] at h1 h2 ⊢
  subst a c
  rw [mul_add]