[GOAL]
α : Type u_1
inst✝ : Ring α
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = ↑a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n : ℕ
⊢ ↑(Int.negOfNat n) = -↑n
[PROOFSTEP]
simp [Int.negOfNat_eq, Int.cast_neg]
[GOAL]
α : Type u_1
inst✝ : Ring α
a✝ : ℕ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑(Int.ofNat a✝) * ⅟↑1 = ↑a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ 1 * ↑1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝) * ⅟↑1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num✝ * ⅟↑1 = ↑num✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ 1 * ↑1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑n✝ = ↑n✝ * ⅟↑1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
n : ℤ
d : ℕ
inst✝ : DivisionRing α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = Rat.rawCast n d
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d = -(↑n / ↑d)
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.ofNat n) * ⅟↑d = ↑n / ↑d
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ Rat.rawCast n d = ↑n * ⅟↑d
[PROOFSTEP]
simp [div_eq_mul_inv]
