-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_add_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
    normalize n₁ d₁ z₁ + normalize n₂ d₂ z₂ =
    normalize (n₁ * d₂ + n₂ * d₁) (d₁ * d₂) (Nat.mul_ne_zero z₁ z₂)

Proof state:
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_num
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ (num✝¹ * ↑den✝ + num✝ * ↑den✝¹) * ↑(g₁ * g₂) = num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)

Tactic:
rw [Int.add_mul]

Result:
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_num
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ num✝¹ * ↑den✝ * ↑(g₁ * g₂) + num✝ * ↑den✝¹ * ↑(g₁ * g₂) = num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ normalize n₁ d₁ z₁ + normalize n₂ d₂ z₂ = normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯

Tactic:
cases e₁ : normalize n₁ d₁ z₁

Result:
case mk'
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
e₁ : normalize n₁ d₁ z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } + normalize n₂ d₂ z₂ =
    normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯

Proof state:
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_num
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ num✝¹ * ↑den✝ * ↑(g₁ * g₂) + num✝ * ↑den✝¹ * ↑(g₁ * g₂) = num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)

Tactic:
simp [Int.ofNat_mul, Int.mul_assoc, Int.mul_left_comm, Int.mul_comm]

Result:
no goals

Proof state:
case mk'.intro.intro.intro.mk'
n₂ : Int
d₂ : Nat
z₂ : d₂ ≠ 0
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
e₂ : normalize n₂ d₂ z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } +
      { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } =
    normalize (num✝¹ * ↑g₁ * ↑d₂ + n₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * d₂) ⋯

Tactic:
rcases normalize_num_den e₂ with ⟨g₂, zg₂, rfl, rfl⟩

Result:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } +
      { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } =
    normalize (num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

Proof state:
case mk'
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
e₁ : normalize n₁ d₁ z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } + normalize n₂ d₂ z₂ =
    normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯

Tactic:
rcases normalize_num_den e₁ with ⟨g₁, zg₁, rfl, rfl⟩

Result:
case mk'.intro.intro.intro
n₂ : Int
d₂ : Nat
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝ * g₁ ≠ 0
e₁ : normalize (num✝ * ↑g₁) (den✝ * g₁) z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } + normalize n₂ d₂ z₂ =
    normalize (num✝ * ↑g₁ * ↑d₂ + n₂ * ↑(den✝ * g₁)) (den✝ * g₁ * d₂) ⋯

Proof state:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ normalize (num✝¹ * ↑den✝ + num✝ * ↑den✝¹) (den✝¹ * den✝) ⋯ =
    normalize (num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

Tactic:
rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]

Result:
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : num✝¹.natAbs.Coprime den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ normalize ((num✝¹ * ↑den✝ + num✝ * ↑den✝¹) * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) ⋯ =
    normalize (num✝¹ * ↑g₁ * ↑(den✝ * g₂) + num✝ * ↑g₂ * ↑(den✝¹ * g₁)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