case zero
F : Type ?u.32377
ι : Type ?u.32380
α : Type u_1
β : Type ?u.32386
inst✝ : DivisionRing α
⊢ ↑(↑Nat.zero)⁻¹ = (↑Nat.zero)⁻¹

case succ
F : Type ?u.32377
ι : Type ?u.32380
α : Type u_1
β : Type ?u.32386
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Nat.succ n))⁻¹ = (↑(Nat.succ n))⁻¹
F : Type ?u.32377
ι : Type ?u.32380
α : Type u_1
β : Type ?u.32386
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹
cases' n with n
no goals
case succ
F : Type ?u.32377
ι : Type ?u.32380
α : Type u_1
β : Type ?u.32386
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Nat.succ n))⁻¹ = (↑(Nat.succ n))⁻¹
rw [cast_def, inv_coe_nat_num, inv_coe_nat_den, if_neg n.succ_ne_zero,
  Int.sign_eq_one_of_pos (Nat.cast_pos.mpr n.succ_pos), Int.cast_one, one_div]
no goals
case zero
F : Type ?u.32377
ι : Type ?u.32380
α : Type u_1
β : Type ?u.32386
inst✝ : DivisionRing α
⊢ ↑(↑Nat.zero)⁻¹ = (↑Nat.zero)⁻¹
simp