awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
this : IsDomain B
H : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)

Tactic:
exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)

Premises used: IsLocalization.injective, powers_le_nonZeroDivisors_of_noZeroDivisors, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H :
  HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (↑(a₀, y).2 : R) : B) = (algebraMap R B : (a : R) → B) (a₀, y).1
d : ℕ
hy : x ^ d = (↑y : R)
⊢ a₀ ≠ 0

Tactic:
have ha₀ : a₀ ≠ 0 := by
    haveI := isDomain_of_le_nonZeroDivisors B
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
    simp only [← hy, map_pow] at H
    apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
    · rw [← H]
      apply mul_ne_zero hb (pow_ne_zero _ _)
      exact
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
          (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
          (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
    · exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H :
  HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (↑(a₀, y).2 : R) : B) = (algebraMap R B : (a : R) → B) (a₀, y).1
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
⊢ HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀

Tactic:
simp only [← hy] at H
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
H : HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀
obtain :
  ∀ (m : ℕ) (a : R) (hyp1 : ¬x ∣ a) (hyp2 : a₀ = x ^ m * a),
    ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b

Tactic:
obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx

Premises used: WfDvdMonoid.max_power_factor
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
H : HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b

Tactic:
⟨a, m - d, ?_⟩

Premises used: HSub.hSub, Nat.cast, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
H : HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
refine :
  ¬x ∣ a ∧
    HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑m : ℤ) (↑d : ℤ))) ((algebraMap R B : (a : R) → B) a : B) = b
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b

Tactic:
refine ⟨a, m - d, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
H : HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
rw :
  ¬x ∣ a ∧
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m * mk' (M := Submonoid.powers x) B a 1 =
      HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m)
        ((algebraMap R B : (a : R) → B) a : B)
⊢ ¬x ∣ a ∧
    HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑m : ℤ) (↑d : ℤ))) ((algebraMap R B : (a : R) → B) a : B) = b

Tactic:
rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_natCast, selfZPow_natCast,
    ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]

Premises used: selfZPow_pow_sub, map_pow, map_mul, IsLocalization.mk'_one, selfZPow_natCast, mul_comm
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
H : HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m * mk' (M := Submonoid.powers x) B a 1 =
      HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m)
        ((algebraMap R B : (a : R) → B) a : B)

Tactic:
⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩

Premises used: congr_arg, IsLocalization.mk'_one, And.intro
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_3
inst : CommRing R
x : R
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra R B
inst_3 : IsLocalization.Away x B
inst_4 : IsDomain R
inst_5 : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = (↑y : R)
ha₀ : a₀ ≠ 0
H : HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) (x ^ d) : B) = (algebraMap R B : (a : R) → B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧
    HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m * mk' (M := Submonoid.powers x) B a 1 =
      HMul.hMul (β := B) (HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) m)
        ((algebraMap R B : (a : R) → B) a : B)

Tactic:
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
rw : s ⊆ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
⊢ Eq (α := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) ⊤

Tactic:
rw [← Ideal.radical_eq_top, eq_top_iff, ← hsone, Ideal.span_le]

Premises used: Ideal.span_le, eq_top_iff, Ideal.radical_eq_top
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
⊢ IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))

Tactic:
haveI : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩) :=
    inferInstanceAs <| IsLocalization.Away (⟨a, ha⟩ : s).val (Rₜ ⟨a, ha⟩)
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
rw :
  p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha) ⊆
    (↑(Ideal.span
          ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
            Set.range (mulNumerator s (Rₜ := Rₜ) p))) :
      Set (Rₜ ⟨a, ha⟩))
⊢ LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
x : Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)
hx :
  Membership.mem (γ := Set (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
rw :
  ∃ (y : R),
    Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y ∧
      ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y z
⊢ x ∈
    (↑(Ideal.span
          ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
            Set.range (mulNumerator s (Rₜ := Rₜ) p))) :
      Set (Rₜ ⟨a, ha⟩))

Tactic:
rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]

Premises used: IsLocalization.mem_span_map, SetLike.mem_coe, Submonoid.powers
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
x : Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)
hx :
  Membership.mem (γ := Set (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
⊢ ∃ (y : R),
    Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y ∧
      ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y z

Tactic:
⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩

Premises used: Ideal.subset_span, HMul.hMul, IsLocalization.Away.sec, Prod.fst, Subtype.mk, And.intro, Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
x : Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)
hx :
  Membership.mem (γ := Set (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
refine : ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (a * (sec a x).1) z
⊢ ∃ (y : R),
    Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y ∧
      ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y z

Tactic:
refine ⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
x : Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)
hx :
  Membership.mem (γ := Set (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
h :
  x =
    mk' (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (a * (sec a x).1)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x) (a ^ ((sec a x).2 + 1))
        ⋯)
⊢ ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (a * (sec a x).1) z

Tactic:
use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
⊢ LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))

Tactic:
have h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span
      (algebraMap R (Rₜ ⟨a, ha⟩) '' Set.range (IsLocalization.Away.mulNumerator s p)) := by
    rw [Ideal.span_le]
    intro x hx
    rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]
    refine ⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩
    use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩
    rw [IsLocalization.eq_mk'_iff_mul_eq, map_pow, map_mul, ← map_pow, pow_add, map_mul,
      ← mul_assoc, IsLocalization.Away.sec_spec a x, mul_comm, pow_one]
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
rw :
  Membership.mem (γ := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
    ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) 1)
⊢ Membership.mem (γ := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
    (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)

Tactic:
rw [IsLocalization.mk'_one]

Premises used: IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
a₁ :
  Membership.mem (γ :=
    Submodule (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) 1)
⊢ Membership.mem (γ := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
    ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) 1)

Tactic:
apply h₁
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
⊢ Membership.mem (γ :=
    Submodule (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) 1)

Tactic:
simp [htone]
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
⊢ Membership.mem (γ := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
    (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)

Tactic:
have h₂ : IsLocalization.mk' (Rₜ ⟨a, ha⟩) 1 (1 : Submonoid.powers a) ∈ Ideal.span
      (algebraMap R (Rₜ ⟨a, ha⟩) ''
        (Set.range <| IsLocalization.Away.mulNumerator s p)) := by
    rw [IsLocalization.mk'_one]
    apply h₁
    simp [htone]