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
d : ℤ
hd : d ≤ 0
⊢ selfZpow x B d * selfZpow x B (-d) = 1

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
d : ℤ
hd : ¬d ≤ 0
⊢ selfZpow x B d * selfZpow x B (-d) = 1
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
d : ℤ
⊢ selfZpow x B d * selfZpow x B (-d) = 1
by_cases hd : d ≤ 0
case pos.hn
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
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d
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
d : ℤ
hd : d ≤ 0
⊢ selfZpow x B d * selfZpow x B (-d) = 1
erw [selfZpow_of_nonpos x B hd, selfZpow_of_nonneg, ← map_pow, Int.natAbs_neg,
  IsLocalization.mk'_spec, map_one]
case pos.hn.a
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
d : ℤ
hd : d ≤ 0
⊢ - -d ≤ 0
case pos.hn
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
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d
apply nonneg_of_neg_nonpos
no goals
case pos.hn.a
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
d : ℤ
hd : d ≤ 0
⊢ - -d ≤ 0
rwa [neg_neg]
case neg.hn
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
d : ℤ
hd : ¬d ≤ 0
⊢ -d ≤ 0
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
d : ℤ
hd : ¬d ≤ 0
⊢ selfZpow x B d * selfZpow x B (-d) = 1
erw [selfZpow_of_nonneg x B (le_of_not_le hd), selfZpow_of_nonpos, ← map_pow, Int.natAbs_neg,
  @IsLocalization.mk'_spec' R _ (Submonoid.powers x) B _ _ _ 1 (Submonoid.pow x d.natAbs),
  map_one]
case neg.hn
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
d : ℤ
hd : ¬d ≤ 0
⊢ 0 < - -d
case neg.hn
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
d : ℤ
hd : ¬d ≤ 0
⊢ -d ≤ 0
refine' nonpos_of_neg_nonneg (le_of_lt _)
no goals
case neg.hn
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
d : ℤ
hd : ¬d ≤ 0
⊢ 0 < - -d
rwa [neg_neg, ← not_le]