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

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₁ * n₂) (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₁ * n₂) (den✝ * g₁ * d₂) ⋯

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ normalize n₁ d₁ z₁ * normalize n₂ d₂ z₂ = normalize (n₁ * n₂) (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₁ * n₂) (d₁ * d₂) ⋯

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₁ * n₂) (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₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

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✝¹ * num✝ * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) ⋯ =
    normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯

Tactic:
congr 1

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✝¹ * num✝ * ↑(g₁ * g₂) = num✝¹ * ↑g₁ * (num✝ * ↑g₂)

case mk'.intro.intro.intro.mk'.intro.intro.intro.e_den
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✝ }
⊢ den✝¹ * den✝ * (g₁ * g₂) = den✝¹ * g₁ * (den✝ * g₂)

Proof state:
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₁ * n₂) (den✝ * g₁ * d₂) ⋯

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

Result:
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₁ * n₂) (den✝¹ * g₁ * d₂) ⋯

Proof state:
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_den
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✝ }
⊢ den✝¹ * den✝ * (g₁ * g₂) = den✝¹ * g₁ * (den✝ * g₂)

Tactic:
simp [Nat.mul_left_comm, Nat.mul_comm]

Result:
no goals

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✝¹ * num✝ * ↑(g₁ * g₂) = num✝¹ * ↑g₁ * (num✝ * ↑g₂)

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

Result:
no goals