case pos
R : Type u_2
inst✝³ : CommRing R
x : R
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))

case neg
R : Type u_2
inst✝³ : CommRing R
x : R
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
R : Type u_2
inst✝³ : CommRing R
x : R
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
by_cases hn0 : n = 0
no goals
case pos
R : Type u_2
inst✝³ : CommRing R
x : R
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
simp [hn0, selfZpow_zero, Submonoid.pow_apply]
no goals
case neg
R : Type u_2
inst✝³ : CommRing R
x : R
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZpow x B n = mk' B 1 (Submonoid.pow x (Int.natAbs n))
simp [selfZpow_of_neg _ _ (lt_of_le_of_ne hn hn0)]