case ofNat
F : Type ?u.33624
ι : Type ?u.33627
α : Type u_1
β : Type ?u.33633
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹

case negSucc
F : Type ?u.33624
ι : Type ?u.33627
α : Type u_1
β : Type ?u.33633
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹
F : Type ?u.33624
ι : Type ?u.33627
α : Type u_1
β : Type ?u.33633
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹
cases' n with n n
no goals
case ofNat
F : Type ?u.33624
ι : Type ?u.33627
α : Type u_1
β : Type ?u.33633
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹
simp [ofInt_eq_cast, cast_inv_nat]
no goals
case negSucc
F : Type ?u.33624
ι : Type ?u.33627
α : Type u_1
β : Type ?u.33633
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹
simp only [ofInt_eq_cast, Int.cast_negSucc, ← Nat.cast_succ, cast_neg, inv_neg, cast_inv_nat]