awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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)
this : IsDomain B
⊢ a₀ ≠ 0
have H₁ : b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = (algebraMap R B : (a : R) → B) a₀
Tactic: simp only [← hy, map_pow] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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₀
⊢ a₀ ≠ 0
have apply : ¬Eq.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) a₀ : B) (0 : B)
Tactic: apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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₀
apply : ¬Eq.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) a₀ : B) (0 : B)
⊢ a₀ ≠ 0
have apply₁ : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
Tactic: apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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₀
⊢ ¬Eq.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) a₀ : B) (0 : B)
have rw : ¬b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = 0
Tactic: rw [← H]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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₀
⊢ ¬b * HPow.hPow (α := B) ((algebraMap R B : (a : R) → B) x : B) d = 0
have apply : Ne.{u_4 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B) (0 : B)
Tactic: apply mul_ne_zero hb (pow_ne_zero _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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 : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
have ha₀ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (hypothesis)
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
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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₀
⊢ ∃ (a : R) (n : ℤ), ¬x ∣ a ∧ HMul.hMul (β := B) (selfZPow x B n) ((algebraMap R B : (a : R) → B) a : B) = b
have 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
Tactic: obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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
have refine : ¬x ∣ a ∧
  HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑m : ℤ) (↑d : ℤ))) ((algebraMap R B : (a : R) → B) a : B) = b
Tactic: refine ⟨a, m - d, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
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 ∧
    HMul.hMul (β := B) (selfZPow x B (HSub.hSub (α := ℤ) (↑m : ℤ) (↑d : ℤ))) ((algebraMap R B : (a : R) → B) a : B) = b
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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)) ⊤
⊢ Eq (α := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) ⊤
have rw : s ⊆ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
Tactic: rw [← Ideal.radical_eq_top, eq_top_iff, ← hsone, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (hypothesis)
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
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have this : 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⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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)))
have 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⟩))
Tactic: rw [Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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
⊢ 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⟩))
have 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
Tactic: rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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
have refine : ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (a * (sec a x).1) z
Tactic: refine ⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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
⊢ ∃ (z : ↥(Submonoid.powers a)), x = mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (a * (sec a x).1) z
have 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)) sorry)
Tactic: use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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
⊢ 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))
        ⋯)
have h : HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
    ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
              (a ^ ((sec a x).2 + 1)) sorry) :
          R) :
      Rₜ (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⟩) (a * (sec a x).1)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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 :
  HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                (a ^ ((sec a x).2 + 1)) ⋯) :
            R) :
        Rₜ (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⟩) (a * (sec a x).1)
⊢ 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))
        ⋯)
have h₁ : x *
    HPow.hPow (α := Rₜ (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⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((sec a x).2 + 1) =
  (algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (a * (sec a x).1)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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 :
  HMul.hMul (β := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) x
      ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩)
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                (a ^ ((sec a x).2 + 1)) ⋯) :
            R) :
        Rₜ (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⟩) (a * (sec a x).1)
h₁ :
  x *
      HPow.hPow (α := Rₜ (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⟩) a :
          Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        ((sec a x).2 + 1) =
    (algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) (a * (sec a x).1)
⊢ 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))
        ⋯)
have h₂ : x *
    HPow.hPow (α := Rₜ (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⟩) a :
        Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
      ((sec a x).2 + 1) =
  HMul.hMul (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (β :=
    Rₜ (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⟩) a :
      Rₜ (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⟩) (sec a x).1 :
      Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (hypothesis)
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))
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have 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)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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)
have 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)
Tactic: rw [IsLocalization.mk'_one]