awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
rw : n + m = n - (↑m.natAbs : ℤ)
rw₁ : n + m = n - -m
rw₂ rw₃ : n + m = n + m
⊢ n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)

Tactic:
rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]

Premises used: LT.lt.le, Int.natAbs_of_nonneg, Int.ofNat_natAbs_of_nonpos, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)

Tactic:
have : n + m = n.natAbs - m.natAbs := by
      rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
this : n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)
inl : selfZPow x B (n + m) = HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * selfZPow x B m
inl₁ :
  selfZPow x B (n + m) =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)
inl₂ :
  selfZPow x B (HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)) =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)
inl₃ :
  mk' B (x ^ n.natAbs) (Submonoid.pow x m.natAbs) =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)
inl₄ :
  HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) (x ^ n.natAbs) : B) (mk' B 1 (Submonoid.pow x m.natAbs)) =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)
inl₅ inl₆ :
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs) =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * mk' B 1 (Submonoid.pow x m.natAbs)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]

Premises used: IsLocalization.mk'_eq_mul_mk'_one, selfZPow_of_neg, map_pow, selfZPow_sub_natCast, selfZPow_of_nonneg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
rw : n + m = m - (↑n.natAbs : ℤ)
rw₁ : n + m = m - -n
rw₂ : n + m = m + n
rw₃ rw₄ : m + n = m + n
⊢ n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)

Tactic:
rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]

Premises used: LT.lt.le, add_comm, Int.natAbs_of_nonneg, Int.ofNat_natAbs_of_nonpos, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)

Tactic:
have : n + m = m.natAbs - n.natAbs := by
      rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
this : n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)
inr : selfZPow x B (n + m) = selfZPow x B n * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inr₁ :
  selfZPow x B (n + m) =
    mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inr₂ :
  selfZPow x B (HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)) =
    mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inr₃ :
  mk' B (x ^ m.natAbs) (Submonoid.pow x n.natAbs) =
    mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inr₄ :
  HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) (x ^ m.natAbs) : B) (mk' B 1 (Submonoid.pow x n.natAbs)) =
    mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inr₅ :
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs * mk' B 1 (Submonoid.pow x n.natAbs) =
    mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inr₆ inr₇ :
  mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs =
    mk' B 1 (Submonoid.pow x n.natAbs) * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm]

Premises used: IsLocalization.mk'_eq_mul_mk'_one, selfZPow_of_neg, map_pow, mul_comm, selfZPow_sub_natCast, selfZPow_of_nonneg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
inr :
  mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) =
    mk' B 1 (HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs))
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rw [selfZPow_of_neg _ _ hn, selfZPow_of_neg _ _ hm, selfZPow_of_neg _ _ (add_neg hn hm),
      Int.natAbs_add_of_nonpos hn.le hm.le, ← mk'_mul, one_mul]

Premises used: add_neg, LT.lt.le, selfZPow_of_neg, Int.natAbs_add_of_nonpos, one_mul, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
inr :
  Submonoid.pow x (n.natAbs + m.natAbs) =
    HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs)
⊢ mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) =
    mk' B 1 (HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs))

Tactic:
congr
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
inr :
  (↑(Submonoid.pow x (n.natAbs + m.natAbs)) : R) =
    (↑(HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs)) : R)
⊢ Submonoid.pow x (n.natAbs + m.natAbs) =
    HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ (↑(Submonoid.pow x (n.natAbs + m.natAbs)) : R) =
    (↑(HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs)) : R)

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
pos : ∀ (hd : d ≤ 0), selfZPow x B d * selfZPow x B (-d) = 1
neg : ∀ (hd : 0 < d), selfZPow x B d * selfZPow x B (-d) = 1
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
by_cases! hd : d ≤ 0
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
pos : 0 ≤ -d
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
rw [selfZPow_of_nonpos x B hd, selfZPow_of_nonneg, ← map_pow, Int.natAbs_neg,
      Submonoid.pow_apply, IsLocalization.mk'_spec, map_one]

Premises used: selfZPow_of_nonpos, map_pow, Submonoid.pow_apply, map_one, selfZPow_of_nonneg, Int.natAbs_neg, IsLocalization.mk'_spec
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
pos : - -d ≤ 0
⊢ 0 ≤ -d

Tactic:
apply nonneg_of_neg_nonpos

Premises used: nonneg_of_neg_nonpos
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
pos pos₁ pos₂ pos₃ : d ≤ 0
⊢ - -d ≤ 0

Tactic:
rwa [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : 0 < d
neg : -d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
rw [selfZPow_of_nonneg x B hd.le, selfZPow_of_nonpos, ← map_pow, Int.natAbs_neg,
      Submonoid.pow_apply, IsLocalization.mk'_spec'_mk, map_one]

Premises used: selfZPow_of_nonpos, LT.lt.le, map_pow, Submonoid.pow_apply, map_one, IsLocalization.mk'_spec'_mk, selfZPow_of_nonneg, Int.natAbs_neg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ -d ≤ 0

Tactic:
nonpos_of_neg_nonneg (le_of_lt ?_)

Premises used: le_of_lt, nonpos_of_neg_nonneg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : 0 < d
neg : 0 < - -d
⊢ -d ≤ 0

Tactic:
refine nonpos_of_neg_nonneg (le_of_lt ?_)

Premises used: le_of_lt, nonpos_of_neg_nonneg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
hd : 0 < d
neg neg₁ neg₂ neg₃ : 0 < d
⊢ 0 < - -d

Tactic:
rwa [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
d : ℤ
rw : selfZPow x B d * selfZPow x B (-d) = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := B) 1 1
⊢ selfZPow x B (-d) * selfZPow x B d = 1

Tactic:
rw [mul_comm, selfZPow_mul_neg x B d]

Premises used: mul_comm, selfZPow_mul_neg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
a : R
b : B
m d : ℤ
rw :
  selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b ↔
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
⊢ selfZPow x B (m - d) * mk' (M := Submonoid.powers x) B a 1 = b ↔
    selfZPow x B m * mk' (M := Submonoid.powers x) 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]

Premises used: mul_assoc, sub_eq_add_neg, IsLocalization.mk', mul_comm, OfNat.ofNat, selfZPow_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
a : R
b : B
m d : ℤ
mp :
  selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b →
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
mpr :
  selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b →
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b ↔
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
⊢ Eq.{u_2 + 1} (α := B)
    ((fun (s : B) ↦ s * selfZPow x B d) (selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d)))
    ((fun (s : B) ↦ s * selfZPow x B d) b)

Tactic:
have := congr_arg (fun s : B => s * selfZPow x B d) h
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) * selfZPow x B d = b * selfZPow x B d
mp :
  ∀
    (this :
      selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * (selfZPow x B (-d) * selfZPow x B d) = b * selfZPow x B d),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
