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)
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})
      ⊤
⊢ 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})
    ⊤
have 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)))) ⊤
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]
-- 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 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
⊢ Algebra.FiniteType.{u_2, u_2} (↥(𝒜 0)) (Away 𝒜 f)
have out : Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
Tactic: constructor
-- 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 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
⊢ Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
have 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) ⊤
Tactic: obtain ⟨s, hs, hs'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
-- 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 𝒜
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
⊢ Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
have 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) ⊤
Tactic: choose dx hdx hxd using Subtype.forall'.mp 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 𝒜
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)
⊢ Subalgebra.FG.{u_2, u_2} (R := ↥(𝒜 0)) (A := Away 𝒜 f) ⊤
have 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) sorry = x})
      (Algebra.adjoin (↥(𝒜 0)) t)
Tactic: simp_rw [Subalgebra.fg_def, ← top_le_iff,
    ← Away.adjoin_mk_prod_pow_eq_top hf (ι' := s) Subtype.val (by simpa) dx hxd]
-- 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 𝒜
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)
⊢ ∃ (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)
have 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) sorry = x})
        (Algebra.adjoin (↥(𝒜 0)) t)
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 𝒜
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)
⊢ ∃ (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)
have 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) sorry = x})
        (Algebra.adjoin (↥(𝒜 0)) t)
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 𝒜
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)
have 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) sorry = x})
  (↥(𝒜 0))[f']
Tactic: refine ⟨{f'}, Set.finite_singleton f', ?_⟩
-- 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 𝒜
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 ⋯
⊢ 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']
have 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) sorry = x} ⊆
  (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))
Tactic: rw [Algebra.adjoin_le_iff]
-- 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 𝒜
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
⊢ Away.mk 𝒜 hf a (∏ i : ↥s, (↑i : A) ^ ai i) ⋯ ∈ (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))
have 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)) sorry ∈ (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))
Tactic: obtain rfl : ai = 0 := funext <| by simpa [hd, hdx] using hai
Cleared hypotheses: ai, hai, 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 𝒜
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
⊢ Away.mk 𝒜 hf a (∏ i : ↥s, HPow.hPow (β := ℕ) (↑i : A) (0 i)) ⋯ ∈ (↑(↥(𝒜 0))[f'] : Set (Away 𝒜 f))
have out : Membership.mem (γ := Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) (↥(𝒜 0))[f'] (Away.mk 𝒜 hf a 1 sorry)
Tactic: simp only [Finset.univ_eq_attach, Pi.zero_apply, pow_zero, Finset.prod_const_one, mem_coe]
-- 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 𝒜
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'] (Away.mk 𝒜 hf a 1 ⋯)
have h : Away.mk 𝒜 hf a 1 sorry = f' ^ a
Tactic: convert! pow_mem (Algebra.self_mem_adjoin_singleton (𝒜 0) f') a using 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 𝒜
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
⊢ Away.mk 𝒜 hf a 1 ⋯ = f' ^ a
have h : val (Away.mk 𝒜 hf a 1 sorry) = val (f' ^ a)
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 𝒜
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)
have 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) sorry = x}
Tactic: refine ⟨_, ?_, le_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 𝒜
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)
⊢ ∏ i : ↥s, (↑i : A) ^ (↑((↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).2 i) : ℕ) ∈
    𝒜 ((↑(↑ai : Fin (b + 1) × (↥s → Fin (d + 1))).1 : ℕ) • d)
have 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
Tactic: convert! SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
-- 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 𝒜
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) : ℕ)) ⋯
⊢ 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}
have 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) sorry = x} ⊆
  Set.range F
Tactic: apply (Set.finite_range F).subset
-- 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 𝒜
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
have out : a < b + 1
Tactic: refine ⟨⟨⟨⟨a, ?_⟩, fun i ↦ ⟨ai i, (hai' i).trans_lt d.lt_succ_self⟩⟩, hai⟩, 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 𝒜
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
⊢ a < b + 1
have out : LE.le (α := ℕ) (∑ i : ↥s, ai i • dx i) (∑ i : ↥s, dx i * d)
Tactic: rw [Nat.lt_succ_iff, ← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul, ← hai, Finset.sum_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 𝒜
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
⊢ LE.le (α := ℕ) (∑ i : ↥s, ai i • dx i) (∑ i : ↥s, dx i * d)
have out : LE.le (α := ℕ) (∑ x : ↥s, ai x * dx x) (∑ x : ↥s, d * dx x)
Tactic: simp_rw [smul_eq_mul, mul_comm _ 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 𝒜
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
⊢ LE.le (α := ℕ) (∑ x : ↥s, ai x * dx x) (∑ x : ↥s, d * dx x)
have out : ∀ (i : ↥s), Membership.mem (γ := Finset ↥s) Finset.univ i → ai i ≤ d
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
have by_contra! : ∀ (rid₁ : x ∉ I) (rid₂ : y ∉ I), False
Tactic: by_contra! ⟨rid₁, rid₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Radical (hypothesis)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : CommRing A
inst_1 : AddCommMonoid ι
inst_2 : LinearOrder ι
inst_3 : IsOrderedCancelAddMonoid ι
inst_4 : SetLike σ A
inst_5 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_6 : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x y : A
hxy : x * y ∈ I
rid₁ : x ∉ I
rid₂ : y ∉ I
⊢ False
have set₁_eq : let set₁ : Finset ι :=
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I};
set₁ =
  {i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x) |
    ((proj 𝒜 i : (a : A) → A) x : A) ∉ I}
Tactic: set set₁ := {i ∈ (decompose 𝒜 x).support | proj 𝒜 i x ∉ I} with set₁_eq