awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x : ℕ
ih : Eq (α := (a : A) → A) (⇑(f ^ x) : (a : A) → A) (⇑f : (a : A) → A)^[x]
x_1 : A
⊢ (f ^ x.succ : (a : A) → A) x_1 = (⇑f : (a : A) → A)^[x.succ] x_1

Tactic:
simp [pow_succ, ih]

Premises used: pow_succ
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
C : Type u_8
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : DecidableEq ι
inst_8 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
inst_9 : GradedAlgebra 𝒜
inst_10 : GradedAlgebra ℬ
inst_11 : GradedAlgebra 𝒞
g₁ g₂ : ℬ →ₐᵍ[R] 𝒞
f : 𝒜 →ₐᵍ[R] ℬ
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h ↦ coe_algHom_injective <| (AlgHom.cancel_right hf).1 congr($h), fun h ↦ h ▸ rfl⟩

Premises used: congrArg, GradedAlgHom.coe_algHom_injective, GradedAlgHom.toAlgHom, Eq.rec, AlgHom.cancel_right, id, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
C : Type u_8
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : DecidableEq ι
inst_8 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
inst_9 : GradedAlgebra 𝒜
inst_10 : GradedAlgebra ℬ
inst_11 : GradedAlgebra 𝒞
g₁ g₂ : 𝒜 →ₐᵍ[R] ℬ
f : ℬ →ₐᵍ[R] 𝒞
hf : Function.Injective.{u_7 + 1, u_8 + 1} (α := B) (β := C) (⇑f : (a : B) → C)
⊢ f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

Tactic:
⟨fun h ↦ coe_algHom_injective <| (AlgHom.cancel_left hf).1 congr($h), fun h ↦ h ▸ rfl⟩

Premises used: congrArg, GradedAlgHom.coe_algHom_injective, GradedAlgHom.toAlgHom, Eq.rec, id, AlgHom.cancel_left, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
V : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst_11 : GradedAlgebra 𝒜
inst_12 : GradedAlgebra ℬ
inst_13 : GradedAlgebra 𝒞
inst_14 : GradedAlgebra 𝒟
f : 𝒜 →ₐᵍ[R] ℬ
inst_15 : Subsingleton B
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ Membership.mem (α := B) (ℬ i) ((AlgHom.toRingHom.{u_1, u_6, u_7} (R := R) default : (a : A) → B) x : B)

Tactic:
aesop
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Subsingleton B
x : A
⊢ Eq.{u_7 + 1} (α := B) ((default : (a : A) → B) x : B) (0 : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
R₀ : Type u_11
inst_9 : CommSemiring R₀
inst_10 : Algebra R₀ R
inst_11 : Algebra R₀ A
inst_12 : Algebra R₀ B
inst_13 : IsScalarTower R₀ R A
inst_14 : IsScalarTower R₀ R B
f : 𝒜 →ₐᵍ[R] ℬ
⊢ Eq (α := (a : A) → B)
    (⇑((↑R₀ :
            [inst_15 : CommSemiring R₀] →
              [inst_16 : Algebra R₀ R] →
                [inst_17 : Algebra R₀ A] →
                  [inst_18 : Algebra R₀ B] →
                    [inst_19 : IsScalarTower R₀ R A] →
                      [inst_20 : IsScalarTower R₀ R B] →
                        (f : 𝒜 →ₐᵍ[R] ℬ) →
                          (fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) ↦
                            Submodule.restrictScalars R₀ (ℬ x))
          f) :
      (a : A) → B)
    (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
R₀ : Type u_11
inst_9 : CommSemiring R₀
inst_10 : Algebra R₀ R
inst_11 : Algebra R₀ A
inst_12 : Algebra R₀ B
inst_13 : IsScalarTower R₀ R A
inst_14 : IsScalarTower R₀ R B
f : 𝒜 →ₐᵍ[R] ℬ
⊢ Eq (α := A →ₐ[R₀] B) (AlgHom.restrictScalars R₀ (↑f : A →ₐ[R] B))
    (↑((↑R₀ :
            [inst_15 : CommSemiring R₀] →
              [inst_16 : Algebra R₀ R] →
                [inst_17 : Algebra R₀ A] →
                  [inst_18 : Algebra R₀ B] →
                    [inst_19 : IsScalarTower R₀ R A] →
                      [inst_20 : IsScalarTower R₀ R B] →
                        (f : 𝒜 →ₐᵍ[R] ℬ) →
                          (fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) ↦
                            Submodule.restrictScalars R₀ (ℬ x))
          f) :
      A →ₐ[R₀] B)

Tactic:
rfl

Premises used: AlgHom.restrictScalars, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
R₀ : Type u_11
inst_9 : CommSemiring R₀
inst_10 : Algebra R₀ R
inst_11 : Algebra R₀ A
inst_12 : Algebra R₀ B
inst_13 : IsScalarTower R₀ R A
inst_14 : IsScalarTower R₀ R B
f : 𝒜 →ₐᵍ[R] ℬ
⊢ Eq (α := A →ₗ[R₀] B)
    ((↑R₀ :
        {S : Type u_1} →
          {M : Type u_6} →
            {M₂ : Type u_7} →
              [inst : Semiring R₀] →
                [inst_15 : Semiring S] →
                  [inst_16 : AddCommMonoid M] →
                    [inst_17 : AddCommMonoid M₂] →
                      [inst_18 : Module R₀ M] →
                        [inst_19 : Module R₀ M₂] →
                          [inst_20 : Module S M] →
                            [inst_21 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R₀ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R₀] M₂)
      (↑f : [inst_15 : FunLike (𝒜 →ₐᵍ[R] ℬ) A B] → [SemilinearMapClass (𝒜 →ₐᵍ[R] ℬ) (RingHom.id R) A B] → A →ₗ[R] B))
    (↑((↑R₀ :
            [inst_15 : CommSemiring R₀] →
              [inst_16 : Algebra R₀ R] →
                [inst_17 : Algebra R₀ A] →
                  [inst_18 : Algebra R₀ B] →
                    [inst_19 : IsScalarTower R₀ R A] →
                      [inst_20 : IsScalarTower R₀ R B] →
                        (f : 𝒜 →ₐᵍ[R] ℬ) →
                          (fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) ↦
                            Submodule.restrictScalars R₀ (ℬ x))
          f) :
      [inst_15 :
          FunLike
            ((fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) ↦
              Submodule.restrictScalars R₀ (ℬ x))
            A B] →
        [SemilinearMapClass
              ((fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) ↦
                Submodule.restrictScalars R₀ (ℬ x))
              (RingHom.id R₀) A B] →
          A →ₗ[R₀] B)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.AlgHom
Goal:
R : Type u_1
A : Type u_6
B : Type u_7
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq ι
inst_6 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
R₀ : Type u_11
inst_9 : CommSemiring R₀
inst_10 : Algebra R₀ R
inst_11 : Algebra R₀ A
inst_12 : Algebra R₀ B
inst_13 : IsScalarTower R₀ R A
inst_14 : IsScalarTower R₀ R B
⊢ Function.Injective (α := 𝒜 →ₐᵍ[R] ℬ) (β :=
    GradedAlgHom.{u_11, u_6, u_7, u_10} R₀ (A := A) (B := B) (fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x))
      fun (x : ι) ↦ Submodule.restrictScalars R₀ (ℬ x))
    (↑R₀ :
      [inst_15 : CommSemiring R₀] →
        [inst_16 : Algebra R₀ R] →
          [inst_17 : Algebra R₀ A] →
            [inst_18 : Algebra R₀ B] →
              [inst_19 : IsScalarTower R₀ R A] →
                [inst_20 : IsScalarTower R₀ R B] →
                  (f : 𝒜 →ₐᵍ[R] ℬ) →
                    (fun (x : ι) ↦ Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) ↦
                      Submodule.restrictScalars R₀ (ℬ x))

Tactic:
fun _ _ h ↦ coe_fn_injective congr($h)

Premises used: congrArg, id, Function.Injective, DFunLike.coe, GradedAlgHom.coe_fn_injective
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
⊢ Eq (α := ⨁ (i : ι), ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1) 1

Tactic:
map_one (decomposeRingEquiv 𝒜)

Premises used: DirectSum.decomposeRingEquiv, map_one
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
⊢ Eq.{u_3 + 1} (α := A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) 1 : A) (1 : A)

Tactic:
map_one (decomposeRingEquiv 𝒜).symm

Premises used: DirectSum.decomposeRingEquiv, map_one, RingEquiv.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x y : A
⊢ (decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x * y) =
    HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
      ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i))
      ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i))

Tactic:
map_mul (decomposeRingEquiv 𝒜) x y

Premises used: DirectSum.decomposeRingEquiv, map_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x y : ⨁ (i : ι), ↥(𝒜 i)
⊢ (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) (x * y) =
    HMul.hMul (α := A) (β := A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) x : A)
      ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) y : A)

Tactic:
map_mul (decomposeRingEquiv 𝒜).symm x y

Premises used: DirectSum.decomposeRingEquiv, map_mul, RingEquiv.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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 [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, DirectSum.decompose_symm_of, GradedRing.proj_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : (i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0)
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 ZeroMemClass.coe_eq_zero.not.symm

Premises used: ZeroMemClass.coe_eq_zero, Iff.not, DFinsupp.mem_support_iff, Iff.trans, Iff.symm
-- 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 j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
⊢ a ∈ 𝒜 i

Tactic:
a_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 j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
lift :
  ∀ (a : ↥(𝒜 i)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
        A) =
      (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) : A) =
    a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : 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 : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
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))
          (i + 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)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + 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)) (i + 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_add]

Premises used: DirectSum.coe_of_mul_apply_add, 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 j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ b ∈ 𝒜 j

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 j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
lift :
  ∀ (b : ↥(𝒜 j)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
        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 + j)) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * b

Tactic:
lift b to 𝒜 j using 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 j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
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 + j)) :
      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)) j : ↥(𝒜 j) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 j)) → ⨁ (i : ι), ↥(𝒜 i))
                  b :
                ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      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 + j)) :
      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_add]

Premises used: DirectSum.coe_mul_of_apply_add, 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 j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
a : ↥(𝒜 i)
b : A
⊢ Eq (α := ↥(𝒜 (i + j)))
    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j))
    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _ a
      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j))

Tactic:
Subtype.ext <| coe_decompose_mul_add_of_left_mem 𝒜 a.2

Premises used: DirectSum.coe_decompose_mul_add_of_left_mem, Subtype.property, Subtype.ext
-- 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 j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ Eq (α := ↥(𝒜 (i + j)))
    ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j))
    (@GradedMonoid.GMul.mul _ (fun (i : ι) ↦ ↥(𝒜 i)) AddSemigroup.toAdd _ _ _
      ((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) b)

Tactic:
Subtype.ext <| coe_decompose_mul_add_of_right_mem 𝒜 b.2

Premises used: DirectSum.coe_decompose_mul_add_of_right_mem, Subtype.property, Subtype.ext
-- 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 𝒜
a b : A
a_mem : a ∈ 𝒜 0
⊢ a ∈ 𝒜 0

Tactic:
a_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
𝒜 : ι → σ
j : ι
inst_4 : AddMonoid ι
inst_5 : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 0
lift :
  ∀ (a : ↥(𝒜 0)),
    (↑((((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)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
    a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)

Tactic:
lift a to 𝒜 0 using a_mem

Premises used: OfNat.ofNat