awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) z = 1
have toIsLocalizationMap : val
    (HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x)
      z) =
  val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ val
      (HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x)
        z) =
    val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 1
have toIsLocalizationMap : Eq (α := at Submonoid.powers x)
  (Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)))
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e)) sorry))
  1
Tactic: simp only [val_mul, val_one, awayMap_mk, Away.val_mk, z, Localization.mk_mul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ Eq (α := at Submonoid.powers x)
    (Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e)) ⋯))
    1
have toIsLocalizationMap : ∃ (c : ↥(Submonoid.powers x)),
  (↑c : A) *
      ((↑(1, 1).2 : A) *
        (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e))
                sorry).1) =
    (↑c : A) *
      ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (d + e)) sorry).2 :
          A) *
        (1, 1).1)
Tactic: rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(1, 1).2 : A) *
          (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (d + e)) ⋯).1) =
      (↑c : A) *
        ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e)
                      ⋯ *
                    Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (d + e)) ⋯).2 :
            A) *
          (1, 1).1)
have h : (↑1 : A) *
    ((↑(1, 1).2 : A) *
      (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
          Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry *
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e))
              sorry).1) =
  (↑1 : A) *
    ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (d + e)) sorry).2 :
        A) *
      (1, 1).1)
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ (↑1 : A) *
      ((↑(1, 1).2 : A) *
        (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e))
                ⋯).1) =
    (↑1 : A) *
      ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (d + e)) ⋯).2 :
          A) *
        (1, 1).1)
have h : g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)) = (f * g) ^ e * (f * g) ^ (d + e)
Tactic: simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_one, hx]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
z : Away 𝒜 x
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (β := Away 𝒜 x) z
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
have toIsLocalizationMap : ∀ (n : ℕ) (s : A) (hs : s ∈ 𝒜 (n • (d + e))),
  ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 sorry n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
Tactic: obtain ⟨n, s, hs, rfl⟩ := Away.mk_surjective 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
hs : s ∈ 𝒜 (n • (d + e))
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
have toIsLocalizationMap : ∀ (hf : f ∈ 𝒜 0) (hd : Ne (α := ℕ) 0 0) (hs : s ∈ 𝒜 (n • (0 + e))),
  ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 sorry n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
Tactic: rcases d with - | d
Cleared hypotheses: d, hf, hd, hs
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
hs : s ∈ 𝒜 (n • (d + e))
toIsLocalizationMap :
  ∀ (hf : f ∈ 𝒜 0) (hd : Ne (α := ℕ) 0 0) (hs : s ∈ 𝒜 (n • (0 + e))),
    ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
      HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
          ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
        (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
have toIsLocalizationMap₁ : ∀ (d : ℕ) (hf : f ∈ 𝒜 (d + 1)) (hd : d + 1 ≠ 0) (hs : s ∈ 𝒜 (n • (d + 1 + e))),
  ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 sorry n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
Tactic: rcases d with - | d
Cleared hypotheses: d, hf, hd, hs
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ s * g ^ (n * d) ∈ 𝒜 ((n * (e + 1)) • (d + 1))
have h : (n * (e + 1)) • (d + 1) = n • (d + 1 + e) + (n * d) • e
Tactic: convert! SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
have toIsLocalizationMap : HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 sorry n s hs)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
        (↑(t,
                Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                  Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                  ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) sorry).2 :
          Away 𝒜 f) :
      Away 𝒜 x) =
  (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
    (t,
        Subtype.mk (p := fun (x : Away 𝒜 f) ↦
          Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
          ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) sorry).1
Tactic: refine ⟨⟨t, ⟨_, ⟨n, rfl⟩⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
          (↑(t,
                  Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                    Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                    ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).2 :
            Away 𝒜 f) :
        Away 𝒜 x) =
    (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
      (t,
          Subtype.mk (p := fun (x : Away 𝒜 f) ↦
            Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).1
have toIsLocalizationMap : val
    (HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 sorry n s hs)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
          (↑(t,
                  Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                    Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                    ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) sorry).2 :
            Away 𝒜 f) :
        Away 𝒜 x)) =
  val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
      (t,
          Subtype.mk (p := fun (x : Away 𝒜 f) ↦
            Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) sorry).1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ val
      (HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
            (↑(t,
                    Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                      Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                      ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).2 :
              Away 𝒜 f) :
          Away 𝒜 x)) =
    val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
        (t,
            Subtype.mk (p := fun (x : Away 𝒜 f) ↦
              Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).1)
