case inl
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n : ℕ
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
rcases eq_or_ne d 0 with (rfl | hd)
case hd
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑d ≠ 0

case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
replace hd : (d : α) ≠ 0
no goals
case inr
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
rw [cast_div hm, cast_div hn, div_div_div_cancel_right _ hd] <;> exact hd
no goals
case inl
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n : ℕ
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n
simp [zero_dvd_iff.mp hm]
no goals
case hd
α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
m n d : ℕ
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑d ≠ 0
norm_cast