awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
j : ι
hj :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
hj₀ : j = 0
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
exact (DFinsupp.mem_support_iff.mp hj <| hj₀ ▸ (by simpa using hx)).elim

Premises used: False.elim, Eq.rec, DFinsupp.mem_support_iff, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
j : ι
hj :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
hj₀ : j = 0
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
classical exact (DFinsupp.mem_support_iff.mp hj <| hj₀ ▸ (by simpa using hx)).elim

Premises used: False.elim, Eq.rec, DFinsupp.mem_support_iff, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
j : ι
hj :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
hj₀ : ¬j = 0
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
AddSubmonoid.mem_iSup_of_mem j <| AddSubmonoid.mem_iSup_of_mem (pos_of_ne_zero hj₀) <|
      Subtype.prop _

Premises used: Set.Mem, Subtype.prop, pos_of_ne_zero, AddSubmonoid.mem_iSup_of_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
x : A
hx : Membership.mem (γ := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊))) x
j : ι
hj :
  Membership.mem (γ := Finset ι)
    (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x)) j
hj₀ : ¬j = 0
⊢ Membership.mem (γ := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i))
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
exact AddSubmonoid.mem_iSup_of_mem j <| AddSubmonoid.mem_iSup_of_mem (pos_of_ne_zero hj₀) <|
      Subtype.prop _

Premises used: Subtype.prop, pos_of_ne_zero, AddSubmonoid.mem_iSup_of_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
rw :
  Eq.{u_3 + 1} (α := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), ofClass (𝒜 i))
    (closure (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))
⊢ Eq (α := AddSubmonoid A) (Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊)))
    (closure (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))

Tactic:
rw [irrelevant_eq_iSup]

Premises used: HomogeneousIdeal.irrelevant_eq_iSup
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
⊢ Eq.{u_3 + 1} (α := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), ofClass (𝒜 i))
    (closure (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))

Tactic:
le_antisymm (iSup_le fun i ↦ iSup_le fun hi _ hx ↦ subset_closure <| mem_biUnion hi hx) <|
    closure_le.mpr <| iUnion_subset fun i ↦ iUnion_subset fun hi ↦ le_biSup (ofClass <| 𝒜 ·) hi

Premises used: Iff.mpr, Set.iUnion_subset, AddSubmonoid.subset_closure, Set.mem_biUnion, le_antisymm, AddSubmonoid.closure_le, iSup_le, le_biSup, AddSubmonoid.ofClass
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
⊢ Eq.{u_3 + 1} (α := AddSubmonoid A) (⨆ (i : ι), ⨆ (_ : i > 0), ofClass (𝒜 i))
    (closure (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))

Tactic:
exact le_antisymm (iSup_le fun i ↦ iSup_le fun hi _ hx ↦ subset_closure <| mem_biUnion hi hx) <|
    closure_le.mpr <| iUnion_subset fun i ↦ iUnion_subset fun hi ↦ le_biSup (ofClass <| 𝒜 ·) hi

Premises used: Iff.mpr, Set.iUnion_subset, le_antisymm, AddSubmonoid.closure_le, iSup_le, le_biSup, AddSubmonoid.ofClass
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
⊢ Eq (α := Ideal A) (toIdeal (𝒜₊)) (Ideal.span (⋃ (i : ι), ⋃ (_ : i > 0), (↑(𝒜 i) : Set A)))

Tactic:
le_antisymm ((irrelevant_eq_closure 𝒜).trans_le <| closure_le.mpr Ideal.subset_span) <|
    Ideal.span_le.mpr <| iUnion_subset fun _ ↦ iUnion_subset fun hi _ hx ↦
    mem_irrelevant_of_mem _ hi hx

Premises used: Ideal.span_le, Iff.mpr, Ideal.subset_span, Set.iUnion_subset, HomogeneousIdeal.mem_irrelevant_of_mem, Eq.trans_le, le_antisymm, AddSubmonoid.closure_le, HomogeneousIdeal.irrelevant_eq_closure
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
P : AddSubmonoid A
rw : ⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i) ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
rw₁ rw₂ : (∀ (i : ι) (j : i > 0), AddSubmonoid.ofClass (𝒜 i) ≤ P) ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
⊢ Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊)) ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P

Tactic:
rw [irrelevant_eq_iSup, iSup₂_le_iff]

Premises used: iSup₂_le_iff, HomogeneousIdeal.irrelevant_eq_iSup
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
I : Ideal A
⊢ toIdeal (𝒜₊) ≤ I ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ I.toAddSubmonoid

