awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.AdjoinRoot
Goal:
R : Type u_2
S : Type u_3
S' : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
inst_5 : Algebra S S'
inst_6 : IsScalarTower R S S'
f : S
inst_7 : IsLocalization.Away f S'
inst_8 : FinitePresentation R S
⊢ FinitePresentation R S'

Tactic:
have : Algebra.FinitePresentation S S' :=
    IsLocalization.Away.finitePresentation f
  .trans R S S'

Premises used: IsLocalization.Away.finitePresentation, Algebra.FinitePresentation.trans
-- Module: Mathlib.RingTheory.Localization.Away.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.FinitePresentation R S
f : S
⊢ Algebra.FinitePresentation.{u_1, u_2} R (Away f)

Tactic:
.of_isLocalizationAway f

Premises used: Algebra.FinitePresentation.of_isLocalizationAway
-- Module: Mathlib.RingTheory.Localization.Away.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.FiniteType R S
f : S
⊢ Algebra.FiniteType.{u_1, u_2} R (Away f)

Tactic:
.trans ‹_› inferInstance

Premises used: inferInstance, Algebra.FiniteType.trans
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
⊢ mk' (M := Submonoid.powers x) S
        (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) : R) 1 *
      mk' S (↑1 : R)
        (Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) =
    1

Tactic:
IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1

Premises used: IsLocalization.mk'_mul_mk'_eq_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
h :
  (algebraMap R S : (a : R) → S) x =
    mk' (M := Submonoid.powers x) S
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) : R) 1
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) (invSelf x : S) = 1

Tactic:
convert! IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1

Premises used: IsLocalization.mk'_mul_mk'_eq_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
h :
  mk' (M := Submonoid.powers x) S
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) : R) 1 =
    (algebraMap R S : (a : R) → S) x
⊢ (algebraMap R S : (a : R) → S) x =
    mk' (M := Submonoid.powers x) S
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) : R) 1

Tactic:
symm
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
⊢ mk' (M := Submonoid.powers x) S
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1) x ⋯) : R) 1 =
    (algebraMap R S : (a : R) → S) x

Tactic:
apply IsLocalization.mk'_one

Premises used: IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
simp :
  HMul.hMul (β := S) s
      ((algebraMap R S : (a : R) → S)
          (x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) ⋯) :
        S) =
    HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R) : S)
⊢ HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (x ^ (sec x s).2) : S) =
    (algebraMap R S : (a : R) → S) (sec x s).1

Tactic:
simp only [IsLocalization.Away.sec, ← IsLocalization.sec_spec]

Premises used: IsLocalization.Away.sec, IsLocalization.sec_spec
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
e_a :
  x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) ⋯ =
    (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)
⊢ HMul.hMul (β := S) s
      ((algebraMap R S : (a : R) → S)
          (x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) ⋯) :
        S) =
    HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R) : S)

Tactic:
congr
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
⊢ x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) ⋯ =
    (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)

Tactic:
(IsLocalization.sec (Submonoid.powers x) s).2.property.choose_spec

Premises used: IsLocalization.sec, Exists.choose_spec, Submonoid.powers, Prod.snd, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
⊢ x ^ Exists.choose (p := fun (y : ℕ) ↦ x ^ y = (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)) ⋯ =
    (↑(IsLocalization.sec (Submonoid.powers x) s).2 : R)

Tactic:
exact (IsLocalization.sec (Submonoid.powers x) s).2.property.choose_spec

Premises used: IsLocalization.sec, Exists.choose_spec, Submonoid.powers, Prod.snd, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
n : ℕ
⊢ (fun (x_1 : ℕ) ↦ x ^ x_1) 1 = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
⊢ (fun (x_1 : ℕ) ↦ x ^ x_1) 1 = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
rw : Associated (s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) (sec x s).2) s
⊢ Associated ((algebraMap R S : (a : R) → S) (sec x s).1) s

Tactic:
rw [← IsLocalization.Away.sec_spec, map_pow]

Premises used: IsLocalization.Away.sec_spec, map_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
⊢ Associated (s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) (sec x s).2) s

Tactic:
associated_mul_unit_left _ _ <| .pow _ <| IsLocalization.Away.algebraMap_isUnit _

Premises used: IsUnit.pow, associated_mul_unit_left, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
s : S
⊢ Associated (s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) (sec x s).2) s

Tactic:
exact associated_mul_unit_left _ _ <| .pow _ <| IsLocalization.Away.algebraMap_isUnit _

Premises used: associated_mul_unit_left, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
y : R
⊢ (∃ (m : R), Membership.mem (γ := Submonoid R) (Submonoid.powers x) m ∧ y ∣ m) ↔ ∃ (n : ℕ), y ∣ x ^ n

Tactic:
simp [Submonoid.mem_powers_iff]

Premises used: Submonoid.mem_powers_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
z : S
obtain :
  ∀ (a : R) (n : ℕ)
    (h :
      HMul.hMul (β := S) z
          ((algebraMap R S : (a : R) → S)
              (↑(a,
                      Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                        ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).2 :
                R) :
            S) =
        (algebraMap R S : (a : R) → S)
          (a,
              Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).1),
    ∃ (n : ℕ) (a : R),
      z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
⊢ ∃ (n : ℕ) (a : R), z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a

Tactic:
obtain ⟨⟨a, ⟨-, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers x) z

Premises used: IsLocalization.surj, Submonoid.powers, rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
z : S
a : R
n : ℕ
h :
  HMul.hMul (β := S) z
      ((algebraMap R S : (a : R) → S)
          (↑(a,
                  Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                    ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).2 :
            R) :
        S) =
    (algebraMap R S : (a : R) → S)
      (a,
          Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).1
