num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
⊢ (if hg : g = 1 then mk' num den else mk' (Int.div num ↑g) (den / g)) = mk' (Int.div num ↑g) (den / g)
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
⊢ maybeNormalize num den g den_nz reduced = mk' (Int.div num ↑g) (den / g)
unfold maybeNormalize
case inl
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
h✝ : g = 1
⊢ mk' num den = mk' (Int.div num ↑g) (den / g)

case inr
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
h✝ : ¬g = 1
⊢ mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
⊢ (if hg : g = 1 then mk' num den else mk' (Int.div num ↑g) (den / g)) = mk' (Int.div num ↑g) (den / g)
split
case inl
num : Int
den : Nat
den_nz : den / 1 ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑1)) (den / 1)
⊢ mk' num den = mk' (Int.div num ↑1) (den / 1)
case inl
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
h✝ : g = 1
⊢ mk' num den = mk' (Int.div num ↑g) (den / g)
subst g
no goals
case inl
num : Int
den : Nat
den_nz : den / 1 ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑1)) (den / 1)
⊢ mk' num den = mk' (Int.div num ↑1) (den / 1)
simp
no goals
case inr
num : Int
den g : Nat
den_nz : den / g ≠ 0
reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
h✝ : ¬g = 1
⊢ mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)
rfl