a b : Rat
⊢ Rat.mul a b = normalize (a.num * b.num) (a.den * b.den)
a b : Rat
⊢ a * b = normalize (a.num * b.num) (a.den * b.den)
show Rat.mul .. = _
a b : Rat
⊢ (let g1 := Nat.gcd (Int.natAbs a.num) b.den;
    let g2 := Nat.gcd (Int.natAbs b.num) a.den;
    mk' (Int.div a.num ↑g1 * Int.div b.num ↑g2) (a.den / g2 * (b.den / g1))) =
    normalize (a.num * b.num) (a.den * b.den)
a b : Rat
⊢ Rat.mul a b = normalize (a.num * b.num) (a.den * b.den)
delta Rat.mul
a b : Rat
⊢ mk' (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den)) =
    normalize (a.num * b.num) (a.den * b.den)
a b : Rat
⊢ (let g1 := Nat.gcd (Int.natAbs a.num) b.den;
    let g2 := Nat.gcd (Int.natAbs b.num) a.den;
    mk' (Int.div a.num ↑g1 * Int.div b.num ↑g2) (a.den / g2 * (b.den / g1))) =
    normalize (a.num * b.num) (a.den * b.den)
dsimp only
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
⊢ mk' (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den)) =
    normalize (a.num * b.num) (a.den * b.den)
a b : Rat
⊢ mk' (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den)) =
    normalize (a.num * b.num) (a.den * b.den)
have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ mk' (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den)) =
    normalize (a.num * b.num) (a.den * b.den)
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
⊢ mk' (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den)) =
    normalize (a.num * b.num) (a.den * b.den)
have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ normalize
      (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den) *
        ↑(Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den) *
        (Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den)) =
    normalize (a.num * b.num) (a.den * b.den)
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ mk' (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den)) =
    normalize (a.num * b.num) (a.den * b.den)
rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]
case e_num
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den) *
      ↑(Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den) =
    a.num * b.num

case e_den
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den) *
      (Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den) =
    a.den * b.den
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ normalize
      (Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den) *
        ↑(Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den))
      (a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den) *
        (Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den)) =
    normalize (a.num * b.num) (a.den * b.den)
congr 1
no goals
case e_num
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ Int.div a.num ↑(Nat.gcd (Int.natAbs a.num) b.den) * Int.div b.num ↑(Nat.gcd (Int.natAbs b.num) a.den) *
      ↑(Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den) =
    a.num * b.num
rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.div ..),
  Int.div_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
  Int.div_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]
no goals
case e_den
a b : Rat
H1 : Nat.gcd (Int.natAbs a.num) b.den ≠ 0
H2 : Nat.gcd (Int.natAbs b.num) a.den ≠ 0
⊢ a.den / Nat.gcd (Int.natAbs b.num) a.den * (b.den / Nat.gcd (Int.natAbs a.num) b.den) *
      (Nat.gcd (Int.natAbs a.num) b.den * Nat.gcd (Int.natAbs b.num) a.den) =
    a.den * b.den
rw [← Nat.mul_assoc, Nat.mul_right_comm, Nat.mul_right_comm (_/_),
  Nat.div_mul_cancel (Nat.gcd_dvd_right ..), Nat.mul_assoc,
  Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]