Tactic:
toAddSubmonoid_irrelevant_le _

Premises used: Set.Mem, HomogeneousIdeal.toAddSubmonoid_irrelevant_le
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
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 𝒜
P : HomogeneousIdeal 𝒜
⊢ 𝒜₊ ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P.toAddSubmonoid

Tactic:
toIdeal_irrelevant_le _

Premises used: Set.Mem, HomogeneousIdeal.toIdeal_irrelevant_le
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
i : ι
b : B
hb : Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal) b
⊢ Membership.mem (γ := Submodule B B) (Ideal.span ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) b

Tactic:
rw [Ideal.map] at hb

Premises used: Ideal.map
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b : B
i : ι
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑(((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) 0 : (a : ι) → ↥(ℬ a)) i) : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b x y : B
hx : Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) x
hy : Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) y
h :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) x :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
h_1 :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) y :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
i : ι
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) (x + y) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
simp [*, Ideal.add_mem]

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a : B
ha : Membership.mem (γ := Set B) ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A)) a
i : ι
mem :
  ∀ (a : A) (ha : a ∈ (↑I.toIdeal : Set A)),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) a) :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
obtain ⟨a, ha, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b : B
i : ι
a : A
ha : a ∈ (↑I.toIdeal : Set A)
mem :
  Membership.mem.{u_2, u_2} (α := B) (γ := Submodule B B) (Ideal.map f I.toIdeal)
    ((f : (a : A) → B)
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) a :
                  DirectSum.{u_7, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              i) :
          A) :
      B)
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) a) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
rw [← f.map_directSumDecompose]

Premises used: GradedRingHom.map_directSumDecompose
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b : B
i : ι
a : A
ha : a ∈ (↑I.toIdeal : Set A)
⊢ Membership.mem.{u_2, u_2} (α := B) (γ := Submodule B B) (Ideal.map f I.toIdeal)
    ((f : (a : A) → B)
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) a :
                  DirectSum.{u_7, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              i) :
          A) :
      B)

Tactic:
Ideal.mem_map_of_mem _ (I.2 _ ha)

Premises used: Ideal.mem_map_of_mem, Set.Mem, HomogeneousSubmodule.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b : B
i : ι
a : A
ha : a ∈ (↑I.toIdeal : Set A)
⊢ Membership.mem.{u_2, u_2} (α := B) (γ := Submodule B B) (Ideal.map f I.toIdeal)
    ((f : (a : A) → B)
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) a :
                  DirectSum.{u_7, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              i) :
          A) :
      B)

Tactic:
exact Ideal.mem_map_of_mem _ (I.2 _ ha)

Premises used: Ideal.mem_map_of_mem, HomogeneousSubmodule.is_homogeneous'
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a₁ a₂ : B
ha₂ : Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) a₂
ih :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
i : ι
smul :
  Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (∑
      ij ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂)) with
      ij.1 + ij.2 = i,
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.1) :
          B) *
        (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.2) :
          B))
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) (a₁ • a₂) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]

Premises used: DirectSum.coe_mul_apply, DirectSum.decompose_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a₁ a₂ : B
ha₂ : Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) a₂
ih :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
i : ι
smul :
  Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (∑
      ij ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂)) with
      ij.1 + ij.2 = i,
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.1) :
          B) *
        (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.2) :
          B))
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) (a₁ • a₂) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)

Tactic:
classical rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]

Premises used: DirectSum.coe_mul_apply, DirectSum.decompose_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SetLike σ A
inst_4 : SetLike τ B
inst_5 : SetLike ω C
inst_6 : AddSubmonoidClass σ A
inst_7 : AddSubmonoidClass τ B
inst_8 : AddSubmonoidClass ω C
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_11 : GradedRing 𝒜
inst_12 : GradedRing ℬ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b a₁ a₂ : B
ha₂ : Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) a₂
ih :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
              (a : ι) → ↥(ℬ a))
            i) :
        B)
i : ι
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (∑
      ij ∈
        SProd.sprod (α := Finset ι) (β := Finset ι)
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁))
          (DFinsupp.support (β := fun (i : ι) ↦ ↥(ℬ i))
            ((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂)) with
      ij.1 + ij.2 = i,
      (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₁ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.1) :
          B) *
        (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) a₂ :
                  DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
                (a : ι) → ↥(ℬ a))
              ij.2) :
          B))

Tactic:
sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _

Premises used: Ideal.map, Prod.fst, Ideal.mul_mem_left, Subtype.val, HomogeneousIdeal.toIdeal, Prod.snd, DFunLike.coe, sum_mem, DirectSum.decompose