[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : ↑n = 0
⊢ n = 0
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0
[PROOFSTEP]
erw [Int.cast_ofNat] at h 
[GOAL]
case ofNat
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑a✝ = 0
⊢ ofNat a✝ = 0
[PROOFSTEP]
exact congr_arg _ (Nat.cast_eq_zero.1 h)
[GOAL]
case negSucc
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0
[PROOFSTEP]
rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h 
[GOAL]
case negSucc
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : a✝ + 1 = 0
⊢ -[a✝+1] = 0
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : n = 0
⊢ ↑n = 0
[PROOFSTEP]
rw [h, cast_zero]
[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ ↑m = ↑n ↔ m = n
[PROOFSTEP]
rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
[GOAL]
α : Type u_1
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = 1 ↔ n = 1
[PROOFSTEP]
rw [← cast_one, cast_inj]
[GOAL]
α : Type u_1
k : Type u_2
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
α : Type u_1
k : Type u_2
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0
[PROOFSTEP]
simp [Int.ediv_zero]
[GOAL]
case inr
α : Type u_1
k : Type u_2
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
exact cast_div n_dvd (cast_ne_zero.mpr hn)
