awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
x x_1 : R × S
xR : R
xS : S
yR : R
yS : S
⊢ xR = yR ↔ (1, 0) * (xR, xS) = (1, 0) * (yR, yS)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
fst : (HMul.hMul (α := R × S) (0, 1) (0, 1)).1 = (0, 1).1
snd : (HMul.hMul (α := R × S) (0, 1) (0, 1)).2 = (0, 1).2
⊢ IsIdempotentElem (M := R × S) (0, 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ (HMul.hMul (α := R × S) (0, 1) (0, 1)).1 = (0, 1).1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ (HMul.hMul (α := R × S) (0, 1) (0, 1)).2 = (0, 1).2

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
x x_1 : R × S
xR : R
xS : S
yR : R
yS : S
⊢ xS = yS ↔ (0, 1) * (xR, xS) = (0, 1) * (yR, yS)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
⊢ Away r T

Tactic:
.mk _ hr (fun t ↦ ?_) fun x y h ↦ ⟨n, ?_⟩

Premises used: IsLocalization.Away.mk, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
refine_1 :
  ∀ (t : T),
    ∃ (n : ℕ) (a : S),
      t * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n = (algebraMap S T : (a : S) → T) a
refine_2 :
  ∀ (x y : S) (h : Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) x : T) ((algebraMap S T : (a : S) → T) y : T)),
    r ^ n * x = r ^ n * y
⊢ Away r T

Tactic:
refine .mk _ hr (fun t ↦ ?_) fun x y h ↦ ⟨n, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
t : T
refine_1 :
  ∀ (s : S),
    ∃ (n : ℕ) (a : S),
      HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
          (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n) =
        (algebraMap S T : (a : S) → T) a
⊢ ∃ (n : ℕ) (a : S), t * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n = (algebraMap S T : (a : S) → T) a

Tactic:
obtain ⟨s, rfl⟩ := h₁ t

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
s : S
⊢ ∃ (a : S),
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
        (HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) r : T) 0) =
      (algebraMap S T : (a : S) → T) a

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
s : S
⊢ ∃ (n : ℕ) (a : S),
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n) =
      (algebraMap S T : (a : S) → T) a

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
x y : S
h : Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) x : T) ((algebraMap S T : (a : S) → T) y : T)
refine_2 : r ^ n * (x - y) = 0
⊢ r ^ n * x = r ^ n * y

Tactic:
rw [← sub_eq_zero, ← mul_sub]

Premises used: mul_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
x y : S
h : Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) x : T) ((algebraMap S T : (a : S) → T) y : T)
⊢ x - y ∈ (↑(RingHom.ker (F := S →+* T) (algebraMap S T)) : Set S) ∧
    (DistribSMul.toLinearMap S S (r ^ n) : (a : S) → S) (x - y) = r ^ n * (x - y)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
x y : S
h : Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) x : T) ((algebraMap S T : (a : S) → T) y : T)
⊢ r ^ n * (x - y) = 0

Tactic:
exact hn ⟨x - y, by simp [h]⟩

Premises used: HSub.hSub, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
⊢ Away.{u_4, u_5} (R := S) ((algebraMap R S : (a : R) → S) r : S) T

Tactic:
Away.of_surjective h₁ ?_ n ?_

