awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
mul :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y),
      (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + i_1) : ↥(𝒜 (j + i_1)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + i_1))) → ⨁ (i : ι), ↥(𝒜 i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i_1)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((DFinsupp.sum (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)
                fun (x_2 : ι) (aj : ↥(𝒜 x_2)) ↦
                ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + x_2) : ↥(𝒜 (j + x_2)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + x_2))) → ⨁ (i : ι), ↥(𝒜 i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) aj) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]

Premises used: AddSubmonoidClass.coe_finsetSum, DFinsupp.sum, DFinsupp.sum_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y),
      (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + i_1) : ↥(𝒜 (j + i_1)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + i_1))) → ⨁ (i : ι), ↥(𝒜 i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i_1)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))

Tactic:
sum_mem fun k _ ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
mul :
  ∀ (k : ι),
    Membership.mem (γ := Finset ι)
        (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) k →
      Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
        (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + k) : ↥(𝒜 (j + k)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 (j + k))) → ⨁ (i : ι), ↥(𝒜 i))
                    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k)) :
                  ⨁ (i : ι), ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              i) :
          A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (∑ i_1 ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y),
      (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + i_1) : ↥(𝒜 (j + i_1)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 (j + i_1))) → ⨁ (i : ι), ↥(𝒜 i))
                  (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i_1)) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            i) :
        A))

Tactic:
refine sum_mem fun k _ ↦ ?_

Premises used: sum_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
j : ι
h_1 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
k : ι
h_2 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) k
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + k) : ↥(𝒜 (j + k)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ↥(𝒜 (j + k))) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (j + k)) :
      A)

Tactic:
simp [of_eq_of_ne, mul_mem, *]

Premises used: MulMemClass.mul_mem, DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h_1 :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
x_1 x y : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
hy : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y
h₁ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
h₂ :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
i j : ι
h_2 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
k : ι
h_3 :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y)) k
h : i ≠ j + k
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) (j + k) : ↥(𝒜 (j + k)) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ↥(𝒜 (j + k))) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j)
                  ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) k)) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)

Tactic:
simp [of_eq_of_ne, mul_mem, *]

Premises used: MulMemClass.mul_mem, DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
rw : IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure (insert 0 s))
⊢ IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure s)

Tactic:
rw [← Subsemiring.closure_insert_zero s]

Premises used: Subsemiring.closure_insert_zero
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
⊢ IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure (insert 0 s))

Tactic:
IsHomogeneous.subsemiringClosure fun i x hx ↦ ?_

Premises used: IsHomogeneous.subsemiringClosure
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
refine :
  ∀ (i : ι) (x : A) (hx : x ∈ insert 0 s),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
⊢ IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure (insert 0 s))

Tactic:
refine IsHomogeneous.subsemiringClosure fun i x hx ↦ ?_

