awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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
Tactic: rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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
Tactic: rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ 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))
have inr : Submonoid.pow x (n.natAbs + m.natAbs) =
  HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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) =
    HMul.hMul (α := ↥(Submonoid.powers x)) (Submonoid.pow x n.natAbs) (Submonoid.pow x m.natAbs)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 : ℤ
⊢ selfZPow x B d * selfZPow x B (-d) = 1
have pos : ∀ (hd : d ≤ 0), selfZPow x B d * selfZPow x B (-d) = 1
Tactic: by_cases! hd : d ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B d * selfZPow x B (-d) = 1
have neg : ∀ (hd : 0 < d), selfZPow x B d * selfZPow x B (-d) = 1
Tactic: by_cases! hd : d ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B d * selfZPow x B (-d) = 1
have pos : 0 ≤ -d
Tactic: rw [selfZPow_of_nonpos x B hd, selfZPow_of_nonneg, ← map_pow, Int.natAbs_neg,
      Submonoid.pow_apply, IsLocalization.mk'_spec, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ 0 ≤ -d
have pos : - -d ≤ 0
Tactic: apply nonneg_of_neg_nonpos
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B d * selfZPow x B (-d) = 1
have neg : -d ≤ 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
have neg : 0 < - -d
Tactic: refine nonpos_of_neg_nonneg (le_of_lt ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 : ℤ
⊢ selfZPow x B (-d) * selfZPow x B d = 1
have rw : selfZPow x B d * selfZPow x B (-d) = 1
Tactic: rw [mul_comm, selfZPow_mul_neg x B d]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B (-d) * selfZPow x B d = 1
have rw₁ : Eq.{u_2 + 1} (α := B) 1 1
Tactic: rw [mul_comm, selfZPow_mul_neg x B d]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 : ℤ
⊢ 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
have 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
Tactic: rw [sub_eq_add_neg, selfZPow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 : ℤ
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
have 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
Tactic: rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
have 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
Tactic: rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
have 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
Tactic: rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
have 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
Tactic: rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 = selfZPow x B d * b
have 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
Tactic: rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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)
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
have 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
Tactic: rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
have 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
Tactic: rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
have 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
Tactic: rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ selfZPow x B m * mk' (M := Submonoid.powers x) B a 1 * selfZPow x B (-d) = b
have 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
Tactic: rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
have 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
Tactic: obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
have 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
Tactic: obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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)
⊢ a₀ ≠ 0
have this : IsDomain B
Tactic: haveI := isDomain_of_le_nonZeroDivisors B
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)