-- 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)
let let₁ let₂ :
  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_2 :
  let 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})
        ⊤),
    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 refine_1₁ :
  let s : Finset ι' := {x : ι' | 0 < dv x};
  Eq (α := Subalgebra (↥(𝒜 0)) A)
    (Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥s) (v ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) ⊤
refine_2₁ refine_2₂ :
  let 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})
        ⊤),
    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_2₃ :
  let 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})
        ⊤),
    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})
refine_2₄ :
  let 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})
        ⊤),
    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}
refine_2₅ :
  let 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) ⋯)
refine_2₆ :
  let 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
refine_2₇ :
  let 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
refine_2₈ :
  let 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 (α := 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) ⋯)
refine_2₉ :
  let 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
refine_2₁₀ refine_2₁₁ :
  let 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 (α := 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) ⋯)
⊢ 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:
classical
  let s := Finset.univ.filter (0 < dv ·)
  have := Away.adjoin_mk_prod_pow_eq_top_of_pos hf (ι' := s) (v ∘ Subtype.val) ?_
    (dv ∘ Subtype.val) (fun _ ↦ hxd _) (by simp [s])
  swap
  · rw [← top_le_iff, ← hx, Algebra.adjoin_le_iff, Set.range_subset_iff]
    intro i
    rcases (dv i).eq_zero_or_pos with hi | hi
    · exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩
    exact Algebra.subset_adjoin ⟨⟨i, by simpa [s] using hi⟩, rfl⟩
  rw [← top_le_iff, ← this]
  apply Algebra.adjoin_mono
  rintro _ ⟨a, ai, hai : ∑ x ∈ s.attach, _ = _, h, rfl⟩
  refine ⟨a, fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0, ?_, ?_, ?_⟩
  · simpa [Finset.sum_attach_eq_sum_dite] using hai
  · simp [apply_dite, dite_apply, h]
  · congr 1
    change _ = ∏ x ∈ s.attach, _
    simp [Finset.prod_attach_eq_prod_dite]

Premises used: apply_dite, Finset.sum_attach_eq_sum_dite, Finset.prod_attach_eq_prod_dite, Algebra.adjoin_mono, Algebra.adjoin_le_iff, top_le_iff, dite_apply, Set.range_subset_iff, rfl