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
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b ↔ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
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
a : R
b : B
m d : ℤ
⊢ selfZpow x B (m - d) * mk' B a 1 = b ↔ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
rw [sub_eq_add_neg, selfZpow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc]
case mp
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
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b → selfZpow x B m * mk' B a 1 = selfZpow x B d * b

case mpr
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
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b → selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
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
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b ↔ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
constructor
case mp
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
case mp
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
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b → selfZpow x B m * mk' B a 1 = selfZpow x B d * b
intro h
case mp
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
this : (fun s => s * selfZpow x B d) (selfZpow x B m * mk' B a 1 * selfZpow x B (-d)) = (fun s => s * selfZpow x B d) b
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
case mp
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
have := congr_arg (fun s : B => s * selfZpow x B d) h
case mp
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
this : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) * selfZpow x B d = b * selfZpow x B d
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
case mp
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
this : (fun s => s * selfZpow x B d) (selfZpow x B m * mk' B a 1 * selfZpow x B (-d)) = (fun s => s * selfZpow x B d) b
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
simp only at this
no goals
case mp
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
this : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) * selfZpow x B d = b * selfZpow x B d
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b
rwa [mul_assoc, mul_assoc, selfZpow_neg_mul, mul_one, mul_comm b _] at this
case mpr
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
case mpr
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
a : R
b : B
m d : ℤ
⊢ selfZpow x B m * mk' B a 1 = selfZpow x B d * b → selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
intro h
case mpr
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
this :
  (fun s => s * selfZpow x B (-d)) (selfZpow x B m * mk' B a 1) = (fun s => s * selfZpow x B (-d)) (selfZpow x B d * b)
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
case mpr
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
have := congr_arg (fun s : B => s * selfZpow x B (-d)) h
case mpr
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
this : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = selfZpow x B d * b * selfZpow x B (-d)
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
case mpr
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
this :
  (fun s => s * selfZpow x B (-d)) (selfZpow x B m * mk' B a 1) = (fun s => s * selfZpow x B (-d)) (selfZpow x B d * b)
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
simp only at this
no goals
case mpr
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
a : R
b : B
m d : ℤ
h : selfZpow x B m * mk' B a 1 = selfZpow x B d * b
this : selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = selfZpow x B d * b * selfZpow x B (-d)
⊢ selfZpow x B m * mk' B a 1 * selfZpow x B (-d) = b
rwa [mul_comm _ b, mul_assoc b _ _, selfZpow_mul_neg, mul_one] at this