-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_pow_sub (a : R) (b : B) (m d : ℤ) :
    selfZPow x B (m - d) * mk' B a (1 : Submonoid.powers x) = b ↔
      selfZPow x B m * mk' B a (1 : Submonoid.powers x) = selfZPow x B d * b

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
simp only at this

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
simp only at this

Result:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
rw [sub_eq_add_neg, selfZPow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc]

Result:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
have := congr_arg (fun s : B => s * selfZPow x B d) h

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
have := congr_arg (fun s : B => s * selfZPow x B (-d)) h

Result:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Proof state:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring 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