case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
n_nonzero : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
rcases n_dvd with ⟨k, rfl⟩
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
have : n ≠ 0 := by
  rintro rfl
  simp at n_nonzero
no goals
case intro
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
rw [Int.mul_ediv_cancel_left _ this, mul_comm n k, Int.cast_mul, mul_div_cancel _ n_nonzero]
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
n_nonzero : ↑0 ≠ 0
⊢ False
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
n_nonzero : ↑n ≠ 0
k : ℤ
⊢ n ≠ 0
rintro rfl
no goals
α : Type u_1
inst✝ : DivisionRing α
k : ℤ
n_nonzero : ↑0 ≠ 0
⊢ False
simp at n_nonzero