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 ℬ
rw :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) 1))
    1
rw₁ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
        ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (1 ⊗ₜ[R] 1)) :
      (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    (1 : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
rw₂ :
  Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
rw₃ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) 1) 1
rw₄ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] 1) 1
rw₅ rw₆ : Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] 1)
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1

Tactic:
rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]

Premises used: GradedTensorProduct.auxEquiv_tmul, DirectSum.decompose_one, GradedTensorProduct.of_one, Algebra.TensorProduct.one_def
-- 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 ℬ
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ) 1) 1

Tactic:
(LinearEquiv.symm_apply_eq _).mpr (auxEquiv_one _ _).symm

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, GradedTensorProduct.auxEquiv_one, Eq.symm
-- 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 ℤˣ)
fAB1 : 𝒜 ᵍ⊗[R] ℬ ≃ₗ[R] (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i) := auxEquiv R 𝒜 ℬ
have : (this : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ
⊢ 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ

Tactic:
have := ((gradedMul R (𝒜 ·) (ℬ ·)).compl₁₂ fAB1.toLinearMap fAB1.toLinearMap).compr₂
    fAB1.symm.toLinearMap
-- 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 ℤˣ)
fAB1 : 𝒜 ᵍ⊗[R] ℬ ≃ₗ[R] (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i) := auxEquiv R 𝒜 ℬ
this : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ
⊢ 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ

Tactic:
exact this
-- 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 : 𝒜 ᵍ⊗[R] ℬ
⊢ Eq (α := 𝒜 ᵍ⊗[R] ℬ)
    ((((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
          (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
        y :
      𝒜 ᵍ⊗[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))
          ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) y)) :
      𝒜 ᵍ⊗[R] ℬ)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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 ℤˣ)
x y : 𝒜 ᵍ⊗[R] ℬ
⊢ x * y =
    (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
      y

Tactic:
rfl

Premises used: 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 ℤˣ)
x y : 𝒜 ᵍ⊗[R] ℬ
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (x * y) :
      (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((((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))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) y) :
      (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))

Tactic:
LinearEquiv.eq_symm_apply _ |>.mp rfl

Premises used: LinearEquiv.eq_symm_apply, Iff.mp, 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 ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
rw : ((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) 1 : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ) x = x
rw₁ :
  (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)) 1) :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
rw₂ :
  (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))
            1 :
          (a : (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x)) → (⨁ (x : ι), ↥(𝒜 x)) ⊗[R] ⨁ (x : ι), ↥(ℬ x))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) =
    x
rw₃ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) =
    x
rw₄ rw₅ : x = x
⊢ 1 * x = x

Tactic:
rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]

Premises used: GradedTensorProduct.auxEquiv_one, GradedTensorProduct.mul_def, LinearEquiv.symm_apply_apply, GradedTensorProduct.mulHom_apply, TensorProduct.one_gradedMul
-- 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 : 𝒜 ᵍ⊗[R] ℬ
rw :
  (((mulHom 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) x : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] 𝒜 ᵍ⊗[R] ℬ) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → 𝒜 ᵍ⊗[R] ℬ)
      1 =
    x
rw₁ :
  (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))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1)) =
    x
rw₂ :
  (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))
        1) =
    x
rw₃ :
  (LinearEquiv.symm (auxEquiv R 𝒜 ℬ) : (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → 𝒜 ᵍ⊗[R] ℬ)
      ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) =
    x
rw₄ rw₅ : x = x
⊢ x * 1 = x

Tactic:
rw [mul_def, mulHom_apply, auxEquiv_one, gradedMul_one, LinearEquiv.symm_apply_apply]

Premises used: GradedTensorProduct.auxEquiv_one, GradedTensorProduct.mul_def, LinearEquiv.symm_apply_apply, TensorProduct.gradedMul_one, GradedTensorProduct.mulHom_apply
-- 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₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
dsimp :
  (of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
      (((LinearEquiv.symm
              (TensorProduct.congr (↑(decomposeAlgEquiv 𝒜) : A ≃ₗ[R] ⨁ (i : ι), ↥(𝒜 i))
                (↑(decomposeAlgEquiv ℬ) : B ≃ₗ[R] ⨁ (i : ι), ↥(ℬ i))) :
            ((⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) ≃ₗ[R] A ⊗[R] B) :
          (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → A ⊗[R] B)
        ((((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)) a₁ ⊗ₜ[R]
                  (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) (↑b₁ : B)) :
              ((⨁ (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)) (↑a₂ : A) ⊗ₜ[R]
            (decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂))) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[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)) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B))) :
            ((⨁ (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)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂))) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))

Tactic:
dsimp [auxEquiv, tmul]

Premises used: GradedTensorProduct.tmul, GradedTensorProduct.auxEquiv
-- 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₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
dsimp :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
              (HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i))
                (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                    a₂ :
                  ⨁ (i : ι), ↥(𝒜 i))) ⊗ₜ[R]
            (Equiv.symm (decompose ℬ) : (a : ⨁ (i : ι), ↥(ℬ i)) → B)
              (HMul.hMul (α := ⨁ (i : ι), ↥(ℬ i)) (β := ⨁ (i : ι), ↥(ℬ i))
                (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                      (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                    b₁ :
                  ⨁ (i : ι), ↥(ℬ i))
                ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)))) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)
