case pos
a b c : ℚ
n d : ℤ
d0 : d = 0
⊢ n /. d = ↑n / ↑d

case neg
a b c : ℚ
n d : ℤ
d0 : ¬d = 0
⊢ n /. d = ↑n / ↑d
a b c : ℚ
n d : ℤ
⊢ n /. d = ↑n / ↑d
by_cases d0 : d = 0
no goals
case neg
a b c : ℚ
n d : ℤ
d0 : ¬d = 0
⊢ n /. d = ↑n / ↑d
simp [division_def, coe_int_eq_divInt, mul_def' one_ne_zero d0]
no goals
case pos
a b c : ℚ
n d : ℤ
d0 : d = 0
⊢ n /. d = ↑n / ↑d
simp [d0, div_zero]