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

Proof state:
a b : Rat
⊢ (let g := a.den.gcd b.den;
    if hg : g = 1 then
      let_fun den_nz := ⋯;
      let_fun reduced := ⋯;
      { num := a.num * ↑b.den + b.num * ↑a.den, den := a.den * b.den, den_nz := den_nz, reduced := reduced }
    else
      let den := a.den / g * b.den;
      let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g);
      let g1 := num.natAbs.gcd g;
      let_fun den_nz := ⋯;
      let_fun e := ⋯;
      maybeNormalize num den g1 ⋯ ⋯) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Tactic:
dsimp only

Result:
a b : Rat
⊢ (if hg : a.den.gcd b.den = 1 then
      { num := a.num * ↑b.den + b.num * ↑a.den, den := a.den * b.den, den_nz := ⋯, reduced := ⋯ }
    else
      maybeNormalize (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den))
        (a.den / a.den.gcd b.den * b.den)
        ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)).natAbs.gcd (a.den.gcd b.den)) ⋯ ⋯) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Proof state:
case isFalse
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ maybeNormalize (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den))
      (a.den / a.den.gcd b.den * b.den)
      ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)).natAbs.gcd (a.den.gcd b.den)) ⋯ ⋯ =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

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

Result:
case isFalse
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ normalize ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)) * ↑(a.den.gcd b.den))
      (a.den / a.den.gcd b.den * b.den * a.den.gcd b.den) ⋯ =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Proof state:
a b : Rat
⊢ (if hg : a.den.gcd b.den = 1 then
      { num := a.num * ↑b.den + b.num * ↑a.den, den := a.den * b.den, den_nz := ⋯, reduced := ⋯ }
    else
      maybeNormalize (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den))
        (a.den / a.den.gcd b.den * b.den)
        ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)).natAbs.gcd (a.den.gcd b.den)) ⋯ ⋯) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Tactic:
split

Result:
case isTrue
a b : Rat
h✝ : a.den.gcd b.den = 1
⊢ { num := a.num * ↑b.den + b.num * ↑a.den, den := a.den * b.den, den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

case isFalse
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
⊢ maybeNormalize (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den))
      (a.den / a.den.gcd b.den * b.den)
      ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)).natAbs.gcd (a.den.gcd b.den)) ⋯ ⋯ =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

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

Tactic:
delta Rat.add

Result:
a b : Rat
⊢ (let g := a.den.gcd b.den;
    if hg : g = 1 then
      let_fun den_nz := ⋯;
      let_fun reduced := ⋯;
      { num := a.num * ↑b.den + b.num * ↑a.den, den := a.den * b.den, den_nz := den_nz, reduced := reduced }
    else
      let den := a.den / g * b.den;
      let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g);
      let g1 := num.natAbs.gcd g;
      let_fun den_nz := ⋯;
      let_fun e := ⋯;
      maybeNormalize num den g1 ⋯ ⋯) =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Proof state:
case isTrue
a b : Rat
h✝ : a.den.gcd b.den = 1
⊢ { num := a.num * ↑b.den + b.num * ↑a.den, den := a.den * b.den, den_nz := ⋯, reduced := ⋯ } =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Tactic:
exact (normalize_self _).symm

Result:
no goals

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

Tactic:
show Rat.add .. = _

Result:
a b : Rat
⊢ a.add b = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Proof state:
case isFalse
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ normalize ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)) * ↑(a.den.gcd b.den))
      (a.den / a.den.gcd b.den * b.den * a.den.gcd b.den) ⋯ =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Tactic:
congr 1

Result:
case isFalse.e_num
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)) * ↑(a.den.gcd b.den) =
    a.num * ↑b.den + b.num * ↑a.den

case isFalse.e_den
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ a.den / a.den.gcd b.den * b.den * a.den.gcd b.den = a.den * b.den

Proof state:
case isFalse
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
⊢ maybeNormalize (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den))
      (a.den / a.den.gcd b.den * b.den)
      ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)).natAbs.gcd (a.den.gcd b.den)) ⋯ ⋯ =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Tactic:
have : a.den.gcd b.den ≠ 0 := Nat.gcd_ne_zero_left a.den_nz

Result:
case isFalse
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ maybeNormalize (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den))
      (a.den / a.den.gcd b.den * b.den)
      ((a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)).natAbs.gcd (a.den.gcd b.den)) ⋯ ⋯ =
    normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

Proof state:
case isFalse.e_den
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ a.den / a.den.gcd b.den * b.den * a.den.gcd b.den = a.den * b.den

Tactic:
rw [Nat.mul_right_comm, Nat.div_mul_cancel (Nat.gcd_dvd_left ..)]

Result:
no goals

Proof state:
case isFalse.e_num
a b : Rat
h✝ : ¬a.den.gcd b.den = 1
this : a.den.gcd b.den ≠ 0
⊢ (a.num * ↑(b.den / a.den.gcd b.den) + b.num * ↑(a.den / a.den.gcd b.den)) * ↑(a.den.gcd b.den) =
    a.num * ↑b.den + b.num * ↑a.den

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

Result:
no goals