[GOAL]
R✝ : Type ?u.74090
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 1 = 1
[PROOFSTEP]
simp
[GOAL]
R✝ : Type ?u.76702
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
⊢ Int.rawCast (Int.negOfNat 1) = -1
[PROOFSTEP]
simp [Int.negOfNat_eq]
[GOAL]
R✝ : Type ?u.78211
inst✝² : CommSemiring R✝
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nat.AtLeastTwo n
⊢ Int.rawCast (Int.negOfNat n) = -OfNat.ofNat n
[PROOFSTEP]
simp [Int.negOfNat_eq, OfNat.ofNat]
[GOAL]
R✝ : Type ?u.80333
inst✝¹ : CommSemiring R✝
n : ℤ
d : ℕ
R : Type u_1
inst✝ : DivisionRing R
⊢ Rat.rawCast n d = ↑n / ↑d
[PROOFSTEP]
simp
