awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊)) ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
have rw : ⨆ (i : ι), ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i) ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
Tactic: rw [irrelevant_eq_iSup, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal (goal)
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
⊢ Submodule.toAddSubmonoid (HomogeneousSubmodule.toSubmodule (𝒜₊)) ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
have rw₁ : (∀ (i : ι) (j : i > 0), AddSubmonoid.ofClass (𝒜 i) ≤ P) ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
Tactic: rw [irrelevant_eq_iSup, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (hypothesis)
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.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) b :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
have hb₁ : Membership.mem (γ := Submodule B B) (Ideal.span ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) b
Tactic: rw [Ideal.map] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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 : ι
⊢ 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)
have 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)
Tactic: obtain ⟨a, ha, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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 (γ := 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)
have 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)
Tactic: rw [← f.map_directSumDecompose]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) (a₁ • a₂) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
have 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))
Tactic: rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) (a₁ • a₂) :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
have 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))
Tactic: classical rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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.span ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) b
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) b :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
have zero : ∀ (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: induction hb using Submodule.span_induction generalizing i with
    | zero => simp
    | add => simp [*, Ideal.add_mem]
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      rw [← f.map_directSumDecompose]
      exact Ideal.mem_map_of_mem _ (I.2 _ ha)
    | smul a₁ a₂ ha₂ ih =>
      classical rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]
      exact sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _
Cleared hypotheses: i, hb
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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.span ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) b
zero :
  ∀ (i : ι),
    Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
      (↑(((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) 0 : (a : ι) → ↥(ℬ a)) i) : B)
⊢ Membership.mem (γ := Submodule B B) (Ideal.map f I.toIdeal)
    (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) b :
              DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
            (a : ι) → ↥(ℬ a))
          i) :
      B)
have add : ∀ (x y : B),
  Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) x →
    Membership.mem (γ := Submodule B B) (Submodule.span B ((⇑f : (a : A) → B) '' (↑I.toIdeal : Set A))) y →
      (∀ (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)) →
        (∀ (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: induction hb using Submodule.span_induction generalizing i with
    | zero => simp
    | add => simp [*, Ideal.add_mem]
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      rw [← f.map_directSumDecompose]
      exact Ideal.mem_map_of_mem _ (I.2 _ ha)
    | smul a₁ a₂ ha₂ ih =>
      classical rw [smul_eq_mul, DirectSum.decompose_mul, DirectSum.coe_mul_apply]
      exact sum_mem fun ij hij ↦ Ideal.mul_mem_left _ _ <| ih _
Cleared hypotheses: i, hb
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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 ℬ
n : ι
a : A
ha : Membership.mem (γ := Submodule A A) (Ideal.comap f I.toIdeal) a
⊢ Membership.mem (γ := Submodule A A) (Ideal.comap f I.toIdeal)
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) a :
              DirectSum.{u_7, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          n) :
      A)
have rw : (↑((((DirectSum.decompose ℬ : (a : B) → DirectSum ι fun (i : ι) ↦ ↥(ℬ i)) ((f : (a : A) → B) a) :
            DirectSum.{u_7, u_2} ι fun (i : ι) ↦ ↥(ℬ i)) :
          (a : ι) → ↥(ℬ a))
        n) :
    B) ∈
  I
Tactic: rw [Ideal.mem_comap, HomogeneousIdeal.mem_iff, f.map_directSumDecompose]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps (goal)
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
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 : AddCommMonoid ι
inst_11 : PartialOrder ι
inst_12 : CanonicallyOrderedAdd ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst_13 : GradedRing 𝒜
inst_14 : GradedRing ℬ
inst_15 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (ℬ₊))
⊢ LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map (g.comp f) (𝒜₊))
have rw : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (map g (map f (𝒜₊)))
Tactic: rw [map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
⊢ I = J
have h₁ : ∀ (x : M), x ∈ I.toSubmodule ↔ x ∈ J.toSubmodule
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
x : M
⊢ x ∈ I.toSubmodule ↔ x ∈ J.toSubmodule
have h₁ : (∀ (i : ιM),
    (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
      I.toSubmodule) ↔
  ∀ (i : ιM),
    (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
      J.toSubmodule
Tactic: rw [I.isHomogeneous.mem_iff, J.isHomogeneous.mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst : Semiring A
inst_1 : AddCommMonoid M
inst_2 : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst_3 : DecidableEq ιA
inst_4 : AddMonoid ιA
inst_5 : SetLike σA A
inst_6 : AddSubmonoidClass σA A
inst_7 : GradedRing 𝒜
inst_8 : DecidableEq ιM
inst_9 : SetLike σM M
inst_10 : AddSubmonoidClass σM M
inst_11 : Decomposition ℳ
inst_12 : VAdd ιA ιM
inst_13 : GradedSMul 𝒜 ℳ
I J : HomogeneousSubmodule 𝒜 ℳ
h : ∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J
x : M
⊢ (∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
        I.toSubmodule) ↔
    ∀ (i : ιM),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) i) : M) ∈
        J.toSubmodule
have h₁ : ∀ (a : ιM),
  (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
      I.toSubmodule ↔
    (↑((((decompose ℳ : (a : M) → ⨁ (i : ιM), ↥(ℳ i)) x : ⨁ (i : ιM), ↥(ℳ i)) : (a : ιM) → ↥(ℳ a)) a) : M) ∈
      J.toSubmodule
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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 : A
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 : (a : ι) → ↥(𝒜 a)) i) : A)
have one : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
  (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
              (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A)
Tactic: rw [decompose_one, one_def]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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 : A
i : ι
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
have one : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
  (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
              (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        0) :
    A)
Tactic: obtain rfl | h := eq_or_ne i 0
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
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 : A
i : ι
one :
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
have one₁ : ∀ (h : i ≠ 0),
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                (@GradedMonoid.GOne.one _ (fun (i : ι) ↦ ↥(𝒜 i)) AddZero.toZero _) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A)
Tactic: obtain rfl | h := eq_or_ne i 0