awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ
r_1 : (a : (↑(↑s : Set R) : Type u_1)) → R
eq_1 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a)
N_1 : ℕ := s.attach.sup n
r_2 : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ (N_1 - n a) * r_1 a
eq_2 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N_1) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_2 a)
N'_1 : (a b : (↑(↑s : Set R) : Type u_1)) → ℕ
hN' :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r_2 a * (↑b : R) ^ N_1) =
      ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r_2 b * (↑a : R) ^ N_1)
N' : ℕ :=
  (s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
    N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)
eq2 :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N' * (r_2 a * (↑b : R) ^ N_1) = ((↑a : R) * (↑b : R)) ^ N' * (r_2 b * (↑a : R) ^ N_1)
N : ℕ := N' + N_1
r : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ N' * r_2 a
eq :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)
⊢ ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
have eq2₁ : ∀ (a b : (↑(↑s : Set R) : Type u_1)), r a * (↑b : R) ^ N = r b * (↑a : R) ^ N
Tactic: have eq2 a b : r a * b ^ N = r b * a ^ N := by
    rw [pow_add, mul_mul_mul_comm, ← mul_pow, eq2,
      mul_comm a.1, mul_pow, mul_mul_mul_comm, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ
r_1 : (a : (↑(↑s : Set R) : Type u_1)) → R
eq_1 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a)
N_1 : ℕ := s.attach.sup n
r_2 : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ (N_1 - n a) * r_1 a
eq_2 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N_1) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_2 a)
N'_1 : (a b : (↑(↑s : Set R) : Type u_1)) → ℕ
hN' :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r_2 a * (↑b : R) ^ N_1) =
      ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r_2 b * (↑a : R) ^ N_1)
N' : ℕ :=
  (s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
    N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)
eq2_1 :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N' * (r_2 a * (↑b : R) ^ N_1) = ((↑a : R) * (↑b : R)) ^ N' * (r_2 b * (↑a : R) ^ N_1)
N : ℕ := N' + N_1
r : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ N' * r_2 a
eq :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)
eq2 : ∀ (a b : (↑(↑s : Set R) : Type u_1)), r a * (↑b : R) ^ N = r b * (↑a : R) ^ N
⊢ ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
have have : ∀ (c : (↑(↑s : Set R) : Type u_1) → R)
  (eq1 : Eq.{u_1 + 1} (α := R) (∑ i : (↑(↑s : Set R) : Type u_1), c i • (↑i : R) ^ N) 1),
  ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
Tactic: have ⟨c, eq1⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp <|
    (Ideal.eq_top_iff_one _).mp <| (Set.image_eq_range _ _ ▸ Ideal.span_pow_eq_top _ span_eq N)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Finset R
f : (a : (↑(↑s : Set R) : Type u_1)) → Away (↑a : R)
h :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    Eq (α := Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayRight (↑a : R) (↑b : R) : (a_1 : Away (↑a : R)) → Away ((↑a : R) * (↑b : R))) (f a) :
        Away ((↑a : R) * (↑b : R)))
      ((Away.awayToAwayLeft (↑b : R) (↑a : R) : (a_1 : Away (↑b : R)) → Away ((↑a : R) * (↑b : R))) (f b) :
        Away ((↑a : R) * (↑b : R)))
mem : Membership.mem (γ := Ideal R) (Ideal.span (↑s : Set R)) 1
span_eq : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
n : (a : (↑(↑s : Set R) : Type u_1)) → ℕ
r_1 : (a : (↑(↑s : Set R) : Type u_1)) → R
eq_1 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) (n a) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_1 a)
N_1 : ℕ := s.attach.sup n
r_2 : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ (N_1 - n a) * r_1 a
eq_2 :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N_1) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r_2 a)
N'_1 : (a b : (↑(↑s : Set R) : Type u_1)) → ℕ
hN' :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r_2 a * (↑b : R) ^ N_1) =
      ((↑a : R) * (↑b : R)) ^ N'_1 a b * (r_2 b * (↑a : R) ^ N_1)
N' : ℕ :=
  (s ×ˢ s).attach.sup fun (a : ↥(s ×ˢ s)) ↦
    N'_1 (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).1 ⋯)
      (Subtype.mk (p := fun (x : R) ↦ x ∈ (↑s : Set R)) (↑a : R × R).2 ⋯)
eq2_1 :
  ∀ (a b : (↑(↑s : Set R) : Type u_1)),
    ((↑a : R) * (↑b : R)) ^ N' * (r_2 a * (↑b : R) ^ N_1) = ((↑a : R) * (↑b : R)) ^ N' * (r_2 b * (↑a : R) ^ N_1)
