awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
h : a₁ = a₁ * 1
h₁ h₂ : a₁ = a₁
⊢ a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)

Tactic:
rw [SetLike.coe_gOne, mul_one]

Premises used: SetLike.coe_gOne, mul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ)
      (a₁ ᵍ⊗ₜ[R] (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
      ((↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A) ᵍ⊗ₜ[R] b₂) =
    (a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)) ᵍ⊗ₜ[R]
      ((↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂)

Tactic:
tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ (GradedMonoid.GOne.one (A := (ℬ ·)))
      (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂

Premises used: GradedMonoid.GOne.one, GradedTensorProduct.tmul_coe_mul_zero_coe_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
h : a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
h₁ : b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] b₂) = a₁ ᵍ⊗ₜ[R] b₂

Tactic:
convert!
    tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ (GradedMonoid.GOne.one (A := (ℬ ·)))
      (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂

Premises used: GradedMonoid.GOne.one, GradedTensorProduct.tmul_coe_mul_zero_coe_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
h : a₁ = a₁ * 1
h₁ h₂ : a₁ = a₁
⊢ a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)

Tactic:
rw [SetLike.coe_gOne, mul_one]

Premises used: SetLike.coe_gOne, mul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
h : b₂ = 1 * b₂
h₁ h₂ : b₂ = b₂
⊢ b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂

Tactic:
rw [SetLike.coe_gOne, one_mul]

Premises used: SetLike.coe_gOne, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
rw :
  (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)
⊢ (a₁ * a₂) ᵍ⊗ₜ[R] 1 = HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) (a₂ ᵍ⊗ₜ[R] 1)

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 a₂, Finset.mul_sum]

Premises used: Finset.mul_sum, DirectSum.sum_support_decompose
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
simp_rw :
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
              1) :
          𝒜 ᵍ⊗[R] ℬ))
⊢ (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
        a₁ *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
      1 =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1)
      ((∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ᵍ⊗ₜ[R]
        1)

Tactic:
simp_rw [tmul, sum_tmul, map_sum, Finset.mul_sum]

Premises used: Finset.mul_sum, GradedTensorProduct.tmul, map_sum, TensorProduct.sum_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
e_f :
  Eq (α := ι → 𝒜 ᵍ⊗[R] ℬ)
    (fun (x : ι) ↦
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    fun (i : ι) ↦
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂),
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
              1) :
          𝒜 ᵍ⊗[R] ℬ))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
a₁ a₂ : A
e_f :
  ∀ (i : ι),
    (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)) ⊗ₜ[R]
          1) =
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
            ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
              1) :
          𝒜 ᵍ⊗[R] ℬ)
⊢ Eq (α := ι → 𝒜 ᵍ⊗[R] ℬ)
    (fun (x : ι) ↦
      (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
        ((a₁ *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) x) : A)) ⊗ₜ[R]
          1))
    fun (i : ι) ↦
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (a₁ ⊗ₜ[R] 1) : 𝒜 ᵍ⊗[R] ℬ)
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₂ : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ⊗ₜ[R]
            1) :
        𝒜 ᵍ⊗[R] ℬ)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ) (0 ᵍ⊗ₜ[R] 1) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
⊢ ∀ (x y : A), (x + y) ᵍ⊗ₜ[R] 1 = HAdd.hAdd (α := 𝒜 ᵍ⊗[R] ℬ) (x ᵍ⊗ₜ[R] 1) (y ᵍ⊗ₜ[R] 1)

Tactic:
simp [tmul, TensorProduct.add_tmul]

Premises used: GradedTensorProduct.tmul, TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
dsimp :
  Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
        ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                  (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                    ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
                  (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) :
              ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
            (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) :
      𝒜 ᵍ⊗[R] ℬ)
    ((LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
        ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                  (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                    ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
                ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
              ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
            (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
          ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
            (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1)) :
      𝒜 ᵍ⊗[R] ℬ)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ)
      ((RingHom.comp (includeLeftRingHom 𝒜 ℬ) (algebraMap R A) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ) x =
    HMul.hMul (β := 𝒜 ᵍ⊗[R] ℬ) x
      ((RingHom.comp (includeLeftRingHom 𝒜 ℬ) (algebraMap R A) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ)

Tactic:
dsimp [mul_def, mulHom_apply, auxEquiv_tmul]

Premises used: GradedTensorProduct.mul_def, GradedTensorProduct.mulHom_apply, GradedTensorProduct.auxEquiv_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
dsimp :
  r • x =
    (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
                (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x))
⊢ r • x =
    HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ)
      ((RingHom.comp (includeLeftRingHom 𝒜 ℬ) (algebraMap R A) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ) x

Tactic:
dsimp [mul_def, mulHom_apply, auxEquiv_tmul]

Premises used: GradedTensorProduct.mul_def, GradedTensorProduct.mulHom_apply, GradedTensorProduct.auxEquiv_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
simp_rw :
  r • x =
    (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (HSMul.hSMul (β := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) r
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x :
          (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)))
⊢ r • x =
    (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((((gradedMul R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
                (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →
                  ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((algebraMap R A : (a : R) → A) r) ⊗ₜ[R]
                (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) :
            ((⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) →ₗ[R] (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x))

Tactic:
simp_rw [DirectSum.decompose_algebraMap, DirectSum.decompose_one, algebraMap_gradedMul]

Premises used: TensorProduct.algebraMap_gradedMul, DirectSum.decompose_algebraMap, DirectSum.decompose_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
rw :
  r • x =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) r
      ((LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
        𝒜 ᵍ⊗[R] ℬ)
⊢ r • x =
    (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      (HSMul.hSMul (β := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) r
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x :
          (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)))

Tactic:
rw [LinearEquiv.map_smul]

Premises used: LinearEquiv.map_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) r
      ((LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
        𝒜 ᵍ⊗[R] ℬ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
r : R
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ) ((algebraMap R (𝒜 ᵍ⊗[R] ℬ) : (a : R) → 𝒜 ᵍ⊗[R] ℬ) r : 𝒜 ᵍ⊗[R] ℬ)
    ((algebraMap R A : (a : R) → A) r ᵍ⊗ₜ[R] 1 : 𝒜 ᵍ⊗[R] ℬ)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
i₂ : ι
a₁ : A
r : R
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (algebraMap R B : (a : R) → B) r : 𝒜 ᵍ⊗[R] ℬ)
      ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b₂

Tactic:
tmul_zero_coe_mul_coe_tmul 𝒜 ℬ a₁ (GAlgebra.toFun (A := (ℬ ·)) r) a₂ b₂

Premises used: GradedTensorProduct.tmul_zero_coe_mul_coe_tmul, DirectSum.GAlgebra.toFun, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
r : R
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B))
      ((algebraMap R A : (a : R) → A) r ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) =
    HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) r : A) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)

Tactic:
tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ b₁ (GAlgebra.toFun (A := (𝒜 ·)) r) b₂

Premises used: GradedTensorProduct.tmul_coe_mul_zero_coe_tmul, DirectSum.GAlgebra.toFun, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
⊢ ∀ (x y : B), 1 ᵍ⊗ₜ[R] (x + y) = HAdd.hAdd (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] x) (1 ᵍ⊗ₜ[R] y)

Tactic:
simp [tmul, TensorProduct.tmul_add]

Premises used: GradedTensorProduct.tmul, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
⊢ ∀ (m : R) (x : B),
    1 ᵍ⊗ₜ[R] (m • x) = HSMul.hSMul (α := R) (β := 𝒜 ᵍ⊗[R] ℬ) ((RingHom.id R : (a : R) → R) m : R) (1 ᵍ⊗ₜ[R] x)

Tactic:
simp [tmul, TensorProduct.tmul_smul]

Premises used: TensorProduct.tmul_smul, GradedTensorProduct.tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
rw :
  Eq (α := B →ₗ[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)
    (LinearMap.compr₂ (LinearMap.mul R B) { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ })
    (LinearMap.compl₂ (σ₄₂ := RingHom.id R)
      (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ
        { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ })
      { toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ })
⊢ ∀ (x y : B),
    ({ toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } : (a : B) → 𝒜 ᵍ⊗[R] ℬ) (x * y) =
      HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (β := 𝒜 ᵍ⊗[R] ℬ)
        (({ toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } :
              (a : B) → 𝒜 ᵍ⊗[R] ℬ)
            x :
          𝒜 ᵍ⊗[R] ℬ)
        (({ toFun := fun (b : B) ↦ 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ : B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ } :
              (a : B) → 𝒜 ᵍ⊗[R] ℬ)
            y :
          𝒜 ᵍ⊗[R] ℬ)

Tactic:
rw [LinearMap.map_mul_iff]

Premises used: LinearMap.map_mul_iff