have toIsLocalizationMap : Eq (α := at Submonoid.powers x)
  (Localization.mk (s * (g ^ (d + 1) * g ^ e) ^ n)
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry ^ n))
  (Localization.mk (s * g ^ (n * d) * g ^ (n * (e + 1)))
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (n * (e + 1)))
      sorry))
Tactic: simp only [RingHom.algebraMap_toAlgebra, map_pow, awayMap_mk, val_mul, val_mk, val_pow,
      Localization.mk_pow, Localization.mk_mul, t]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ Eq (α := at Submonoid.powers x)
    (Localization.mk (s * (g ^ (d + 1) * g ^ e) ^ n)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ ^ n))
    (Localization.mk (s * g ^ (n * d) * g ^ (n * (e + 1)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (n * (e + 1)))
        ⋯))
have toIsLocalizationMap : ∃ (c : ↥(Submonoid.powers x)),
  (↑c : A) *
      ((↑(s * g ^ (n * d) * g ^ (n * (e + 1)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (n * (e + 1))) sorry).2 :
          A) *
        (s * (g ^ (d + 1) * g ^ e) ^ n,
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) sorry *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) sorry ^
                n).1) =
    (↑c : A) *
      ((↑(s * (g ^ (d + 1) * g ^ e) ^ n,
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) sorry *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e)
                      sorry ^
                    n).2 :
          A) *
        (s * g ^ (n * d) * g ^ (n * (e + 1)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
              (x ^ (n * (e + 1))) sorry).1)
Tactic: rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ (↑1 : A) *
      ((↑(s * g ^ (n * d) * g ^ (n * (e + 1)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (n * (e + 1))) ⋯).2 :
          A) *
        (s * (g ^ (d + 1) * g ^ e) ^ n,
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) ⋯ *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ ^
                n).1) =
    (↑1 : A) *
      ((↑(s * (g ^ (d + 1) * g ^ e) ^ n,
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) ⋯ *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e)
                      ⋯ ^
                    n).2 :
          A) *
        (s * g ^ (n * d) * g ^ (n * (e + 1)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
              (x ^ (n * (e + 1))) ⋯).1)
have simp : x ^ (n * (e + 1)) * (s * (g ^ (d + 1) * g ^ e) ^ n) = x ^ n * (x ^ e) ^ n * (s * g ^ (n * d) * g ^ (n * (e + 1)))
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
a b : Away 𝒜 f
e :
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) a : Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) b : Away 𝒜 x)
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * a = (↑c : Away 𝒜 f) * b
have toIsLocalizationMap : ∀ (n : ℕ) (a : A) (ha : a ∈ 𝒜 (n • d))
  (e :
    Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) b : Away 𝒜 x)),
  ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * b
Tactic: obtain ⟨n, a, ha, rfl⟩ := Away.mk_surjective 𝒜 hf a
Cleared hypotheses: a, e
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
b : Away 𝒜 f
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
e :
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) b : Away 𝒜 x)
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * b
have toIsLocalizationMap : ∀ (m : ℕ) (b : A) (hb : b ∈ 𝒜 (m • d))
  (e :
    Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb) : Away 𝒜 x)),
  ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
Tactic: obtain ⟨m, b, hb, rfl⟩ := Away.mk_surjective 𝒜 hf b
Cleared hypotheses: b, e