case mk'
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
e₁ : normalize n₁ d₁ = mk' num✝ den✝
⊢ mk' num✝ den✝ * normalize n₂ d₂ = normalize (n₁ * n₂) (d₁ * d₂)
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ normalize n₁ d₁ * normalize n₂ d₂ = normalize (n₁ * n₂) (d₁ * d₂)
cases e₁ : normalize n₁ d₁ z₁
case mk'.intro.intro.intro
n₂ : Int
d₂ : Nat
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝ * g₁ ≠ 0
e₁ : normalize (num✝ * ↑g₁) (den✝ * g₁) = mk' num✝ den✝
⊢ mk' num✝ den✝ * normalize n₂ d₂ = normalize (num✝ * ↑g₁ * n₂) (den✝ * g₁ * d₂)
case mk'
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
e₁ : normalize n₁ d₁ = mk' num✝ den✝
⊢ mk' num✝ den✝ * normalize n₂ d₂ = normalize (n₁ * n₂) (d₁ * d₂)
rcases normalize_num_den e₁ with ⟨g₁, zg₁, rfl, rfl⟩
case mk'.intro.intro.intro.mk'
n₂ : Int
d₂ : Nat
z₂ : d₂ ≠ 0
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
e₂ : normalize n₂ d₂ = mk' num✝ den✝
⊢ mk' num✝¹ den✝¹ * mk' num✝ den✝ = normalize (num✝¹ * ↑g₁ * n₂) (den✝¹ * g₁ * d₂)
case mk'.intro.intro.intro
n₂ : Int
d₂ : Nat
z₂ : d₂ ≠ 0
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝ * g₁ ≠ 0
e₁ : normalize (num✝ * ↑g₁) (den✝ * g₁) = mk' num✝ den✝
⊢ mk' num✝ den✝ * normalize n₂ d₂ = normalize (num✝ * ↑g₁ * n₂) (den✝ * g₁ * d₂)
cases e₂ : normalize n₂ d₂ z₂
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ mk' num✝¹ den✝¹ * mk' num✝ den✝ = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂))
case mk'.intro.intro.intro.mk'
n₂ : Int
d₂ : Nat
z₂ : d₂ ≠ 0
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
e₂ : normalize n₂ d₂ = mk' num✝ den✝
⊢ mk' num✝¹ den✝¹ * mk' num✝ den✝ = normalize (num✝¹ * ↑g₁ * n₂) (den✝¹ * g₁ * d₂)
rcases normalize_num_den e₂ with ⟨g₂, zg₂, rfl, rfl⟩
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ normalize (num✝¹ * num✝) (den✝¹ * den✝) = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂))
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ mk' num✝¹ den✝¹ * mk' num✝ den✝ = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂))
simp only [mul_def]
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ normalize (num✝¹ * num✝ * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) =
    normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂))
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ normalize (num✝¹ * num✝) (den✝¹ * den✝) = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂))
rw [← normalize_mul_right _ (Nat.mul_ne_zero zg₁ zg₂)]
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_num
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ 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✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ den✝¹ * den✝ * (g₁ * g₂) = den✝¹ * g₁ * (den✝ * g₂)
case mk'.intro.intro.intro.mk'.intro.intro.intro
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ normalize (num✝¹ * num✝ * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) =
    normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂))
congr 1
no goals
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_num
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ num✝¹ * num✝ * ↑(g₁ * g₂) = num✝¹ * ↑g₁ * (num✝ * ↑g₂)
simp [Int.ofNat_mul, Int.mul_assoc, Int.mul_left_comm]
no goals
case mk'.intro.intro.intro.mk'.intro.intro.intro.e_den
num✝¹ : Int
den✝¹ : Nat
den_nz✝¹ : den✝¹ ≠ 0
reduced✝¹ : Nat.coprime (Int.natAbs num✝¹) den✝¹
g₁ : Nat
zg₁ : g₁ ≠ 0
z₁ : den✝¹ * g₁ ≠ 0
e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) = mk' num✝¹ den✝¹
num✝ : Int
den✝ : Nat
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
g₂ : Nat
zg₂ : g₂ ≠ 0
z₂ : den✝ * g₂ ≠ 0
e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) = mk' num✝ den✝
⊢ den✝¹ * den✝ * (g₁ * g₂) = den✝¹ * g₁ * (den✝ * g₂)
simp [Nat.mul_left_comm, Nat.mul_comm]