case inl
R : Type ?u.1348
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_1
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m : ℕ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0

case inr
R : Type ?u.1348
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_1
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
R : Type ?u.1348
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_1
inst✝¹ : DivisionSemiring 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
R : Type ?u.1348
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_1
inst✝¹ : DivisionSemiring k
inst✝ : CharZero k
m : ℕ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0
simp
no goals
case inr
R : Type ?u.1348
inst✝³ : AddMonoidWithOne R
inst✝² : CharZero R
k : Type u_1
inst✝¹ : DivisionSemiring 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.2 hn)