N : ℕ := N' + N_1
r : (a : (↑(↑s : Set R) : Type u_1)) → R := fun (a : (↑(↑s : Set R) : Type u_1)) ↦ (↑a : R) ^ N' * r_2 a
eq :
  ∀ (a : (↑(↑s : Set R) : Type u_1)),
    HMul.hMul (β := Away (↑a : R)) (f a)
        ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) ((↑a : R) ^ N) : Away (↑a : R)) =
      (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (r a)
eq2 : ∀ (a b : (↑(↑s : Set R) : Type u_1)), r a * (↑b : R) ^ N = r b * (↑a : R) ^ N
c : (↑(↑s : Set R) : Type u_1) → R
eq1 : Eq.{u_1 + 1} (α := R) (∑ i : (↑(↑s : Set R) : Type u_1), c i • (↑i : R) ^ N) 1
⊢ ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a
have refine : ∀ (a : (↑(↑s : Set R) : Type u_1)),
  (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (∑ b : (↑(↑s : Set R) : Type u_1), c b * r b) *
      HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) N =
    f a * HPow.hPow (α := Away (↑a : R)) ((algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) (↑a : R)) N
Tactic: refine ⟨∑ b, c b * r b, fun a ↦ ((Away.algebraMap_isUnit a.1).pow N).mul_left_inj.mp ?_⟩
-- 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 : ℤ
hn : n ≤ 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
have pos : ∀ (hn0 : n = 0), selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
Tactic: by_cases hn0 : n = 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
n : ℤ
hn : n ≤ 0
pos : ∀ (hn0 : n = 0), selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
have neg : ∀ (hn0 : ¬n = 0), selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
Tactic: by_cases hn0 : n = 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
n m : ℕ
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos : ∀ (h : m ≤ n), selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
Tactic: by_cases! h : m ≤ n
-- 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 : ℕ
pos : ∀ (h : m ≤ n), selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have neg : ∀ (h : n < m), selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
Tactic: by_cases! h : m ≤ n
-- 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 : m ≤ n
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos : HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
    ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
  (algebraMap R B : (a : R) → B) (x ^ n)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₁ : HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
    ((algebraMap R B : (a : R) → B)
        (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) sorry) :
          R) :
      B) =
  (algebraMap R B : (a : R) → B) (x ^ n)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₂ : HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ))) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
  (algebraMap R B : (a : R) → B) (x ^ n)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₂ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₃ : HMul.hMul (β := B) (selfZPow x B (↑(n - m) : ℤ)) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
  (algebraMap R B : (a : R) → B) (x ^ n)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₂ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₃ :
  HMul.hMul (β := B) (selfZPow x B (↑(n - m) : ℤ)) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₄ : HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n - m))
    ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
  (algebraMap R B : (a : R) → B) (x ^ n)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₂ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₃ :
  HMul.hMul (β := B) (selfZPow x B (↑(n - m) : ℤ)) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₄ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n - m))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₅ : HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m)) : B)
    ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
  (algebraMap R B : (a : R) → B) (x ^ n)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₂ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₃ :
  HMul.hMul (β := B) (selfZPow x B (↑(n - m) : ℤ)) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₄ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n - m))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₅ :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m)) : B)
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₆ : Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m) * x ^ m) : B)
  ((algebraMap R B : (a : R) → B) (x ^ n) : B)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₂ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₃ :
  HMul.hMul (β := B) (selfZPow x B (↑(n - m) : ℤ)) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₄ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n - m))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₅ :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m)) : B)
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₆ :
  Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m) * x ^ m) : B)
    ((algebraMap R B : (a : R) → B) (x ^ n) : B)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₇ : Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m + m)) : B)
  ((algebraMap R B : (a : R) → B) (x ^ n) : B)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel 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
n m : ℕ
h : m ≤ n
pos :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (↑(Submonoid.pow x m) : R) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₁ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B)
          (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) (x ^ m) ⋯) :
            R) :
        B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₂ :
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₃ :
  HMul.hMul (β := B) (selfZPow x B (↑(n - m) : ℤ)) ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₄ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) (n - m))
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₅ :
  HMul.hMul (α := B) (β := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m)) : B)
      ((algebraMap R B : (a : R) → B) (x ^ m) : B) =
    (algebraMap R B : (a : R) → B) (x ^ n)
pos₆ :
  Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m) * x ^ m) : B)
    ((algebraMap R B : (a : R) → B) (x ^ n) : B)
pos₇ :
  Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ (n - m + m)) : B)
    ((algebraMap R B : (a : R) → B) (x ^ n) : B)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
have pos₈ : Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ n) : B) ((algebraMap R B : (a : R) → B) (x ^ n) : B)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h,
      selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]