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 𝒜
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 :
  ∀ (hd : d = 0),
    ∃ (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)
out₁ :
  ∀ (hd : d > 0),
    ∃ (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)
⊢ ∃ (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)

Tactic:
rcases d.eq_zero_or_pos with hd | hd

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 𝒜
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)
hd : d = 0
⊢ 1 ∈ 𝒜 (HSMul.hSMul (α := ℕ) 1 d)

Tactic:
simp [hd, GradedOne.one_mem]

Premises used: SetLike.GradedOne.one_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 𝒜
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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
⊢ ∃ (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)

Tactic:
⟨{f'}, Set.finite_singleton f', ?_⟩

Premises used: And.intro, Exists.intro, Singleton.singleton, Set.finite_singleton
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
out :
  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})
    (↥(𝒜 0))[f']
⊢ ∃ (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)

Tactic:
refine ⟨{f'}, Set.finite_singleton f', ?_⟩
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
out :
  {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} ⊆
    (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))
⊢ 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})
    (↥(𝒜 0))[f']

Tactic:
rw [Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_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 𝒜
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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i : ↥s, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ ∀ (x : ↥s), ai x = 0 x

Tactic:
simpa [hd, hdx] using hai
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i : ↥s, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
out :
  ∀ (hai : ∑ i : ↥s, HSMul.hSMul (α := ℕ) (0 i) (dx i) = a • d) (hai' : ∀ (i : ↥s), 0 i ≤ d),
    Away.mk 𝒜 hf a (∏ i : ↥s, HPow.hPow (β := ℕ) (↑i : A) (0 i)) ⋯ ∈ (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))
⊢ Away.mk 𝒜 hf a (∏ i : ↥s, (↑i : A) ^ ai i) ⋯ ∈ (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))

Tactic:
obtain rfl : ai = 0 := funext <| by simpa [hd, hdx] using hai

Premises used: funext, 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 𝒜
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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i : ↥s, HSMul.hSMul (α := ℕ) (0 i) (dx i) = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
out : Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) (↥(𝒜 0))[f'] (Away.mk 𝒜 hf a 1 ⋯)
⊢ Away.mk 𝒜 hf a (∏ i : ↥s, HPow.hPow (β := ℕ) (↑i : A) (0 i)) ⋯ ∈ (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))

Tactic:
simp only [Finset.univ_eq_attach, Pi.zero_apply, pow_zero, Finset.prod_const_one, mem_coe]

Premises used: Pi.zero_apply, pow_zero, Finset.prod_const_one, Finset.univ_eq_attach, SetLike.mem_coe
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i : ↥s, HSMul.hSMul (α := ℕ) (0 i) (dx i) = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) (↥(𝒜 0))[f'] (f' ^ a)

Tactic:
pow_mem (Algebra.self_mem_adjoin_singleton (𝒜 0) f') a

Premises used: Membership.mem, Subtype, pow_mem, OfNat.ofNat, Algebra.self_mem_adjoin_singleton
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i : ↥s, HSMul.hSMul (α := ℕ) (0 i) (dx i) = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
h : Away.mk 𝒜 hf a 1 ⋯ = f' ^ a
⊢ Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) (↥(𝒜 0))[f'] (Away.mk 𝒜 hf a 1 ⋯)

Tactic:
convert! pow_mem (Algebra.self_mem_adjoin_singleton (𝒜 0) f') a using 1

Premises used: Membership.mem, Subtype, pow_mem, OfNat.ofNat, Algebra.self_mem_adjoin_singleton
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i : ↥s, HSMul.hSMul (α := ℕ) (0 i) (dx i) = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
h : val (Away.mk 𝒜 hf a 1 ⋯) = val (f' ^ a)
⊢ Away.mk 𝒜 hf a 1 ⋯ = f' ^ a

Tactic:
ext
-- 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)
hd : d = 0
f' : Away 𝒜 f := Away.mk 𝒜 hf 1 1 ⋯
a : ℕ
hai : ∑ i : ↥s, HSMul.hSMul (α := ℕ) (0 i) (dx i) = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
⊢ val (Away.mk 𝒜 hf a 1 ⋯) = val (f' ^ a)

Tactic:
simp [f', Localization.mk_pow]

Premises used: Localization.mk_pow
-- 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)
hd : d > 0
⊢ ∃ (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)

Tactic:
⟨_, ?_, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro
-- 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)
hd : d > 0
out :
  Set.Finite.{u_2} (α := Away 𝒜 f)
    {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}
⊢ ∃ (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)

Tactic:
refine ⟨_, ?_, le_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 𝒜
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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
ai : (↑s' : Type u_2)
⊢ ∏ k : ↥s, (↑k : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 k) : ℕ) ∈
    𝒜 (∑ k : ↥s, (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 k) : ℕ) • dx k)

Tactic:
SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i

Premises used: SetLike.prod_pow_mem_graded
-- 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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
ai : (↑s' : Type u_2)
h :
  (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ) • d =
    ∑ k : ↥s, (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 k) : ℕ) • dx k
⊢ ∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ) ∈
    𝒜 ((↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ) • d)

