-- 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:
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

Tactic:
exact Nat.eq_one_of_dvd_one <| a.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
  Nat.dvd_trans (Nat.gcd_dvd_left ..) (ae ▸ Nat.dvd_mul_right ..)

Result:
no goals

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
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

Tactic:
have := Int.dvd_iff_dvd_of_dvd_add 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
this : ↑(d.gcd num.natAbs) ∣ a.num * ↑bd ↔ ↑(d.gcd num.natAbs) ∣ b.num * ↑ad
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

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
⊢ num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
have hden : den = ad * bd * g := by rw [Nat.mul_assoc, be]

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
⊢ 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
this : bd.gcd num.natAbs ∣ b.num.natAbs
⊢ bd.Coprime num.natAbs

Tactic:
exact Nat.eq_one_of_dvd_one <| b.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
  Nat.dvd_trans (Nat.gcd_dvd_left ..) (be ▸ Nat.dvd_mul_right ..)

Result:
no goals

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
⊢ (ad * bd).Coprime num.natAbs

Tactic:
have cop : ad.Coprime bd := had ▸ hbd ▸ hg ▸
  Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_left _ a.den_pos)

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
⊢ (ad * bd).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
⊢ num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
have be : bd * g = b.den := hbd ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_right ..)

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
⊢ 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
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

Tactic:
have := d.gcd_dvd_right num.natAbs

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.natAbs
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

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
H1 : ∀ (d : Nat), d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad
⊢ (ad * bd).Coprime num.natAbs

Tactic:
apply Nat.Coprime.mul

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
⊢ ad.Coprime num.natAbs

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

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
⊢ den = ad * bd * g

Tactic:
rw [Nat.mul_assoc, be]

Result:
no goals

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
this : ↑(d.gcd num.natAbs) ∣ a.num * ↑bd ↔ ↑(d.gcd num.natAbs) ∣ b.num * ↑ad
⊢ d.gcd num.natAbs ∣ a.num.natAbs * bd ↔ d.gcd num.natAbs ∣ b.num.natAbs * ad

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

Result:
no goals