a b : Rat
g ad bd : Nat
hg : g = Nat.gcd a.den b.den
had : ad = a.den / g
hbd : bd = b.den / g
this :
  let den := ad * (-b).den;
  let num := a.num * ↑bd + (-b).num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
a b : Rat
g ad bd : Nat
hg : g = Nat.gcd a.den b.den
had : ad = a.den / g
hbd : bd = b.den / g
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
have := add.aux a (-b) hg had hbd
a b : Rat
g ad bd : Nat
hg : g = Nat.gcd a.den b.den
had : ad = a.den / g
hbd : bd = b.den / g
this :
  Nat.gcd (Int.natAbs (a.num * ↑bd + -(b.num * ↑ad))) g =
    Nat.gcd (Int.natAbs (a.num * ↑bd + -(b.num * ↑ad))) (ad * (-b).den)
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
a b : Rat
g ad bd : Nat
hg : g = Nat.gcd a.den b.den
had : ad = a.den / g
hbd : bd = b.den / g
this :
  let den := ad * (-b).den;
  let num := a.num * ↑bd + (-b).num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
simp only [show (-b).num = -b.num from rfl, Int.neg_mul] at this
no goals
a b : Rat
g ad bd : Nat
hg : g = Nat.gcd a.den b.den
had : ad = a.den / g
hbd : bd = b.den / g
this :
  Nat.gcd (Int.natAbs (a.num * ↑bd + -(b.num * ↑ad))) g =
    Nat.gcd (Int.natAbs (a.num * ↑bd + -(b.num * ↑ad))) (ad * (-b).den)
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
exact this