⊢ HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ)
          (((LinearEquiv.symm (↑(decomposeAlgEquiv 𝒜) : A ≃ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) : (⨁ (i : ι), ↥(𝒜 i)) ≃ₗ[R] A) :
                (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
              (HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
                ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a₁ : ⨁ (i : ι), ↥(𝒜 i))
                (((DirectSum.of.{u_2, u_3} (fun (x : ι) ↦ ↥(𝒜 x)) i₂ : ↥(𝒜 i₂) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                      (a : ↥(𝒜 i₂)) → ⨁ (i : ι), ↥(𝒜 i))
                    a₂ :
                  ⨁ (i : ι), ↥(𝒜 i))) ⊗ₜ[R]
            ((LinearEquiv.symm (↑(decomposeAlgEquiv ℬ) : B ≃ₗ[R] ⨁ (i : ι), ↥(ℬ i)) : (⨁ (i : ι), ↥(ℬ i)) ≃ₗ[R] B) :
                (a : ⨁ (i : ι), ↥(ℬ i)) → B)
              (HMul.hMul (α := ⨁ (i : ι), ↥(ℬ i)) (β := ⨁ (i : ι), ↥(ℬ i))
                (((DirectSum.of.{u_2, u_4} (fun (x : ι) ↦ ↥(ℬ x)) j₁ : ↥(ℬ j₁) →+ ⨁ (i : ι), ↥(ℬ i)) :
                      (a : ↥(ℬ j₁)) → ⨁ (i : ι), ↥(ℬ i))
                    b₁ :
                  ⨁ (i : ι), ↥(ℬ i))
                ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) b₂ : ⨁ (i : ι), ↥(ℬ i)))) :
        𝒜 ᵍ⊗[R] ℬ) =
    HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂))
      ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ⊗ₜ[R] ((↑b₁ : B) * b₂)) : 𝒜 ᵍ⊗[R] ℬ)

Tactic:
dsimp
-- 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
b₁ : ↥(ℬ 0)
a₂ : ↥(𝒜 i₂)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (0 * i₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₂ :
  HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1 ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₃ rw₄ : Eq (α := 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)

Tactic:
rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul]

Premises used: uzpow_zero, GradedTensorProduct.tmul_coe_mul_coe_tmul, MulZeroClass.zero_mul, one_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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
rw :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j₁ * 0)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₁ :
  HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₂ :
  HSMul.hSMul (α := ℤˣ) (β := 𝒜 ᵍ⊗[R] ℬ) 1 ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)
rw₃ rw₄ : Eq (α := 𝒜 ᵍ⊗[R] ℬ) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)) ((a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂))
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)

Tactic:
rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, one_smul]

Premises used: uzpow_zero, GradedTensorProduct.tmul_coe_mul_coe_tmul, one_smul, MulZeroClass.mul_zero
-- 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
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ)
      (a₁ ᵍ⊗ₜ[R] (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B))
      ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) =
    (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R]
      ((↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂)

Tactic:
tmul_zero_coe_mul_coe_tmul 𝒜 ℬ a₁ (@GradedMonoid.GOne.one _ (ℬ ·) _ _) a₂ b₂

Premises used: GradedTensorProduct.tmul_zero_coe_mul_coe_tmul, GradedMonoid.GOne.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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
h : b₂ = (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(ℬ x)) MulZeroClass.toZero _ : ↥(ℬ 0)) : B) * b₂
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] 1) ((↑a₂ : A) ᵍ⊗ₜ[R] b₂) = (a₁ * (↑a₂ : A)) ᵍ⊗ₜ[R] b₂

Tactic:
convert! tmul_zero_coe_mul_coe_tmul 𝒜 ℬ a₁ (@GradedMonoid.GOne.one _ (ℬ ·) _ _) a₂ b₂

Premises used: GradedTensorProduct.tmul_zero_coe_mul_coe_tmul, GradedMonoid.GOne.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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : 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]
      ((↑b₁ : B) * b₂)

Tactic:
tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ b₁ (@GradedMonoid.GOne.one _ (𝒜 ·) _ _) 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 ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
h : a₁ = a₁ * (↑(@GradedMonoid.GOne.one _ (fun (x : ι) ↦ ↥(𝒜 x)) MulZeroClass.toZero _ : ↥(𝒜 0)) : A)
⊢ HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (a₁ ᵍ⊗ₜ[R] (↑b₁ : B)) (1 ᵍ⊗ₜ[R] b₂) = a₁ ᵍ⊗ₜ[R] ((↑b₁ : B) * b₂)

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

Premises used: GradedMonoid.GOne.one, GradedTensorProduct.tmul_coe_mul_zero_coe_tmul