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 : ℕ
h : n < m
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have neg : Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) ((↑(Submonoid.pow x m) : R) * 1) : B)
  ((algebraMap R B : (a : R) → B) ((↑(Submonoid.pow x (m - n)) : R) * x ^ n) : B)
Tactic: rw [← neg_sub, ← Int.ofNat_sub h.le, selfZPow_neg_natCast, IsLocalization.mk'_eq_iff_eq]
-- 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 : ℤ
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inl : ∀ (hn : 0 ≤ n), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Tactic: rcases le_or_gt 0 n with hn | hn
-- 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 : ℤ
inl : ∀ (hn : 0 ≤ n), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inr : ∀ (hn : n < 0), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Tactic: rcases le_or_gt 0 n with hn | hn
-- 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 : 0 ≤ n
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inl : ∀ (hm : 0 ≤ m), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Tactic: rcases le_or_gt 0 m with hm | hm
-- 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 : 0 ≤ n
inl : ∀ (hm : 0 ≤ m), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inl₁ : ∀ (hm : m < 0), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Tactic: rcases le_or_gt 0 m with hm | hm
-- 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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inr : ∀ (hm : 0 ≤ m), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Tactic: rcases le_or_gt 0 m with hm | hm
-- 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
inr : ∀ (hm : 0 ≤ m), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inr₁ : ∀ (hm : m < 0), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Tactic: rcases le_or_gt 0 m with hm | hm
-- 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 : 0 ≤ n
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inl : selfZPow x B (n + m) = HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * selfZPow x B m
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm,
      selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add]
-- 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 : 0 ≤ n
hm : 0 ≤ m
inl : selfZPow x B (n + m) = HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * selfZPow x B m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inl₁ : selfZPow x B (n + m) =
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs *
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm,
      selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add]
-- 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 : 0 ≤ n
hm : 0 ≤ m
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 *
      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 inl₂ : HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n + m).natAbs =
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs *
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm,
      selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add]
-- 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 : 0 ≤ n
hm : 0 ≤ m
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 *
      HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inl₂ :
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n + m).natAbs =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) 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 inl₃ : HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n.natAbs + m.natAbs) =
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs *
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm,
      selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add]
-- 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 : 0 ≤ n
hm : 0 ≤ m
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 *
      HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inl₂ :
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n + m).natAbs =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs *
      HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
inl₃ :
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n.natAbs + m.natAbs) =
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) 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 inl₄ : HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs *
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs =
  HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs *
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m.natAbs
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_nonneg _ _ hm,
      selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add]
-- 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 : 0 ≤ n
hm : m < 0
⊢ n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)
have rw : n + m = n - (↑m.natAbs : ℤ)
Tactic: rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
-- 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 : 0 ≤ n
hm : m < 0
rw : n + m = n - (↑m.natAbs : ℤ)
⊢ n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)
have rw₁ : n + m = n - -m
Tactic: rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
-- 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 : 0 ≤ n
hm : m < 0
rw : n + m = n - (↑m.natAbs : ℤ)
rw₁ : n + m = n - -m
⊢ n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)
have rw₂ : n + m = n + m
Tactic: rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]
-- 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
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have this : 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]
-- 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 : 0 ≤ n
hm : m < 0
this : n + m = HSub.hSub (α := ℤ) (↑n.natAbs : ℤ) (↑m.natAbs : ℤ)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inl : selfZPow x B (n + m) = HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs * 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]
-- 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 : 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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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)
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]
-- 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 : 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)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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)
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]
-- 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 : 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)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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)
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]
-- 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 : 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)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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)
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]
-- 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 : 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)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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)
Tactic: rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow]
-- 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
⊢ n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)
have rw : n + m = m - (↑n.natAbs : ℤ)
Tactic: rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_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
rw : n + m = m - (↑n.natAbs : ℤ)
⊢ n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)
have rw₁ : n + m = m - -n
Tactic: rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_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
rw : n + m = m - (↑n.natAbs : ℤ)
rw₁ : n + m = m - -n
⊢ n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)
have rw₂ : n + m = m + n
Tactic: rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_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
rw : n + m = m - (↑n.natAbs : ℤ)
rw₁ : n + m = m - -n
rw₂ : n + m = m + n
⊢ n + m = HSub.hSub (α := ℤ) (↑m.natAbs : ℤ) (↑n.natAbs : ℤ)
have rw₃ : m + n = m + n
Tactic: rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]
-- 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
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have this : 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]
-- 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 : ℤ)
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have inr : selfZPow x B (n + m) = selfZPow x B n * 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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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
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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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
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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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
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
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
have 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
Tactic: rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast,
      IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm]