a b : Rat
⊢ Rat.add a b = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
a b : Rat
⊢ a + b = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
show Rat.add .. = _
a b : Rat
⊢ (let g := Nat.gcd a.den b.den;
    if hg : g = 1 then
      let_fun den_nz := (_ : a.den * b.den ≠ 0);
      let_fun reduced := (_ : Nat.gcd (Int.natAbs (a.num * ↑b.den + b.num * ↑a.den)) (a.den * b.den) = 1);
      mk' (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
    else
      let den := a.den / g * b.den;
      let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g);
      let g1 := Nat.gcd (Int.natAbs num) g;
      let_fun den_nz := (_ : a.den / Nat.gcd a.den b.den * b.den ≠ 0);
      let_fun e :=
        (_ :
          let den := a.den / Nat.gcd a.den b.den * b.den;
          let num := a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den);
          Nat.gcd (Int.natAbs num) (Nat.gcd a.den b.den) = Nat.gcd (Int.natAbs num) den);
      maybeNormalize num den g1 (_ : den / g1 ≠ 0) (_ : Nat.coprime (Int.natAbs (Int.div num ↑g1)) (den / g1))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
a b : Rat
⊢ Rat.add a b = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
delta Rat.add
a b : Rat
⊢ (if hg : Nat.gcd a.den b.den = 1 then mk' (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
    else
      maybeNormalize (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
        (a.den / Nat.gcd a.den b.den * b.den)
        (Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
          (Nat.gcd a.den b.den))
        (_ :
          a.den / Nat.gcd a.den b.den * b.den /
              Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                (Nat.gcd a.den b.den) ≠
            0)
        (_ :
          Nat.coprime
            (Int.natAbs
              (Int.div (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
                ↑(Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                    (Nat.gcd a.den b.den))))
            (a.den / Nat.gcd a.den b.den * b.den /
              Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                (Nat.gcd a.den b.den)))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
a b : Rat
⊢ (let g := Nat.gcd a.den b.den;
    if hg : g = 1 then
      let_fun den_nz := (_ : a.den * b.den ≠ 0);
      let_fun reduced := (_ : Nat.gcd (Int.natAbs (a.num * ↑b.den + b.num * ↑a.den)) (a.den * b.den) = 1);
      mk' (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
    else
      let den := a.den / g * b.den;
      let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g);
      let g1 := Nat.gcd (Int.natAbs num) g;
      let_fun den_nz := (_ : a.den / Nat.gcd a.den b.den * b.den ≠ 0);
      let_fun e :=
        (_ :
          let den := a.den / Nat.gcd a.den b.den * b.den;
          let num := a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den);
          Nat.gcd (Int.natAbs num) (Nat.gcd a.den b.den) = Nat.gcd (Int.natAbs num) den);
      maybeNormalize num den g1 (_ : den / g1 ≠ 0) (_ : Nat.coprime (Int.natAbs (Int.div num ↑g1)) (den / g1))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
dsimp only
case inl
a b : Rat
h✝ : Nat.gcd a.den b.den = 1
⊢ mk' (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)

case inr
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
⊢ maybeNormalize (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
      (a.den / Nat.gcd a.den b.den * b.den)
      (Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
        (Nat.gcd a.den b.den))
      (_ :
        a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den) ≠
          0)
      (_ :
        Nat.coprime
          (Int.natAbs
            (Int.div (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
              ↑(Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                  (Nat.gcd a.den b.den))))
          (a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
a b : Rat
⊢ (if hg : Nat.gcd a.den b.den = 1 then mk' (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
    else
      maybeNormalize (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
        (a.den / Nat.gcd a.den b.den * b.den)
        (Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
          (Nat.gcd a.den b.den))
        (_ :
          a.den / Nat.gcd a.den b.den * b.den /
              Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                (Nat.gcd a.den b.den) ≠
            0)
        (_ :
          Nat.coprime
            (Int.natAbs
              (Int.div (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
                ↑(Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                    (Nat.gcd a.den b.den))))
            (a.den / Nat.gcd a.den b.den * b.den /
              Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                (Nat.gcd a.den b.den)))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
split
no goals
case inl
a b : Rat
h✝ : Nat.gcd a.den b.den = 1
⊢ mk' (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
exact (normalize_self _).symm
case inr
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ maybeNormalize (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
      (a.den / Nat.gcd a.den b.den * b.den)
      (Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
        (Nat.gcd a.den b.den))
      (_ :
        a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den) ≠
          0)
      (_ :
        Nat.coprime
          (Int.natAbs
            (Int.div (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
              ↑(Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                  (Nat.gcd a.den b.den))))
          (a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
case inr
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
⊢ maybeNormalize (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
      (a.den / Nat.gcd a.den b.den * b.den)
      (Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
        (Nat.gcd a.den b.den))
      (_ :
        a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den) ≠
          0)
      (_ :
        Nat.coprime
          (Int.natAbs
            (Int.div (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
              ↑(Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                  (Nat.gcd a.den b.den))))
          (a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
have : a.den.gcd b.den ≠ 0 := Nat.gcd_ne_zero_left a.den_nz
case inr
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ normalize ((a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)) * ↑(Nat.gcd a.den b.den))
      (a.den / Nat.gcd a.den b.den * b.den * Nat.gcd a.den b.den) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
case inr
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ maybeNormalize (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
      (a.den / Nat.gcd a.den b.den * b.den)
      (Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
        (Nat.gcd a.den b.den))
      (_ :
        a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den) ≠
          0)
      (_ :
        Nat.coprime
          (Int.natAbs
            (Int.div (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den))
              ↑(Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
                  (Nat.gcd a.den b.den))))
          (a.den / Nat.gcd a.den b.den * b.den /
            Nat.gcd (Int.natAbs (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)))
              (Nat.gcd a.den b.den))) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
rw [maybeNormalize_eq_normalize _ _
    (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)
    (Nat.dvd_trans (Nat.gcd_dvd_right ..) <|
     Nat.dvd_trans (Nat.gcd_dvd_right ..) (Nat.dvd_mul_left ..)),
  ← normalize_mul_right _ this]
case inr.e_num
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)) * ↑(Nat.gcd a.den b.den) =
    a.num * ↑b.den + b.num * ↑a.den

case inr.e_den
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ a.den / Nat.gcd a.den b.den * b.den * Nat.gcd a.den b.den = a.den * b.den
case inr
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ normalize ((a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)) * ↑(Nat.gcd a.den b.den))
      (a.den / Nat.gcd a.den b.den * b.den * Nat.gcd a.den b.den) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
congr 1
no goals
case inr.e_num
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ (a.num * ↑(b.den / Nat.gcd a.den b.den) + b.num * ↑(a.den / Nat.gcd a.den b.den)) * ↑(Nat.gcd a.den b.den) =
    a.num * ↑b.den + b.num * ↑a.den
simp only [Int.add_mul, Int.mul_assoc, Int.ofNat_mul_ofNat,
  Nat.div_mul_cancel (Nat.gcd_dvd_left ..), Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]
no goals
case inr.e_den
a b : Rat
h✝ : ¬Nat.gcd a.den b.den = 1
this : Nat.gcd a.den b.den ≠ 0
⊢ a.den / Nat.gcd a.den b.den * b.den * Nat.gcd a.den b.den = a.den * b.den
rw [Nat.mul_right_comm, Nat.div_mul_cancel (Nat.gcd_dvd_left ..)]