-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    normalize n₁ d₁ z₁ = normalize n₂ d₂ z₂ ↔ n₁ * d₂ = n₂ * d₁

Proof state:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Tactic:
have hn₂ := Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left n₂.natAbs d₂

Result:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
hn₂ : ↑(n₂.natAbs.gcd d₂) ∣ n₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Proof state:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
hn₂ : ↑(n₂.natAbs.gcd d₂) ∣ n₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Tactic:
have hd₁ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₁.natAbs d₁

Result:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
hn₂ : ↑(n₂.natAbs.gcd d₂) ∣ n₂
hd₁ : ↑(n₁.natAbs.gcd d₁) ∣ ↑d₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Proof state:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
hn₂ : ↑(n₂.natAbs.gcd d₂) ∣ n₂
hd₁ : ↑(n₁.natAbs.gcd d₁) ∣ ↑d₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Tactic:
have hd₂ := Int.ofNat_dvd.2 <| Nat.gcd_dvd_right n₂.natAbs d₂

Result:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
hn₂ : ↑(n₂.natAbs.gcd d₂) ∣ n₂
hd₁ : ↑(n₁.natAbs.gcd d₁) ∣ ↑d₁
hd₂ : ↑(n₂.natAbs.gcd d₂) ∣ ↑d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Proof state:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
hn₂ : ↑(n₂.natAbs.gcd d₂) ∣ n₂
hd₁ : ↑(n₁.natAbs.gcd d₁) ∣ ↑d₁
hd₂ : ↑(n₂.natAbs.gcd d₂) ∣ ↑d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

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

Result:
no goals

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

Tactic:
simp only [normalize_eq, mk'.injEq] at h

Result:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

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

Tactic:
rw [← normalize_mul_right _ z₂, ← normalize_mul_left z₂ z₁, Int.mul_comm d₁, h]

Result:
no goals

Proof state:
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ normalize n₁ d₁ z₁ = normalize n₂ d₂ z₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

Tactic:
constructor <;> intro h

Result:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : normalize n₁ d₁ z₁ = normalize n₂ d₂ z₂
⊢ 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₁ z₁ = normalize n₂ d₂ z₂

Proof state:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
⊢ n₁ * ↑d₂ = n₂ * ↑d₁

Tactic:
have hn₁ := Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left n₁.natAbs d₁

Result:
case mp
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
h : n₁ / ↑(n₁.natAbs.gcd d₁) = n₂ / ↑(n₂.natAbs.gcd d₂) ∧ d₁ / n₁.natAbs.gcd d₁ = d₂ / n₂.natAbs.gcd d₂
hn₁ : ↑(n₁.natAbs.gcd d₁) ∣ n₁
⊢ n₁ * ↑d₂ = n₂ * ↑d₁