case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : normalize n₁ d₁ = normalize n₂ d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

case mpr
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ * ↑d₂ = n₂ * ↑d₁
⊢ normalize n₁ d₁ = normalize n₂ d₂
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
constructor <;> intro h
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : normalize n₁ d₁ = normalize n₂ d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
simp only [normalize_eq, mk'.injEq] at h
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
have' hn₁ := Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left n₁.natAbs d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
hn₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
have' hn₂ := Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left n₂.natAbs d₂
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
hn₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂
hd₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
hn₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
have' hd₁ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₁.natAbs d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
hn₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂
hd₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁
hd₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
hn₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂
hd₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
have' hd₂ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₂.natAbs d₂
no goals
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h :
  n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧
    d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂
hn₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁
hn₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂
hd₁ : ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁
hd₂ : ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁
rw [← Int.ediv_mul_cancel (Int.dvd_trans hd₂ (Int.dvd_mul_left ..)),
  Int.mul_ediv_assoc _ hd₂, ← Int.ofNat_ediv, ← h.2, Int.ofNat_ediv,
  ← Int.mul_ediv_assoc _ hd₁, Int.mul_ediv_assoc' _ hn₁,
  Int.mul_right_comm, h.1, Int.ediv_mul_cancel hn₂]
no goals
case mpr
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ * ↑d₂ = n₂ * ↑d₁
⊢ normalize n₁ d₁ = normalize n₂ d₂
rw [← normalize_mul_right _ z₂, ← normalize_mul_left z₂ z₁, Int.mul_comm d₁, h]