Premises used: IsHomogeneous.subsemiringClosure
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx : x ∈ insert 0 s
inl :
  ∀ (hx : 0 ∈ insert 0 s), (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
inr :
  ∀ (hx : x ∈ s),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s

Tactic:
obtain rfl | hx := mem_insert_iff.mp hx

Premises used: Iff.mp, Set.mem_insert_iff, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
hx : 0 ∈ insert 0 s
⊢ (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
inr :
  ∀ (j : ι) (hj : x ∈ 𝒜 j),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s

Tactic:
obtain ⟨j, hj⟩ := h x hx
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
inr :
  ∀ (hj : x ∈ 𝒜 i),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
inr₁ :
  ∀ (h : i ≠ j),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s

Tactic:
obtain rfl | h := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
hj : x ∈ 𝒜 i
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s

Tactic:
simp [decompose_of_mem _ hj, of_eq_of_ne, *]

Premises used: DirectSum.decompose_of_mem, DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h_1 : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
h : i ≠ j
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s

Tactic:
simp [decompose_of_mem _ hj, of_eq_of_ne, *]

Premises used: DirectSum.decompose_of_mem, DirectSum.of_eq_of_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : Subsemiring A
x : Subtype (IsHomogeneousElem 𝒜)
left :
  Membership.mem (γ := Set (Subtype (IsHomogeneousElem 𝒜))) (Subtype.val (p := IsHomogeneousElem 𝒜) ⁻¹' (↑R : Set A)) x
⊢ IsHomogeneousElem 𝒜 (↑x : A)

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : Subsemiring A
x : Subtype (IsHomogeneousElem 𝒜)
left :
  Membership.mem (γ := Set (Subtype (IsHomogeneousElem 𝒜))) (Subtype.val (p := IsHomogeneousElem 𝒜) ⁻¹' (↑R : Set A)) x
⊢ IsHomogeneousElem 𝒜 (↑x : A)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ Monotone (α := Subsemiring A) (β := HomogeneousSubsemiring 𝒜) (homogeneousCore 𝒜)

Tactic:
fun _ _ h => Subsemiring.closure_mono <| Set.image_mono <| fun _ ↦ @h _

Premises used: Subsemiring.closure_mono, Set.Mem, Set.image_mono, Monotone
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : Subsemiring A
⊢ HomogeneousSubsemiring.toSubsemiring (homogeneousCore 𝒜 R) ≤ R

Tactic:
Subsemiring.closure_le.2 <| image_preimage_subset _ _

Premises used: Iff.mpr, Subsemiring.closure_le, Set.Mem, Set.image_preimage_subset
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : Subsemiring A
⊢ IsHomogeneous 𝒜 R ↔ ∀ (i : ι), (↑R : Set A) ⊆ (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) ⁻¹' (↑R : Set A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Set.preimage, DirectSum.SetLike.IsHomogeneous
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
R : Subsemiring A
⊢ IsHomogeneous 𝒜 R ↔ (↑R : Set A) ⊆ ⋂ (i : ι), (⇑(GradedRing.proj 𝒜 i) : (a : A) → A) ⁻¹' (↑R : Set A)

Tactic:
subset_iInter_iff.symm

Premises used: Set.subset_iInter_iff, Set.Mem, setOf, Set.Subset, Set.preimage, DirectSum.SetLike.IsHomogeneous, Iff.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
hdeg : c1.deg = c2.deg
hnum : (↑c1.num : A) = (↑c2.num : A)
hden : (↑c1.den : A) = (↑c2.den : A)
rcases :
  ∀ (i1 : ι) (n1 : A) (hn1 : n1 ∈ 𝒜 i1) (d1 : A) (hd1 : d1 ∈ 𝒜 i1)
    (h1 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1) : A) ∈ x)
    (hdeg :
      { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.deg =
        c2.deg)
    (hnum :
      (↑{ deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.num :
          A) =
        (↑c2.num : A))
    (hden :
      (↑{ deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.den :
          A) =
        (↑c2.den : A)),
    { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x } =
      c2
⊢ c1 = c2

Tactic:
rcases c1 with ⟨i1, ⟨n1, hn1⟩, ⟨d1, hd1⟩, h1⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
c2 : NumDenSameDeg 𝒜 x
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1) : A) ∈ x
hdeg :
  { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.deg =
    c2.deg
hnum :
  (↑{ deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.num :
      A) =
    (↑c2.num : A)
hden :
  (↑{ deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.den :
      A) =
    (↑c2.den : A)
rcases :
  ∀ (i2 : ι) (n2 : A) (hn2 : n2 ∈ 𝒜 i2) (d2 : A) (hd2 : d2 ∈ 𝒜 i2)
    (h2 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2) : A) ∈ x)
    (hdeg :
      { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.deg =
        { deg := i2, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) n2 hn2,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2, den_mem := h2 : NumDenSameDeg 𝒜 x }.deg)
    (hnum :
      (↑{ deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.num :
          A) =
        (↑{ deg := i2, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) n2 hn2,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2, den_mem := h2 : NumDenSameDeg 𝒜 x }.num :
          A))
    (hden :
      (↑{ deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x }.den :
          A) =
        (↑{ deg := i2, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) n2 hn2,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2, den_mem := h2 : NumDenSameDeg 𝒜 x }.den :
          A)),
    { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x } =
      { deg := i2, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) n2 hn2,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2, den_mem := h2 }
⊢ { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x } =
    c2

Tactic:
rcases c2 with ⟨i2, ⟨n2, hn2⟩, ⟨d2, hd2⟩, h2⟩