-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mul_def (a b : Rat) :
    a * b = normalize (a.num * b.num) (a.den * b.den) (Nat.mul_ne_zero a.den_nz b.den_nz)

Proof state:
case e_den
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den) *
      (a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den) =
    a.den * b.den

Tactic:
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 ..)]

Result:
no goals

Proof state:
a b : Rat
⊢ a * b = normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
show Rat.mul .. = _

Result:
a b : Rat
⊢ a.mul b = normalize (a.num * b.num) (a.den * b.den) ⋯

Proof state:
a b : Rat
⊢ (let g1 := a.num.natAbs.gcd b.den;
    let g2 := b.num.natAbs.gcd a.den;
    { num := a.num.tdiv ↑g1 * b.num.tdiv ↑g2, den := a.den / g2 * (b.den / g1), den_nz := ⋯, reduced := ⋯ }) =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
dsimp only

Result:
a b : Rat
⊢ { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den),
      den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Proof state:
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den),
      den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]

Result:
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ normalize
      (a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den) *
        ↑(a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den))
      (a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den) *
        (a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den))
      ⋯ =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Proof state:
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
⊢ { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den),
      den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz

Result:
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den),
      den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Proof state:
a b : Rat
⊢ { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den),
      den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz

Result:
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
⊢ { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den),
      den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Proof state:
a b : Rat
⊢ a.mul b = normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
delta Rat.mul

Result:
a b : Rat
⊢ (let g1 := a.num.natAbs.gcd b.den;
    let g2 := b.num.natAbs.gcd a.den;
    { num := a.num.tdiv ↑g1 * b.num.tdiv ↑g2, den := a.den / g2 * (b.den / g1), den_nz := ⋯, reduced := ⋯ }) =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Proof state:
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ normalize
      (a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den) *
        ↑(a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den))
      (a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den) *
        (a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den))
      ⋯ =
    normalize (a.num * b.num) (a.den * b.den) ⋯

Tactic:
congr 1

Result:
case e_num
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den) *
      ↑(a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den) =
    a.num * b.num

case e_den
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den) *
      (a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den) =
    a.den * b.den

Proof state:
case e_num
a b : Rat
H1 : a.num.natAbs.gcd b.den ≠ 0
H2 : b.num.natAbs.gcd a.den ≠ 0
⊢ a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(b.num.natAbs.gcd a.den) *
      ↑(a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den) =
    a.num * b.num

Tactic:
rw [Int.ofNat_mul, ← Int.mul_assoc, Int.mul_right_comm (Int.tdiv ..),
  Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..), Int.mul_assoc,
  Int.tdiv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..)]

Result:
no goals