Tactic:
convert! SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i

Premises used: SetLike.prod_pow_mem_graded
-- 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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
ai : (↑s' : Type u_2)
⊢ (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ) • d =
    ∑ k : ↥s, (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 k) : ℕ) • dx k

Tactic:
ai.2.symm

Premises used: Eq.symm, Subtype.property
-- 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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
ai : (↑s' : Type u_2)
⊢ (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ) • d =
    ∑ k : ↥s, (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 k) : ℕ) • dx k

Tactic:
exact ai.2.symm

Premises used: Eq.symm, Subtype.property
-- 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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
F : (↑s' : Type u_2) → Away 𝒜 f :=
  fun (ai : (↑s' : Type u_2)) ↦
    Away.mk 𝒜 hf (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ)
      (∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ)) ⋯
out :
  {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} ⊆
    Set.range F
⊢ Set.Finite.{u_2} (α := Away 𝒜 f)
    {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}

Tactic:
apply (Set.finite_range F).subset

Premises used: Set.finite_range, Set.Finite.subset
-- 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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
F : (↑s' : Type u_2) → Away 𝒜 f :=
  fun (ai : (↑s' : Type u_2)) ↦
    Away.mk 𝒜 hf (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ)
      (∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ)) ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i : ↥s, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
⊢ Away.mk 𝒜 hf a (∏ i : ↥s, (↑i : A) ^ ai i) ⋯ ∈ Set.range F

Tactic:
⟨⟨⟨⟨a, ?_⟩, fun i ↦ ⟨ai i, (hai' i).trans_lt d.lt_succ_self⟩⟩, hai⟩, rfl⟩

Premises used: Set.Mem, setOf, Fin.mk, Nat.lt_succ_self, Prod.mk, Subtype.mk, Exists.intro, Set.range, LE.le.trans_lt, 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 𝒜
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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
F : (↑s' : Type u_2) → Away 𝒜 f :=
  fun (ai : (↑s' : Type u_2)) ↦
    Away.mk 𝒜 hf (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ)
      (∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ)) ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i : ↥s, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
out : a < b + 1
⊢ Away.mk 𝒜 hf a (∏ i : ↥s, (↑i : A) ^ ai i) ⋯ ∈ Set.range F

Tactic:
refine ⟨⟨⟨⟨a, ?_⟩, fun i ↦ ⟨ai i, (hai' i).trans_lt d.lt_succ_self⟩⟩, hai⟩, 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 𝒜
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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
F : (↑s' : Type u_2) → Away 𝒜 f :=
  fun (ai : (↑s' : Type u_2)) ↦
    Away.mk 𝒜 hf (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ)
      (∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ)) ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i : ↥s, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
out : LE.le (α := ℕ) (∑ i : ↥s, ai i • dx i) (∑ i : ↥s, dx i * d)
⊢ a < b + 1

Tactic:
rw [Nat.lt_succ_iff, ← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul, ← hai, Finset.sum_mul]

Premises used: mul_le_mul_iff_of_pos_right, Nat.lt_succ_iff, smul_eq_mul, Finset.sum_mul
-- 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)
hd : d > 0
b : ℕ := ∑ i : ↥s, dx i
s' : Set (Fin (b + 1) × (↥s → Fin (d + 1))) :=
  {ai : Fin (b + 1) × (↥s → Fin (d + 1)) | ∑ i : ↥s, (↑(ai.2 i) : ℕ) * dx i = (↑ai.1 : ℕ) * d}
F : (↑s' : Type u_2) → Away 𝒜 f :=
  fun (ai : (↑s' : Type u_2)) ↦
    Away.mk 𝒜 hf (↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ)
      (∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ)) ⋯
a : ℕ
ai : ↥s → ℕ
hai : ∑ i : ↥s, ai i • dx i = a • d
hai' : ∀ (i : ↥s), ai i ≤ d
out : LE.le (α := ℕ) (∑ x : ↥s, ai x * dx x) (∑ x : ↥s, d * dx x)
⊢ LE.le (α := ℕ) (∑ i : ↥s, ai i • dx i) (∑ i : ↥s, dx i * d)

Tactic:
simp_rw [smul_eq_mul, mul_comm _ d]

Premises used: mul_comm, smul_eq_mul