-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Basic.lean
theorem add.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd 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
    num.natAbs.gcd g = num.natAbs.gcd den

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
d : Nat
this : d.gcd num.natAbs ∣ num.natAbs
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

Tactic:
rw [← Int.ofNat_dvd, Int.dvd_natAbs] at this

Result:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
d : Nat
this : ↑(d.gcd num.natAbs) ∣ num
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

Proof state:
case H.H1
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
this : ad.gcd num.natAbs ∣ a.num.natAbs * bd
⊢ ad.Coprime num.natAbs

Tactic:
have := (cop.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this

Result:
case H.H1
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
this✝ : ad.gcd num.natAbs ∣ a.num.natAbs * bd
this : ad.gcd num.natAbs ∣ a.num.natAbs
⊢ ad.Coprime num.natAbs

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
⊢ num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
have ae : ad * g = a.den := had ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_left ..)

Result:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
⊢ num.natAbs.gcd g = num.natAbs.gcd den

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd 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;
  num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
intro den num

Result:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
⊢ num.natAbs.gcd g = num.natAbs.gcd den

Proof state:
case H.H2
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
this : bd.gcd num.natAbs ∣ b.num.natAbs * ad
⊢ bd.Coprime num.natAbs

Tactic:
have := (cop.symm.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this

Result:
case H.H2
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
this✝ : bd.gcd num.natAbs ∣ b.num.natAbs * ad
this : bd.gcd num.natAbs ∣ b.num.natAbs
⊢ bd.Coprime num.natAbs

Proof state:
case H
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
⊢ (ad * bd).Coprime num.natAbs

Tactic:
have H1 (d : Nat) :
    d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad := by
  have := d.gcd_dvd_right num.natAbs
  rw [← Int.ofNat_dvd, Int.dvd_natAbs] at this
  have := Int.dvd_iff_dvd_of_dvd_add this
  rwa [← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul,
    ← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul] at this

Result:
case H
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
⊢ (ad * bd).Coprime num.natAbs

Proof state:
case H.H1
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
⊢ ad.Coprime num.natAbs

Tactic:
have := (H1 ad).2 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)

Result:
case H.H1
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
this : ad.gcd num.natAbs ∣ a.num.natAbs * bd
⊢ ad.Coprime num.natAbs

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
⊢ num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
rw [hden, Nat.Coprime.gcd_mul_left_cancel_right]

Result:
case H
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
⊢ (ad * bd).Coprime num.natAbs

Proof state:
case H.H2
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
⊢ bd.Coprime num.natAbs

Tactic:
have := (H1 bd).1 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)

Result:
case H.H2
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
hden : den = ad * bd * g
cop : ad.Coprime bd
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
this : bd.gcd num.natAbs ∣ b.num.natAbs * ad
⊢ bd.Coprime num.natAbs