case ofNat
F : Type ?u.33869
ι : Type ?u.33872
α : Type u_1
β : Type ?u.33878
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs (ofNat a✝)) = ↑(abs (ofNat a✝))

case negSucc
F : Type ?u.33869
ι : Type ?u.33872
α : Type u_1
β : Type ?u.33878
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
F : Type ?u.33869
ι : Type ?u.33872
α : Type u_1
β : Type ?u.33878
inst✝ : LinearOrderedRing α
a b n : ℤ
⊢ ↑(natAbs n) = ↑(abs n)
cases n
no goals
case ofNat
F : Type ?u.33869
ι : Type ?u.33872
α : Type u_1
β : Type ?u.33878
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs (ofNat a✝)) = ↑(abs (ofNat a✝))
simp
no goals
case negSucc
F : Type ?u.33869
ι : Type ?u.33872
α : Type u_1
β : Type ?u.33878
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs -[a✝+1]) = ↑(abs -[a✝+1])
rw [abs_eq_natAbs, natAbs_negSucc, cast_succ, cast_ofNat, cast_succ]