mp₁ :
  ∀
    (this :
      selfZPow x B m * (mk' (M := Submonoid.powers x) B a 1 * (selfZPow x B (-d) * selfZPow x B d)) =
        b * selfZPow x B d),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
mp₂ :
  ∀ (this : selfZPow x B m * (mk' (M := Submonoid.powers x) B a 1 * 1) = b * selfZPow x B d),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
mp₃ :
  ∀ (this : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = b * selfZPow x B d),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
mp₄ mp₅ mp₆ mp₇ :
  ∀ (this : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b

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

Premises used: selfZPow_neg_mul, mul_assoc, mul_comm, mul_one
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
⊢ Eq.{u_2 + 1} (α := B) ((fun (s : B) ↦ s * selfZPow x B (-d)) (selfZPow x B m * mk' (M := Submonoid.powers x) B a 1))
    ((fun (s : B) ↦ s * selfZPow x B (-d)) (selfZPow x B d * b))

Tactic:
have := congr_arg (fun s : B => s * selfZPow x B (-d)) h
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
B : Type u_2
inst_1 : CommSemiring B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
this : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = selfZPow x B d * b * selfZPow x B (-d)
mpr :
  ∀
    (this :
      selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) =
        b * selfZPow x B d * selfZPow x B (-d)),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
mpr₁ :
  ∀
    (this :
      selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) =
        b * (selfZPow x B d * selfZPow x B (-d))),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
mpr₂ :
  ∀ (this : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b * 1),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
mpr₃ mpr₄ mpr₅ mpr₆ :
  ∀ (this : selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b),
    selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b

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

Premises used: mul_assoc, mul_comm, mul_one, selfZPow_mul_neg
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
obtain :
  ∀ (a₀ : R) (y : ↥(Submonoid.powers x))
    (H :
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (↑(a₀, y).2 : R) : B) =
        (algebraMap R B : (a : R) → B) (a₀, y).1),
    ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b

Tactic:
obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b

Premises used: IsLocalization.surj, Submonoid.powers
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H :
  HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (↑(a₀, y).2 : R) : B) = (algebraMap R B : (a : R) → B) (a₀, y).1
obtain :
  ∀ (d : ℕ) (hy : x ^ d = (↑y : R)),
    ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b

Tactic:
obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2

Premises used: Iff.mp, Submonoid.mem_powers_iff, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H :
  HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (↑(a₀, y).2 : R) : B) = (algebraMap R B : (a : R) → B) (a₀, y).1
d : ℕ
hy : x ^ d = (↑y : R)
⊢ IsDomain B

Tactic:
haveI := isDomain_of_le_nonZeroDivisors B
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H :
  HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (↑(a₀, y).2 : R) : B) = (algebraMap R B : (a : R) → B) (a₀, y).1
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
⊢ b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀

Tactic:
simp only [← hy, map_pow] at H

Premises used: map_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
apply : ¬Eq.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) a₀ : B) (0 : B)
apply₁ : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
⊢ a₀ ≠ 0

Tactic:
apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt

Premises used: Iff.mpr, Algebra.algebraMap, Function.mt, injective_iff_map_eq_zero', Iff.mp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
rw : ¬b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = 0
⊢ ¬Eq.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) a₀ : B) (0 : B)

Tactic:
rw [← H]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
apply : Ne.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B) (0 : B)
⊢ ¬b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = 0

Tactic:
apply mul_ne_zero hb (pow_ne_zero _ _)

Premises used: pow_ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
⊢ Ne.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B) (0 : B)

Tactic:
IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
          (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
          (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)

Premises used: Iff.mpr, powers_le_nonZeroDivisors_of_noZeroDivisors, mem_nonZeroDivisors_iff_ne_zero, Irreducible.ne_zero, IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
⊢ Ne.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B) (0 : B)

Tactic:
exact
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
          (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
          (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)

Premises used: Iff.mpr, powers_le_nonZeroDivisors_of_noZeroDivisors, mem_nonZeroDivisors_iff_ne_zero, Irreducible.ne_zero, IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)

Tactic:
IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)

Premises used: IsLocalization.injective, powers_le_nonZeroDivisors_of_noZeroDivisors, Irreducible.ne_zero