awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
b : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
have rw : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  if i ≤ n then
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
  else 0
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
b : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
a : ↥(𝒜 i)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
have rw₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                a :
              ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  if i ≤ n then
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
  else 0
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
b : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
a : ↥(𝒜 i)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0
have rw₂ : (if i ≤ n then
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
  else 0) =
  if i ≤ n then
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
  else 0
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
a b : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * b
    else 0
have lift : ∀ (b : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
Tactic: lift b to 𝒜 i using b_mem
Cleared hypotheses: b, b_mem
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
a : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
have rw : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  if i ≤ n then
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
  else 0
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
a : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
b : ↥(𝒜 i)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
have rw₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                b :
              ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        n) :
    A) =
  if i ≤ n then
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
  else 0
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
a : A
i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
n : ι
inst_11 : Decidable (i ≤ n)
b : ↥(𝒜 i)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
    else 0
have rw₂ : (if i ≤ n then
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
  else 0) =
  if i ≤ n then
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
  else 0
Tactic: rw [decompose_mul, decompose_coe, coe_mul_of_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
have obtain : ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
  ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
Tactic: obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤
ι₀ : Type (max u_1 u_3) :=
  (x : ↥F) ×
    ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)))
x : (i : ι₀) → S :=
  fun (i : ι₀) ↦
    (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                (↑(i.fst (β := fun (x : ↥F) ↦
                      ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                          ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                  S) :
              DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (↑(i.snd (β := fun (x : ↥F) ↦
                ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                    ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
            ι)) :
      S)
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
have refine : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) ⊤
Tactic: refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤
ι₀ : Type (max u_1 u_3) :=
  (x : ↥F) ×
    ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)))
x : (i : ι₀) → S :=
  fun (i : ι₀) ↦
    (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                (↑(i.fst (β := fun (x : ↥F) ↦
                      ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                          ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                  S) :
              DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (↑(i.snd (β := fun (x : ↥F) ↦
                ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                    ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
            ι)) :
      S)
⊢ Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) ⊤
have rw : (↑F : Set S) ⊆ (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
Tactic: rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤
ι₀ : Type (max u_1 u_3) :=
  (x : ↥F) ×
    ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)))
x : (i : ι₀) → S :=
  fun (i : ι₀) ↦
    (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                (↑(i.fst (β := fun (x : ↥F) ↦
                      ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                          ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                  S) :
              DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (↑(i.snd (β := fun (x : ↥F) ↦
                ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                    ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
            ι)) :
      S)
s : S
hs : s ∈ (↑F : Set S)
⊢ s ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
have rw : ∑
    i ∈
      DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) s),
    (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) s :
              DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      S) ∈
  (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 s]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
have obtain : ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
  ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
Tactic: classical
  obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)
  let ι₀ := Σ (x : F), (DirectSum.decompose 𝒜 x.1).support
  let x (i : ι₀) : S := ((DirectSum.decompose 𝒜) i.1 i.2).1
  refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
  rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]
  intro s hs
  rw [← DirectSum.sum_support_decompose 𝒜 s]
  exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
obtain :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    ∃ (s : Finset S),
      Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
obtain₁ obtain₂ :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    ∃ (s : Finset S),
      Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
have obtain₃ : ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
  let ι₀ :=
    (x : ↥F) ×
      ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)));
  let x : (i : ι₀) → S := fun (i : ι₀) ↦
    (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                (↑(i.fst (β := fun (x : ↥F) ↦
                      ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                          ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                  S) :
              DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (↑(i.snd (β := fun (x : ↥F) ↦
                ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                    ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
            ι)) :
      S);
  Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) ⊤
Tactic: classical
  obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)
  let ι₀ := Σ (x : F), (DirectSum.decompose 𝒜 x.1).support
  let x (i : ι₀) : S := ((DirectSum.decompose 𝒜) i.1 i.2).1
  refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
  rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]
  intro s hs
  rw [← DirectSum.sum_support_decompose 𝒜 s]
  exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n
have obtain : ∀ (s : Finset S) (h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤)
  (h₂ : ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i),
  ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n
Tactic: obtain ⟨s, h₁, h₂⟩ := exists_finset_adjoin_eq_top_and_homogeneous 𝒜
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
h₂ : ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n
have choose! : ∀ (n : (i : S) → ι) (hn : ∀ i ∈ s, i ∈ 𝒜 (n i)),
  ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n
Tactic: choose! n hn using h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n
have refine : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) ⊤
Tactic: refine ⟨s.filter (n · ≠ 0), ?_, by simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.FiniteType (goal)
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤
n : (i : S) → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) ⊤
have rw : (↑s : Set S) ⊆ (↑(Algebra.adjoin ↥(𝒜 0) (↑({x ∈ s | n x ≠ 0}) : Set S)) : Set S)
Tactic: rw [← top_le_iff, ← h₁, Algebra.adjoin_le_iff]