case inl
α : Type ?u.3615
k : Type u_1
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0

case inr
α : Type ?u.3615
k : Type u_1
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
α : Type ?u.3615
k : Type u_1
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n
rcases eq_or_ne n 0 with (rfl | hn)
no goals
case inl
α : Type ?u.3615
k : Type u_1
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0
simp [Int.ediv_zero]
no goals
case inr
α : Type ?u.3615
k : Type u_1
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
exact cast_div n_dvd (cast_ne_zero.mpr hn)