num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
⊢ normalize (num / ↑g) (den / g) = normalize num den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
⊢ maybeNormalize num den g den_nz reduced = normalize num den
simp only [maybeNormalize_eq, mk_eq_normalize, Int.div_eq_ediv_of_dvd hn]
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ normalize num (den / g * g) = normalize num den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ normalize (num / ↑g) (den / g) = normalize num den
rw [← normalize_mul_right _ this, Int.ediv_mul_cancel hn]
case e_den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ den / g * g = den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ normalize num (den / g * g) = normalize num den
congr 1
no goals
case e_den
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
hn : ↑g ∣ num
hd : g ∣ den
this : g ≠ 0
⊢ den / g * g = den
exact Nat.div_mul_cancel hd