n : Int
d : Nat
z : d ≠ 0
n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
h : normalize n d = mk' n' d'
this : ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d).num * ↑d_1 ∧ d = (normalize n d).den * d_1
⊢ ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n : Int
d : Nat
z : d ≠ 0
n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
h : normalize n d = mk' n' d'
⊢ ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
have := normalize_num_den' n d z
no goals
n : Int
d : Nat
z : d ≠ 0
n' : Int
d' : Nat
z' : d' ≠ 0
c : Nat.coprime (Int.natAbs n') d'
h : normalize n d = mk' n' d'
this : ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d).num * ↑d_1 ∧ d = (normalize n d).den * d_1
⊢ ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
rwa [h] at this