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