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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
have hx₁ : Membership.mem (γ := Set (Away 𝒜 f))
  {x : Away 𝒜 f |
    ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
      Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x}
  (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) sorry)
Tactic: apply Algebra.subset_adjoin
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
⊢ Membership.mem (γ := Set (Away 𝒜 f))
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}
    (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
have hx₁ : ∀ (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
Tactic: refine ⟨a - ∑ i : ι', dv i * (ai i / d), (ai · % d), H₀.symm, ?_, 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
⊢ ∀ (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
have hx₁ : ∀ (hd : d = 0) (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
Tactic: rcases d.eq_zero_or_pos with hd | hd
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
hx₁ : ∀ (hd : d = 0) (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
⊢ ∀ (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
have hx₂ : ∀ (hd : d > 0) (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
Tactic: rcases d.eq_zero_or_pos with hd | hd
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (hypothesis)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
hd : d = 0
⊢ ∀ (i : ι'), (fun (x : ι') ↦ ai x % d) i ≤ d
have this : ∀ (x : ι'), ai x = 0
Tactic: have : ∀ (x : ι'), ai x = 0 := by simpa [hd, fun i ↦ (hxd' i).ne'] using hai
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
have hy : ∀ (c : ι'),
  Membership.mem (γ := Finset ι') Finset.univ c →
    Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
      (Algebra.adjoin ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
      (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf sorry) (ai c / d))
Tactic: apply prod_mem
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
j : ι'
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai j / d))
have hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
  (Algebra.adjoin ↥(𝒜 0)
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
  (isLocalizationElem hf sorry)
Tactic: apply pow_mem
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
j : ι'
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (isLocalizationElem hf ⋯)
have hy : Membership.mem (γ := Set (Away 𝒜 f))
  {x : Away 𝒜 f |
    ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
      Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x}
  (isLocalizationElem hf sorry)
Tactic: apply Algebra.subset_adjoin
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
j : ι'
⊢ Membership.mem (γ := Set (Away 𝒜 f))
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}
    (isLocalizationElem hf ⋯)
have hy : ∑ i : ι', HSMul.hSMul (α := ℕ) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ) (dv i) = dv j • d
Tactic: refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
j : ι'
hy : ∑ i : ι', HSMul.hSMul (α := ℕ) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ) (dv i) = dv j • d
⊢ Membership.mem (γ := Set (Away 𝒜 f))
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}
    (isLocalizationElem hf ⋯)
have hy₁ : ∀ (i : ι'), Pi.single (M := fun (a : ι') ↦ ℕ) j d i ≤ d
Tactic: refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
j : ι'
hy : ∑ i : ι', HSMul.hSMul (α := ℕ) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ) (dv i) = dv j • d
hy₁ : ∀ (i : ι'), Pi.single (M := fun (a : ι') ↦ ℕ) j d i ≤ d
⊢ Membership.mem (γ := Set (Away 𝒜 f))
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}
    (isLocalizationElem hf ⋯)
have hy₂ : Eq (α := Away 𝒜 f)
  (Away.mk 𝒜 hf (dv j) (∏ i : ι', HPow.hPow (β := ℕ) (v i) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ)) sorry)
  (isLocalizationElem hf sorry)
Tactic: refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
j : ι'
⊢ Eq (α := Away 𝒜 f)
    (Away.mk 𝒜 hf (dv j) (∏ i : ι', HPow.hPow (β := ℕ) (v i) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ)) ⋯)
    (isLocalizationElem hf ⋯)
have hy : Eq (α := at Submonoid.powers f)
  (val (Away.mk 𝒜 hf (dv j) (∏ i : ι', HPow.hPow (β := ℕ) (v i) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ)) sorry))
  (val (isLocalizationElem hf sorry))
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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
⊢ ∀ (c : ι'),
    Membership.mem (γ := Finset ι') Finset.univ c →
      Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
        (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai c / d))
have hy : ∀ (j : ι'),
  Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
    (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf sorry) (ai j / d))
Tactic: classical
    rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
hy :
  ∀ (j : ι'),
    Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
      (Algebra.adjoin ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai j / d))
⊢ ∀ (c : ι'),
    Membership.mem (γ := Finset ι') Finset.univ c →
      Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
        (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai c / d))
have hy₁ : ∀ (j : ι'),
  Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
    (isLocalizationElem hf sorry)
Tactic: classical
    rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
hy :
  ∀ (j : ι'),
    Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
      (Algebra.adjoin ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai j / d))
hy₁ :
  ∀ (j : ι'),
    Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
      (Algebra.adjoin ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (isLocalizationElem hf ⋯)
⊢ ∀ (c : ι'),
    Membership.mem (γ := Finset ι') Finset.univ c →
      Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
        (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai c / d))
have hy₂ : ∀ (j : ι'),
  Membership.mem (γ := Set (Away 𝒜 f))
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x}
    (isLocalizationElem hf sorry)
Tactic: classical
    rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]
-- 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 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
hy :
  ∀ (j : ι'),
    Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
      (Algebra.adjoin ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai j / d))
hy₁ :
  ∀ (j : ι'),
    Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
      (Algebra.adjoin ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (isLocalizationElem hf ⋯)
hy₂ :
  ∀ (j : ι'),
    Membership.mem (γ := Set (Away 𝒜 f))
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}
      (isLocalizationElem hf ⋯)
⊢ ∀ (c : ι'),
    Membership.mem (γ := Finset ι') Finset.univ c →
      Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
        (HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai c / d))
have hy₃ : ∀ (j : ι'), ∑ i : ι', HSMul.hSMul (α := ℕ) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ) (dv i) = dv j • d
Tactic: classical
    rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]