Premises used: IsLocalization.Away.of_surjective
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
refine_1 : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
refine_2 :
  HSMul.hSMul (β := Ideal S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
      (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤
    ⊥
⊢ Away.{u_4, u_5} (R := S) ((algebraMap R S : (a : R) → S) r : S) T

Tactic:
refine Away.of_surjective h₁ ?_ n ?_

Premises used: IsLocalization.Away.of_surjective
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
refine_1 refine_1₁ refine_1₂ refine_1₃ : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
⊢ IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)

Tactic:
rwa [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
refine_2 :
  LE.le.{u_4} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S)
      (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
    ⊥
⊢ HSMul.hSMul (β := Ideal S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
      (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤
    ⊥

Tactic:
rw [← (RingHom.ker (algebraMap S T)).map_comap_of_surjective _ h₂, ← map_pow,
      ← Ideal.map_pointwise_smul, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]

Premises used: Algebra.algebraMap, RingHom.comap_ker, map_pow, IsScalarTower.algebraMap_eq, Ideal.map_pointwise_smul, Ideal.map_comap_of_surjective, RingHom.ker
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
refine_2 :
  ∀
    (hn :
      HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
        Ideal.comap (F := R →+* S) (algebraMap R S) ⊥),
    LE.le.{u_4} (α := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
      ⊥
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀
    (hn :
      LE.le.{u_4} (α := Ideal S)
        (Ideal.map (F := R →+* S) (algebraMap R S)
          (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
        ⊥),
    LE.le.{u_4} (α := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
      ⊥
⊢ LE.le.{u_4} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S)
      (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
    ⊥

Tactic:
rwa [RingHom.ker_eq_comap_bot (algebraMap R S), ← Ideal.map_le_iff_le_comap] at hn

Premises used: Algebra.algebraMap, Ideal.map_le_iff_le_comap, RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
f : R →+* A
r a : R
v : A
hv : HMul.hMul (α := A) ((f : (a : R) → A) r : A) v = 1
j : ℕ
⊢ (awayLift f r ⋯ : (a : Away r) → A)
      (mk a (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) (r ^ j) ⋯)) =
    HMul.hMul (α := A) ((f : (a : R) → A) a : A) (v ^ j)

Tactic:
simp [Localization.mk_eq_mk', awayLift, Away.lift, IsLocalization.lift_mk',
    Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight, mul_assoc, ← mul_pow, (mul_comm _ _).trans hv]

Premises used: IsUnit.liftRight, Localization.mk_eq_mk', mul_assoc, Units.mul_inv_eq_iff_eq_mul, IsLocalization.lift_mk', Localization.awayLift, mul_comm, IsLocalization.Away.lift, mul_pow, Eq.trans
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
r : R
⊢ Function.Injective.{u_4 + 1, u_2 + 1} (α := Away r) (β := Away (M := S) ((f : (a : R) → S) r : S))
      (⇑(awayMap f r) : (a : Away r) → Away ((f : (a : R) → S) r)) ↔
    ∀ (a : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S) → ∃ (n : ℕ), r ^ n * a = 0

Tactic:
IsLocalization.Away.map_injective_iff _ _ _

Premises used: IsLocalization.Away.map_injective_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
r : R
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away r) (β := Away (M := S) ((f : (a : R) → S) r : S))
      (⇑(awayMap f r) : (a : Away r) → Away ((f : (a : R) → S) r)) ↔
    ∀ (a : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) r : S) m * a

Tactic:
IsLocalization.Away.map_surjective_iff _ _ _ _

Premises used: IsLocalization.Away.map_surjective_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H :
  Function.Injective.{u_4 + 1, u_2 + 1} (α := Away a) (β := Away (M := S) ((f : (a : R) → S) a : S))
    (⇑(awayMap f a) : (a_1 : Away a) → Away ((f : (a : R) → S) a))
simp :
  ∀ (H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0) (a : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S) → ∃ (n : ℕ), b ^ n * a = 0
⊢ Function.Injective.{u_4 + 1, u_2 + 1} (α := Away b) (β := Away (M := S) ((f : (a : R) → S) b : S))
    (⇑(awayMap f b) : (a : Away b) → Away ((f : (a : R) → S) b))

Tactic:
simp only [awayMap_injective_iff] at H ⊢

Premises used: Localization.awayMap_injective_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
obtain : ∀ (b a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), (a * b) ^ n * a_1 = 0
⊢ ∀ (a : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S) → ∃ (n : ℕ), b ^ n * a = 0

Tactic:
obtain ⟨b, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
b : R
⊢ ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), (a * b) ^ n * a_1 = 0

Tactic:
fun x hx ↦ ?_
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
b : R
refine : ∀ (x : R) (hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)), ∃ (n : ℕ), (a * b) ^ n * x = 0
⊢ ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), (a * b) ^ n * a_1 = 0

Tactic:
refine fun x hx ↦ ?_
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
b x : R
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
obtain : ∀ (n : ℕ) (hn : a ^ n * x = 0), ∃ (n : ℕ), (a * b) ^ n * x = 0
⊢ ∃ (n : ℕ), (a * b) ^ n * x = 0

Tactic:
obtain ⟨n, hn⟩ := H x hx
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
b x : R
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
n : ℕ
hn : a ^ n * x = 0
⊢ (a * b) ^ n * x = 0

Tactic:
simp [mul_pow, mul_assoc, mul_left_comm (a ^ n), hn]

Premises used: mul_assoc, mul_left_comm, HPow.hPow, mul_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
b x : R
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
n : ℕ
hn : a ^ n * x = 0
⊢ ∃ (n : ℕ), (a * b) ^ n * x = 0

Tactic:
exact ⟨n, by simp [mul_pow, mul_assoc, mul_left_comm (a ^ n), hn]⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away a) (β := Away (M := S) ((f : (a : R) → S) a : S))
    (⇑(awayMap f a) : (a_1 : Away a) → Away ((f : (a : R) → S) a))
simp :
  ∀ (H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1)
    (a : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) b : S) m * a
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away b) (β := Away (M := S) ((f : (a : R) → S) b : S))
    (⇑(awayMap f b) : (a : Away b) → Away ((f : (a : R) → S) b))

Tactic:
simp only [awayMap_surjective_iff] at H ⊢

Premises used: Localization.awayMap_surjective_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
obtain :
  ∀ (b : R) (a_1 : S),
    ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
⊢ ∀ (a : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) b : S) m * a

Tactic:
obtain ⟨b, 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
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
b : R
⊢ ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1

Tactic:
fun x ↦ ?_
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
b : R
refine :
  ∀ (x : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x
⊢ ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1

Tactic:
refine fun x ↦ ?_
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
b : R
x : S
obtain :
  ∀ (c : R) (m : ℕ) (e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * x),
    ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x
⊢ ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x

Tactic:
obtain ⟨c, m, e⟩ := H x
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
b : R
x : S
c : R
m : ℕ
e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * x
⊢ (f : (a : R) → S) (b ^ m * c) = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x

Tactic:
simp [mul_pow, e, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm, mul_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
b : R
x : S
c : R
m : ℕ
e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * x
⊢ ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x

Tactic:
exact ⟨b ^ m * c, m, by simp [mul_pow, e, mul_assoc, mul_left_comm]⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H :
  Function.Bijective.{u_4 + 1, u_2 + 1} (α := Away a) (β := Away (M := S) ((f : (a : R) → S) a : S))
    (⇑(awayMap f a) : (a_1 : Away a) → Away ((f : (a : R) → S) a))
⊢ Function.Bijective.{u_4 + 1, u_2 + 1} (α := Away b) (β := Away (M := S) ((f : (a : R) → S) b : S))
    (⇑(awayMap f b) : (a : Away b) → Away ((f : (a : R) → S) b))

Tactic:
⟨awayMap_injective_of_dvd f h H.1, awayMap_surjective_of_dvd f h H.2⟩

Premises used: Localization.awayMap_surjective_of_dvd, And.right, And.left, And.intro, Function.Bijective, Localization.awayMap_injective_of_dvd