awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
b_mem : b ∈ 𝒜 i
h : i ≤ n
lift :
  ∀ (b : ↥(𝒜 i)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) *
        (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * b

Tactic:
lift b to 𝒜 i using b_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
rwa :
  (↑((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) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
rwa₁ :
  (↑((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) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
rwa₂ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
h₁ : i ≤ n
rwa₃ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)
h₂ h₃ h₄ : i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) * (↑b : A)

Tactic:
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]

Premises used: DirectSum.coe_mul_of_apply_of_le, DirectSum.decompose_mul, DirectSum.decompose_coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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)
a_mem : a ∈ 𝒜 i
⊢ a ∈ 𝒜 i

Tactic:
a_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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)
a_mem : a ∈ 𝒜 i
lift :
  ∀ (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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    if i ≤ n then
      a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
    else 0

Tactic:
lift a to 𝒜 i using a_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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
rw₂ 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
⊢ (↑((((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

Tactic:
rw [decompose_mul, decompose_coe, coe_of_mul_apply]

Premises used: DirectSum.decompose_mul, DirectSum.decompose_coe, DirectSum.coe_of_mul_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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
⊢ b ∈ 𝒜 i

Tactic:
b_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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
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
⊢ (↑((((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

Tactic:
lift b to 𝒜 i using b_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
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
rw₂ 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
⊢ (↑((((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:
rw [decompose_mul, decompose_coe, coe_mul_of_apply]

Premises used: DirectSum.coe_mul_of_apply, DirectSum.decompose_mul, DirectSum.decompose_coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι_1 : Type u_1
R_1 : Type u_2
A_1 : Type u_3
σ : Type u_4
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Type u_7
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
M : ι → Submodule R A
inst_5 : SetLike.GradedMonoid M
hM : IsInternal M
r : R
⊢ (RingEquiv.toEquiv (RingEquiv.ofBijective (coeAlgHom M) hM)).toFun
      ((algebraMap R (⨁ (i : ι), ↥(M i)) : (a : R) → ⨁ (i : ι), ↥(M i)) r) =
    (algebraMap R A : (a : R) → A) r

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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
⊢ ∃ (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)

Premises used: Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
⊢ ∀ i ∈ Finset.image x Finset.univ, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
refine : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) ⊤
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
rw : (↑F : Set S) ⊆ (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
⊢ Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) ⊤

Tactic:
rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff, top_le_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
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)
⊢ s ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 s]

Premises used: DirectSum.sum_support_decompose
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
n : ι
hn :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
      ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) s))
    n
⊢ (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) s :
              DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      S) ∈
    (↑(Finset.image x Finset.univ) : Set S)

Tactic:
simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
⊢ ∑
      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:
exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)

Premises used: Algebra.subset_adjoin, sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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 :
  ∀ (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
⊢ ∃ (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 𝒜

Premises used: GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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
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
⊢ ∃ (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₂
-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
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)
⊢ ∀ i ∈ {x ∈ s | n x ≠ 0}, ∃ (n : ι), n ≠ 0 ∧ i ∈ 𝒜 n

Tactic:
simpa using fun i hi hin ↦ ⟨n i, hin, hn i hi⟩