a b c : ℚ
n : ℤ
d : ℕ
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
a b c : ℚ
n : ℤ
d : ℕ
⊢ mkRat n d = ↑n / ↑d
simp [mkRat]
case pos
a b c : ℚ
n : ℤ
d : ℕ
h : d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d

case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
a b c : ℚ
n : ℤ
d : ℕ
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
by_cases d = 0
no goals
case pos
a b c : ℚ
n : ℤ
d : ℕ
h : d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
simp [h]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d = ↑n * Rat.inv ↑d
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
simp [h, HDiv.hDiv, Rat.div, Div.div]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d = ↑n * Rat.inv ↑d
unfold Rat.inv
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
have h₁ : 0 < d := Nat.pos_iff_ne_zero.2 h
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
h₂ : ¬↑d < 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
have h₂ : ¬ (d : ℤ) < 0 := by simp
no goals
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
h₂ : ¬↑d < 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
simp [h, h₁, h₂, ←Rat.normalize_eq_mk', Rat.normalize_eq_mkRat, ← mkRat_one,
  Rat.mkRat_mul_mkRat]
no goals
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ ¬↑d < 0
simp