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
den : Nat := ad * b.den
num : Int := 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
intro den num
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
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
⊢ 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
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
⊢ Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
have ae : ad * g = a.den := had ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_left ..)
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
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
⊢ 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
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
⊢ Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
have be : bd * g = b.den := hbd ▸ Nat.div_mul_cancel (hg ▸ Nat.gcd_dvd_right ..)
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
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
⊢ 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
den : Nat := ad * b.den
num : Int := a.num * ↑bd + b.num * ↑ad
ae : ad * g = a.den
be : bd * g = b.den
⊢ Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
have hden : den = ad * bd * g := by rw [Nat.mul_assoc, be]
case H
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
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
⊢ Nat.coprime (ad * bd) (Int.natAbs num)
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
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
⊢ Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
rw [hden, Nat.coprime.gcd_mul_left_cancel_right]
case H
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
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 : Nat.coprime ad bd
⊢ Nat.coprime (ad * bd) (Int.natAbs num)
case H
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
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
⊢ Nat.coprime (ad * bd) (Int.natAbs num)
have cop : ad.coprime bd := had ▸ hbd ▸ hg ▸
  Nat.coprime_div_gcd_div_gcd (Nat.gcd_pos_of_pos_left _ a.den_pos)
case H
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime (ad * bd) (Int.natAbs num)
case H
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
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 : Nat.coprime ad bd
⊢ Nat.coprime (ad * bd) (Int.natAbs num)
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
case H.H1
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime ad (Int.natAbs num)

case H.H2
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime bd (Int.natAbs num)
case H
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime (ad * bd) (Int.natAbs num)
apply Nat.coprime.mul
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
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
rw [Nat.mul_assoc, be]
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
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 : Nat.coprime ad bd
d : Nat
this : Nat.gcd d (Int.natAbs num) ∣ Int.natAbs num
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
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
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 : Nat.coprime ad bd
d : Nat
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
have := d.gcd_dvd_right num.natAbs
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
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 : Nat.coprime ad bd
d : Nat
this : ↑(Nat.gcd d (Int.natAbs num)) ∣ num
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
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
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 : Nat.coprime ad bd
d : Nat
this : Nat.gcd d (Int.natAbs num) ∣ Int.natAbs num
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
rw [← Int.ofNat_dvd, Int.dvd_natAbs] at this
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
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 : Nat.coprime ad bd
d : Nat
this✝ : ↑(Nat.gcd d (Int.natAbs num)) ∣ num
this : ↑(Nat.gcd d (Int.natAbs num)) ∣ a.num * ↑bd ↔ ↑(Nat.gcd d (Int.natAbs num)) ∣ b.num * ↑ad
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
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
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 : Nat.coprime ad bd
d : Nat
this : ↑(Nat.gcd d (Int.natAbs num)) ∣ num
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
have := Int.dvd_iff_dvd_of_dvd_add 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
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 : Nat.coprime ad bd
d : Nat
this✝ : ↑(Nat.gcd d (Int.natAbs num)) ∣ num
this : ↑(Nat.gcd d (Int.natAbs num)) ∣ a.num * ↑bd ↔ ↑(Nat.gcd d (Int.natAbs num)) ∣ b.num * ↑ad
⊢ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
rwa [← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul,
  ← Int.dvd_natAbs, Int.ofNat_dvd, Int.natAbs_mul] at this
case H.H1
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this : Nat.gcd ad (Int.natAbs num) ∣ Int.natAbs a.num * bd
⊢ Nat.coprime ad (Int.natAbs num)
case H.H1
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime ad (Int.natAbs num)
have := (H1 ad).2 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)
case H.H1
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this✝ : Nat.gcd ad (Int.natAbs num) ∣ Int.natAbs a.num * bd
this : Nat.gcd ad (Int.natAbs num) ∣ Int.natAbs a.num
⊢ Nat.coprime ad (Int.natAbs num)
case H.H1
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this : Nat.gcd ad (Int.natAbs num) ∣ Int.natAbs a.num * bd
⊢ Nat.coprime ad (Int.natAbs num)
have := (cop.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this
no goals
case H.H1
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this✝ : Nat.gcd ad (Int.natAbs num) ∣ Int.natAbs a.num * bd
this : Nat.gcd ad (Int.natAbs num) ∣ Int.natAbs a.num
⊢ Nat.coprime ad (Int.natAbs num)
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 ..)
case H.H2
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this : Nat.gcd bd (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime bd (Int.natAbs num)
case H.H2
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime bd (Int.natAbs num)
have := (H1 bd).1 <| Nat.dvd_trans (Nat.gcd_dvd_left ..) (Nat.dvd_mul_left ..)
case H.H2
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this✝ : Nat.gcd bd (Int.natAbs num) ∣ Int.natAbs b.num * ad
this : Nat.gcd bd (Int.natAbs num) ∣ Int.natAbs b.num
⊢ Nat.coprime bd (Int.natAbs num)
case H.H2
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this : Nat.gcd bd (Int.natAbs num) ∣ Int.natAbs b.num * ad
⊢ Nat.coprime bd (Int.natAbs num)
have := (cop.symm.coprime_dvd_left <| Nat.gcd_dvd_left ..).dvd_of_dvd_mul_right this
no goals
case H.H2
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
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 : Nat.coprime ad bd
H1 :
  ∀ (d : Nat), Nat.gcd d (Int.natAbs num) ∣ Int.natAbs a.num * bd ↔ Nat.gcd d (Int.natAbs num) ∣ Int.natAbs b.num * ad
this✝ : Nat.gcd bd (Int.natAbs num) ∣ Int.natAbs b.num * ad
this : Nat.gcd bd (Int.natAbs num) ∣ Int.natAbs b.num
⊢ Nat.coprime bd (Int.natAbs num)
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 ..)