awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          j) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          j) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
rw₂ rw₃ :
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]

Premises used: DirectSum.coe_of_mul_apply_of_mem_zero, DirectSum.decompose_mul, DirectSum.decompose_coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 0
⊢ b ∈ 𝒜 0

Tactic:
b_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 0
lift :
  ∀ (b : ↥(𝒜 0)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * b

Tactic:
lift b to 𝒜 0 using b_mem

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑b : A) : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) 0 : ↥(𝒜 0) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 0)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
rw₂ rw₃ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)

Tactic:
rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]

Premises used: DirectSum.coe_mul_of_apply_of_mem_zero, DirectSum.decompose_mul, DirectSum.decompose_coe
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i))
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i)) x :
        ⨁ (i : ι), ↥(𝒜 i))
suffices : decompose.comp (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))
⊢ Function.RightInverse (α := A) (β := ⨁ (i : ι), ↥(𝒜 i)) (⇑(DirectSum.coeAddMonoidHom 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
    (⇑decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i))

Tactic:
suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i))
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i)) x :
        ⨁ (i : ι), ↥(𝒜 i))
h :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i))
      ((AlgHom.toLinearMap (decompose.comp (coeAlgHom 𝒜)) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
            (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          x :
        ⨁ (i : ι), ↥(𝒜 i))
      ((AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
            (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          x :
        ⨁ (i : ι), ↥(𝒜 i))
⊢ decompose.comp (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))

Tactic:
ext i x : 2
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i))
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i)) x :
        ⨁ (i : ι), ↥(𝒜 i))
i : ι
x : ↥(𝒜 i)
⊢ Eq (α := ⨁ (i : ι), ↥(𝒜 i))
    ((AlgHom.toLinearMap (decompose.comp (coeAlgHom 𝒜)) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
          (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        x :
      ⨁ (i : ι), ↥(𝒜 i))
    ((AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
          (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        x :
      ⨁ (i : ι), ↥(𝒜 i))

Tactic:
(decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x)

Premises used: Multiset.sum, Multiset.foldr, DirectSum.coeAlgHom_of, AlgHom.congr_arg, List.foldr, Finset.sum, Eq.trans, Trunc.lift
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv :
  ∀ (i : ι) (x : ↥(𝒜 i)),
    Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑x : A) : ⨁ (i : ι), ↥(𝒜 i))
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i)) x :
        ⨁ (i : ι), ↥(𝒜 i))
i : ι
x : ↥(𝒜 i)
⊢ Eq (α := ⨁ (i : ι), ↥(𝒜 i))
    ((AlgHom.toLinearMap (decompose.comp (coeAlgHom 𝒜)) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
          (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        x :
      ⨁ (i : ι), ↥(𝒜 i))
    ((AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(𝒜 i)) i :
          (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        x :
      ⨁ (i : ι), ↥(𝒜 i))

Tactic:
exact (decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x)

Premises used: DirectSum.coeAlgHom_of, AlgHom.congr_arg, Eq.trans
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
a : A
⊢ Eq (α := ⨁ (i : ι), ↥(𝒜 i))
    (((decomposeAlgEquiv 𝒜 : A ≃ₐ[R] ⨁ (i : ι), ↥(𝒜 i)) : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ Eq.{u_3 + 1} (α := A)
    (((AlgEquiv.symm (decomposeAlgEquiv 𝒜) : (⨁ (i : ι), ↥(𝒜 i)) ≃ₐ[R] A) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
r : R
⊢ Eq (α := ⨁ (i : ι), ↥(𝒜 i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) : ⨁ (i : ι), ↥(𝒜 i))
    ((algebraMap R (⨁ (i : ι), ↥(𝒜 i)) : (a : R) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i))

Tactic:
(decomposeAlgEquiv 𝒜).commutes r

Premises used: DirectSum.decomposeAlgEquiv, AlgEquiv.commutes
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
r : R
⊢ Eq.{u_3 + 1} (α := A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        ((algebraMap R (⨁ (i : ι), ↥(𝒜 i)) : (a : R) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) :
      A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
(decomposeAlgEquiv 𝒜).symm.commutes r

Premises used: AlgEquiv.symm, DirectSum.decomposeAlgEquiv, AlgEquiv.commutes
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
i : ι
r : A
⊢ (proj 𝒜 i : (a : A) → A) r =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
rw :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          ((a : (a : ι) → ↥(𝒜 a)) i) :
        ⨁ (i : ι), ↥(𝒜 i))
rw₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
rw₂ rw₃ : (↑((a : (a : ι) → ↥(𝒜 a)) i) : A) = (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)

Tactic:
rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, GradedAlgebra.proj_apply, DirectSum.decompose_symm_of
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
inst_6 : DecidableEq A
r : A
i : ι
⊢ Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) r)) i ↔
    Ne (α := A) ((proj 𝒜 i : (a : A) → A) r : A) (0 : A)

Tactic:
DFinsupp.mem_support_iff.trans Submodule.coe_eq_zero.not.symm

Premises used: Iff.not, DFinsupp.mem_support_iff, Submodule.coe_eq_zero, Iff.trans, Iff.symm
-- 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 y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
DirectSum.Decomposition.inductionOn 𝒜 (fun x => ?_) ?_ ?_

Premises used: DirectSum.Decomposition.inductionOn
-- 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 𝒜
refine_1 :
  ∀ (x : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (0 * x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
refine_2 :
  ∀ {i : ι} (m : ↥(𝒜 i)) (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑m : A) * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑m : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
refine_3 :
  ∀ (m m' : A),
    (∀ (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' * 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)
⊢ ∀ (x y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
refine DirectSum.Decomposition.inductionOn 𝒜 (fun x => ?_) ?_ ?_
-- 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 : A
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (0 * x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) =
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A) *
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
simp only [zero_mul, decompose_zero, zero_apply, ZeroMemClass.coe_zero]

Premises used: MulZeroClass.zero_mul, 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * y) :
                ⨁ (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)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_

Premises used: DirectSum.Decomposition.inductionOn
-- 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
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * 0) :
              ⨁ (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)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero]

Premises used: MulZeroClass.mul_zero, 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
refine_2 :
  (↑((((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)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) *
                  (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) c' hc') : A)) :
              ⨁ (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)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) c' hc') : A) :
                ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            0) :
        A)

Tactic:
simp only
-- 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
pos :
  ∀ (h : i + j = 0),
    (↑((((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)
neg :
  ∀ (h : ¬i + j = 0),
    (↑((((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)
⊢ (↑((((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:
by_cases h : i + j = 0