awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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 (α := at Submonoid.powers f)
    (val (Away.mk 𝒜 hf (dv j) (∏ i : ι', HPow.hPow (β := ℕ) (v i) (Pi.single (M := fun (a : ι') ↦ ℕ) j d i : ℕ)) ⋯))
    (val (isLocalizationElem hf ⋯))

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
⊢ ∀ (i : ↥s), 0 < (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i

Tactic:
simp [s]
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
refine_2 :
  ∀
    (this :
      Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_
              : ∀ (i : ↥s), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
        ⊤),
    Eq.{u_2 + 1} (α := 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})
      ⊤
refine_1 :
  Eq (α := Subalgebra (↥(𝒜 0)) A)
    (Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) ⊤
⊢ Eq.{u_2 + 1} (α := 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})
    ⊤

Tactic:
have := Away.adjoin_mk_prod_pow_eq_top_of_pos hf (ι' := s) (v ∘ Subtype.val) ?_
    (dv ∘ Subtype.val) (fun _ ↦ hxd _) (by simp [s])
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
refine_1 :
  ∀ (y : ι'),
    v y ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)
⊢ Eq (α := Subalgebra (↥(𝒜 0)) A)
    (Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) ⊤

Tactic:
rw [← top_le_iff, ← hx, Algebra.adjoin_le_iff, Set.range_subset_iff]

Premises used: Algebra.adjoin_le_iff, top_le_iff, Set.range_subset_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
i : ι'
refine_1 :
  ∀ (hi : dv i = 0),
    v i ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)
refine_1₁ :
  ∀ (hi : dv i > 0),
    v i ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)
⊢ v i ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)

Tactic:
rcases (dv i).eq_zero_or_pos with hi | hi

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
i : ι'
hi : dv i = 0
⊢ v i ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)

Tactic:
algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩

Premises used: Set.Mem, Eq.rec, Subtype.mk, algebraMap_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
i : ι'
hi : dv i = 0
⊢ v i ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)

Tactic:
exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩

Premises used: Eq.rec, Subtype.mk, algebraMap_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
i : ι'
hi : dv i > 0
⊢ i ∈ s

Tactic:
simpa [s] using hi
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
i : ι'
hi : dv i > 0
⊢ v i ∈ (↑(Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) : Set A)

Tactic:
exact Algebra.subset_adjoin ⟨⟨i, by simpa [s] using hi⟩, rfl⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
refine_2 :
  LE.le.{u_2} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    (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})
⊢ Eq.{u_2 + 1} (α := 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})
    ⊤

Tactic:
rw [← top_le_iff, ← this]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
refine_2 :
  Subset.{u_2} (α := Set (Away 𝒜 f))
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
        ∀ (i : ↥s), ai i ≤ d), Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x}
    {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}
⊢ LE.le.{u_2} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    (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})

Tactic:
apply Algebra.adjoin_mono

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x = a • d
h : ∀ (i : ↥s), 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 : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯)

Tactic:
⟨a, fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0, ?_, ?_, ?_⟩

Premises used: Set.Mem, setOf, Membership.mem, dite, Subtype.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
refine_2 :
  ∑ i : ι',
      HSMul.hSMul (α := ℕ)
        ((fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i) (dv i) =
    a • d
refine_2₁ :
  ∀ (i : ι'), (fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i ≤ d
refine_2₂ :
  Eq (α := Away 𝒜 f)
    (Away.mk 𝒜 hf a
      (∏ i : ι',
        HPow.hPow (β := ℕ) (v i)
          ((fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i))
      ⋯)
    (Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯)
⊢ 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 : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯)

Tactic:
refine ⟨a, fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0, ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ ∑ i : ι',
      HSMul.hSMul (α := ℕ)
        ((fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i) (dv i) =
    a • d

Tactic:
simpa [Finset.sum_attach_eq_sum_dite] using hai

Premises used: Finset.sum_attach_eq_sum_dite
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ ∀ (i : ι'), (fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i ≤ d

Tactic:
simp [apply_dite, dite_apply, h]

Premises used: apply_dite, dite_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
refine_2 :
  Eq.{u_2 + 1} (α := A)
    (∏ i : ι',
      HPow.hPow (β := ℕ) (v i)
        ((fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i))
    (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i)
⊢ Eq (α := Away 𝒜 f)
    (Away.mk 𝒜 hf a
      (∏ i : ι',
        HPow.hPow (β := ℕ) (v i)
          ((fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i))
      ⋯)
    (Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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)
s : Finset ι' := {x : ι' | 0 < dv x}
this :
  Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i = a • d) (_ :
          ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ↥s, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i ^ ai i) ⋯ = x})
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ Eq.{u_2 + 1} (α := A)
    (∏ i : ι',
      HPow.hPow (β := ℕ) (v i)
        ((fun (i : ι') ↦ (if hi : i ∈ s then ai (Subtype.mk (p := fun (x : ι') ↦ x ∈ s) i hi) else 0 : ℕ)) i))
    (∏ x ∈ s.attach, (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x ^ ai x)

Tactic:
simp [Finset.prod_attach_eq_prod_dite]

Premises used: Finset.prod_attach_eq_prod_dite
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
out : Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
⊢ Algebra.FiniteType.{u_2, u_2} (↥(𝒜 0)) (Away 𝒜 f)

Tactic:
constructor
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
out :
  ∀ (s : Finset A) (hs : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑s : Set A)) ⊤)
    (hs' : ∀ i ∈ s, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n), Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
⊢ Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤

Tactic:
obtain ⟨s, hs, hs'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜

Premises used: GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑s : Set A)) ⊤
hs' : ∀ i ∈ s, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
out :
  ∀ (dx : (x : ↥s) → ℕ) (hdx : ∀ (x : ↥s), dx x ≠ 0) (hxd : ∀ (x : ↥s), (↑x : A) ∈ 𝒜 (dx x)),
    Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
⊢ Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤

Tactic:
choose dx hdx hxd using Subtype.forall'.mp hs'

Premises used: Iff.mp, Subtype.forall'
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑s : Set A)) ⊤
hs' : ∀ i ∈ s, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
dx : (x : ↥s) → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), (↑x : A) ∈ 𝒜 (dx x)
⊢ Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) A)
    (Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑s : Set A)) ⊤
hs' : ∀ i ∈ s, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
dx : (x : ↥s) → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), (↑x : A) ∈ 𝒜 (dx x)
out :
  ∃ (t : Set (Away 𝒜 f)),
    t.Finite ∧
      LE.le (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ↥s → ℕ) (hai : ∑ i : ↥s, ai i • dx i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ↥s, (↑i : A) ^ ai i) ⋯ = x})
        (Algebra.adjoin (↥(𝒜 0)) t)
⊢ Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤

Tactic:
simp_rw [Subalgebra.fg_def, ← top_le_iff,
    ← Away.adjoin_mk_prod_pow_eq_top hf (ι' := s) Subtype.val (by simpa) dx hxd]

Premises used: HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top, Membership.mem, Subtype, Subalgebra.fg_def, top_le_iff, Subtype.val