awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 :
  ∀ (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
⊢ ∀ (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)

Tactic:
have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
    rw [map_mul, ← eq, mul_left_comm, ← map_mul, ← pow_add]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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)
⊢ ∀ (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]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ ∃ (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)
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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

Tactic:
⟨∑ b, c b * r b, fun a ↦ ((Away.algebraMap_isUnit a.1).pow N).mul_left_inj.mp ?_⟩

Premises used: HMul.hMul, Finset.univ, IsUnit.pow, Exists.intro, Iff.mp, IsUnit.mul_left_inj, Subtype.val, Finset.sum, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ ∃ (x : R), ∀ (a : (↑(↑s : Set R) : Type u_1)), (algebraMap R (Away (↑a : R)) : (a_1 : R) → Away (↑a : R)) x = f a

Tactic:
refine ⟨∑ b, c b * r b, fun a ↦ ((Away.algebraMap_isUnit a.1).pow N).mul_left_inj.mp ?_⟩
-- 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 : ℤ
hn : 0 ≤ n
⊢ selfZPow x B n = HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) n.natAbs

Tactic:
dif_pos hn

Premises used: selfZPow, dif_pos
-- 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 : ℕ
⊢ selfZPow x B (↑d : ℤ) = HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d

Tactic:
selfZPow_of_nonneg _ _ (Int.natCast_nonneg d)

Premises used: Int.natAbs, selfZPow_of_nonneg, Int.natCast_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
⊢ selfZPow x B 0 = 1

Tactic:
simp [selfZPow_of_nonneg _ _ le_rfl]

Premises used: le_rfl, 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 : ℤ
hn : n < 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
dif_neg hn.not_ge

Premises used: selfZPow, dif_neg, LT.lt.not_ge
-- 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 : ℤ
hn : n ≤ 0
pos : ∀ (hn0 : n = 0), selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)
neg : ∀ (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)

Tactic:
by_cases hn0 : n = 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
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
simp [hn0, selfZPow_zero, Submonoid.pow_apply]

Premises used: selfZPow_zero, Submonoid.pow_apply
-- 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 : ℤ
hn : n ≤ 0
hn0 : ¬n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
simp [selfZPow_of_neg _ _ (lt_of_le_of_ne hn hn0)]

Premises used: selfZPow_of_neg, lt_of_le_of_ne
-- 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 : ℕ
⊢ selfZPow x B (-(↑d : ℤ)) = mk' B 1 (Submonoid.pow x d)

Tactic:
simp [selfZPow_of_nonpos _ _ (neg_nonpos.mpr (Int.natCast_nonneg d))]

Premises used: Iff.mpr, selfZPow_of_nonpos, neg_nonpos, Int.natCast_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 : ℕ
pos : ∀ (h : m ≤ n), selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)
neg : ∀ (h : n < m), 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)

Tactic:
by_cases! h : m ≤ n
-- 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 : ℕ
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)
pos₈ pos₉ :
  Eq.{u_2 + 1} (α := B) ((algebraMap R B : (a : R) → B) (x ^ n) : 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)

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]

Premises used: Subtype.coe_mk, Int.ofNat_sub, pow_add, map_pow, Submonoid.pow_apply, map_mul, Nat.sub_add_cancel, selfZPow_natCast, IsLocalization.eq_mk'_iff_mul_eq
-- 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 : ℕ
h : n < m
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)
⊢ selfZPow x B (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
rw [← neg_sub, ← Int.ofNat_sub h.le, selfZPow_neg_natCast, IsLocalization.mk'_eq_iff_eq]

Premises used: neg_sub, Int.ofNat_sub, LT.lt.le, IsLocalization.mk'_eq_iff_eq, selfZPow_neg_natCast
-- 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 : ℕ
h : n < m
⊢ 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:
simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel h.le]

Premises used: pow_add, LT.lt.le, Submonoid.pow_apply, Nat.sub_add_cancel
-- 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 : ℤ
inl : ∀ (hn : 0 ≤ n), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
inr : ∀ (hn : n < 0), 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

Tactic:
rcases le_or_gt 0 n with hn | hn

Premises used: le_or_gt, OfNat.ofNat
-- 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
inl : ∀ (hm : 0 ≤ m), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
inl₁ : ∀ (hm : m < 0), 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

Tactic:
rcases le_or_gt 0 m with hm | hm

Premises used: le_or_gt, OfNat.ofNat
-- 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
inr : ∀ (hm : 0 ≤ m), selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
inr₁ : ∀ (hm : m < 0), 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

Tactic:
rcases le_or_gt 0 m with hm | hm

Premises used: le_or_gt, OfNat.ofNat
-- 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 : 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
inl₄ 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
⊢ selfZPow x B (n + m) = selfZPow x B n * 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]

Premises used: pow_add, add_nonneg, selfZPow_of_nonneg, Int.natAbs_add_of_nonneg