h₁ : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
⊢ ∃ (n : ℕ) (a : R), z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a

Tactic:
use n, a
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
z : S
a : R
n : ℕ
h :
  HMul.hMul (β := S) z
      ((algebraMap R S : (a : R) → S)
          (↑(a,
                  Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                    ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).2 :
            R) :
        S) =
    (algebraMap R S : (a : R) → S)
      (a,
          Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯).1
⊢ z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
a b : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
obtain :
  ∀ (n : ℕ)
    (hx :
      (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯) :
            R) *
          a =
        (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
                ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯) :
            R) *
          b),
    ∃ (n : ℕ), x ^ n * a = x ^ n * b
⊢ ∃ (n : ℕ), x ^ n * a = x ^ n * b

Tactic:
obtain ⟨⟨-, n, rfl⟩, hx⟩ := IsLocalization.exists_of_eq (M := Submonoid.powers x) h

Premises used: IsLocalization.exists_of_eq, rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
a b : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hx :
  (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯) :
        R) *
      a =
    (↑(Subtype.mk (p := fun (x_1 : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) n) ⋯) :
        R) *
      b
w : ℕ
h₁ : x ^ n * a = x ^ n * b
⊢ ∃ (n : ℕ), x ^ n * a = x ^ n * b

Tactic:
use n
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
n : ℕ
simp : IsUnit (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
⊢ IsUnit (M := S)
    ((algebraMap R S : (a : R) → S)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯) :
          R) :
      S)

Tactic:
simp only [map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)

Tactic:
IsUnit.pow _ map_unit

Premises used: IsUnit.pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)

Tactic:
exact IsUnit.pow _ map_unit

Premises used: IsUnit.pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
z : S
obtain :
  ∀ (n : ℕ) (a : R)
    (hn : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a),
    ∃ (x : R × ↥(Submonoid.powers r)),
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
⊢ ∃ (x : R × ↥(Submonoid.powers r)),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

Tactic:
obtain ⟨n, a, hn⟩ := surj z
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
h :
  HMul.hMul (β := S) z
      ((algebraMap R S : (a : R) → S)
          (↑(a, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) ⋯).2 :
            R) :
        S) =
    (algebraMap R S : (a : R) → S)
      (a, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) ⋯).1
⊢ ∃ (x : R × ↥(Submonoid.powers r)),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

Tactic:
use ⟨a, ⟨r ^ n, n, rfl⟩⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
⊢ HMul.hMul (β := S) z
      ((algebraMap R S : (a : R) → S)
          (↑(a, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) ⋯).2 :
            R) :
        S) =
    (algebraMap R S : (a : R) → S)
      (a, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) ⋯).1

Tactic:
simpa using hn
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
x y : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
obtain : ∀ (n : ℕ) (hn : r ^ n * x = r ^ n * y), ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y
⊢ ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y

Tactic:
obtain ⟨n, hn⟩ := exists_of_eq x y h
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
map_unit : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
surj :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
exists_of_eq :
  ∀ (a b : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S) →
      ∃ (n : ℕ), r ^ n * a = r ^ n * b
x y : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
n : ℕ
hn : r ^ n * x = r ^ n * y
w : ↥(Submonoid.powers r)
h₁ :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) ⋯) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ n) ⋯) : R) * y
⊢ ∃ (c : ↥(Submonoid.powers r)), (↑c : R) * x = (↑c : R) * y

Tactic:
use ⟨r ^ n, n, rfl⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r r' : R
h : Associated r r'
inst_3 : Away r S
obtain : ∀ (u : Rˣ), Away (r * (↑u : R)) S
⊢ Away r' S

Tactic:
obtain ⟨u, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
⊢ Away (r * (↑u : R)) S

Tactic:
mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)

Premises used: IsLocalization.Away.mk
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
refine_1 : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S)
refine_2 :
  ∀ (s : S),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
refine_3 :
  ∀ (a b : R)
    (hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)),
    ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
⊢ Away (r * (↑u : R)) S

Tactic:
refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)

Premises used: IsLocalization.Away.mk
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S)

Tactic:
simp [algebraMap_isUnit r, IsUnit.map _ u.isUnit]

Premises used: IsUnit.map, Units.isUnit, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
s : S
refine_2 :
  ∀ (n : ℕ) (a : R)
    (hn : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a),
    ∃ (n : ℕ) (a : R),
      s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a
⊢ ∃ (n : ℕ) (a : R),
    s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a

Tactic:
obtain ⟨n, a, hn⟩ := surj r s

Premises used: IsLocalization.Away.surj
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
h :
  s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n =
    (algebraMap R S : (a : R) → S) (a * (↑u : R) ^ n)
⊢ ∃ (n : ℕ) (a : R),
    s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n = (algebraMap R S : (a : R) → S) a

Tactic:
use n, a * u ^ n
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n = (algebraMap R S : (a : R) → S) a
⊢ s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) (r * (↑u : R)) : S) n =
    (algebraMap R S : (a : R) → S) (a * (↑u : R) ^ n)

Tactic:
simp [mul_pow, ← mul_assoc, hn]

Premises used: mul_assoc, mul_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
refine_3 : ∀ (n : ℕ) (hn : r ^ n * a = r ^ n * b), ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
⊢ ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b

Tactic:
obtain ⟨n, hn⟩ := exists_of_eq r hab

Premises used: IsLocalization.Away.exists_of_eq