awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
pos :
  c * c' =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
pos₁ : c * c' = c * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
pos₂ pos₃ : c * c' = c * c'
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]

Premises used: DirectSum.decompose_of_mem_same, Eq.rec, And.right, And.left, Iff.mp, add_eq_zero, SetLike.GradedMul.mul_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
neg :
  0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (c * c') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]

Premises used: DirectSum.decompose_of_mem_ne, SetLike.GradedMul.mul_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
rwa : ∀ (h : ¬(i = 0 ∧ j = 0)), i ≠ 0 ∨ j ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : ¬i = 0 ∨ ¬j = 0), i ≠ 0 ∨ j ≠ 0
⊢ i ≠ 0 ∨ j ≠ 0

Tactic:
rwa [add_eq_zero, not_and_or] at h

Premises used: not_and_or, add_eq_zero
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
neg :
  ∀ (h' : i ≠ 0),
    0 =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
neg₁ :
  ∀ (h' : j ≠ 0),
    0 =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ 0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : i ≠ 0
⊢ 0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]

Premises used: MulZeroClass.zero_mul, DirectSum.decompose_of_mem_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : j ≠ 0
⊢ 0 =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) c' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]

Premises used: MulZeroClass.mul_zero, DirectSum.decompose_of_mem_ne
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m m' : A
hd :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * m) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
he :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * m') :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * (m + m')) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m + m') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]

Premises used: AddMemClass.coe_add, mul_add, DirectSum.decompose_add, DirectSum.add_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
m m' : A
ha :
  ∀ (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
hb :
  ∀ (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m' * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
y : A
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((m + m') * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m + m') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
simp only [add_mul, decompose_add, add_apply, AddMemClass.coe_add, ha, hb]

Premises used: add_mul, AddMemClass.coe_add, DirectSum.decompose_add, DirectSum.add_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
rw : (↑(((0 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) = 0
rw₁ : Eq.{u_3 + 1} (α := A) (↑0 : A) 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := A) 0 0
⊢ (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) = 0

Tactic:
rw [decompose_zero, zero_apply, ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero, DirectSum.decompose_zero, DirectSum.zero_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
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 𝒜
x x_1 : A
rw :
  (↑((HAdd.hAdd (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          0) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
rw₁ :
  (↑(HAdd.hAdd (α := ↥(𝒜 0))
          ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0)
          ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
rw₂ rw₃ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x + x_1) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) +
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x_1 : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
rw [decompose_add, add_apply, AddMemClass.coe_add]

Premises used: AddMemClass.coe_add, DirectSum.decompose_add, DirectSum.add_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 : A
⊢ Eq (α := A) ((↑(((projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0)) a) : A) : A)
    ((projZeroRingHom 𝒜 : (a : A) → A) a : A)

Tactic:
rfl

Premises used: rfl
-- 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 : ↥(𝒜 0)
a₁ : (↑(((projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0)) (↑a : A)) : A) = (↑a : A)
⊢ ((projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0)) (↑a : A) = a

Tactic:
ext
-- 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 : ↥(𝒜 0)
⊢ (↑(((projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0)) (↑a : A)) : A) = (↑a : A)

Tactic:
simp only [coe_projZeroRingHom'_apply, projZeroRingHom_apply, decompose_coe, of_eq_same]

Premises used: DirectSum.of_eq_same, GradedRing.projZeroRingHom_apply, DirectSum.decompose_coe, GradedRing.coe_projZeroRingHom'_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 𝒜
⊢ Function.Surjective (α := A) (β := ↥(𝒜 0)) (⇑(projZeroRingHom' 𝒜 : A →+* ↥(𝒜 0)) : (a : A) → ↥(𝒜 0))

Tactic:
Function.RightInverse.surjective (GradedRing.projZeroRingHom'_apply_coe 𝒜)

Premises used: GradedRing.projZeroRingHom'_apply_coe, Function.RightInverse.surjective
-- 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 : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ 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
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
lift :
  ∀ (a : ↥(𝒜 i)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 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
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
rwa :
  (↑((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) =
    0
rwa₁ :
  (↑((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) =
    0
rwa₂ : Eq.{u_3 + 1} (α := A) 0 0
h₁ : ¬i ≤ n
rwa₃ : Eq.{u_3 + 1} (α := A) 0 0
h₂ h₃ h₄ : ¬i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0

Tactic:
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]

Premises used: DirectSum.coe_of_mul_apply_of_not_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
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ 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
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
lift :
  ∀ (b : ↥(𝒜 i)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 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
n i : ι
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) =
    0
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) =
    0
rwa₂ : Eq.{u_3 + 1} (α := A) 0 0
h₁ : ¬i ≤ n
rwa₃ : Eq.{u_3 + 1} (α := A) 0 0
h₂ h₃ h₄ : ¬i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) = 0

Tactic:
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]

Premises used: DirectSum.coe_mul_of_apply_of_not_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
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
a_mem : a ∈ 𝒜 i
h : i ≤ n
⊢ 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
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
a_mem : a ∈ 𝒜 i
h : i ≤ n
lift :
  ∀ (a : ↥(𝒜 i)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
      (↑a : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)

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
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
rwa :
  (↑((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) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
rwa₁ :
  (↑((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) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
rwa₂ :
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
h₁ : i ≤ n
rwa₃ :
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)
h₂ h₃ h₄ : i ≤ n
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (n - i)) : A)

Tactic:
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]

Premises used: DirectSum.coe_of_mul_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
n i : ι
inst_8 : Sub ι
inst_9 : OrderedSub ι
inst_10 : AddLeftReflectLE ι
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ b ∈ 𝒜 i

Tactic:
b_mem