case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d

case neg
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d
by_cases hd : d = 0
no goals
case neg
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
rw [mul_def' hx hd, mul_comm x, divInt_mul_right hx]
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d
rw [hd]
no goals
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0
simp