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 m : ℕ
h : m ≤ n
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

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 m : ℕ
h : ¬m ≤ n
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
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 m : ℕ
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
by_cases h : m ≤ n
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 m : ℕ
h : m ≤ n
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
  selfZpow_coe_nat, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]
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 m : ℕ
h : ¬m ≤ n
⊢ ↑(algebraMap R B) (↑(Submonoid.pow x m) * 1) = ↑(algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ 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 m : ℕ
h : ¬m ≤ n
⊢ selfZpow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)
rw [← neg_sub, ← Int.ofNat_sub (le_of_not_le h), selfZpow_neg_coe_nat,
  IsLocalization.mk'_eq_iff_eq]
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 m : ℕ
h : ¬m ≤ n
⊢ ↑(algebraMap R B) (↑(Submonoid.pow x m) * 1) = ↑(algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)
simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel (le_of_not_le h)]