awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
refine :
  DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
    (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)
⊢ DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
    ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)

Tactic:
refine (assoc R _ _ _).symm.toLinearMap ∘ₗ .lTensor _ ?_ ∘ₗ (assoc R _ _ _).toLinearMap

Premises used: LinearEquiv.symm, LinearEquiv.toLinearMap, TensorProduct.assoc
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
refine : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
⊢ DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
    (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)

Tactic:
refine (assoc R _ _ _).toLinearMap ∘ₗ .rTensor _ ?_ ∘ₗ (assoc R _ _ _).symm.toLinearMap

Premises used: LinearEquiv.symm, LinearEquiv.toLinearMap, TensorProduct.assoc
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
⊢ DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i

Tactic:
exact (gradedComm _ _ _).toLinearMap

Premises used: LinearEquiv.toLinearMap, TensorProduct.gradedComm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ HSMul.hSMul (α := R) (β := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (i₂ * j₁)) : ℤ) : R)
      (((map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)) :
              ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R]
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
            (a : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) →
              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
          ((LinearEquiv.symm
                (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)) :
              (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))) →
                ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))
            (a₁ ⊗ₜ[R]
              (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i) :
                  (a : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i) →
                    (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i))
                ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ ⊗ₜ[R]
                    (lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ ⊗ₜ[R]
                  b₂))) :
        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) =
    HSMul.hSMul (α := R) (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (i₂ * j₁)) : ℤ) : R)
      (HMul.hMul (β := ⨁ (i : ι), 𝒜 i) a₁ ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), ℬ i) ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i) b₂)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
this :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((gradedMul R 𝒜 ℬ :
          (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
⊢ (((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      x =
    r • x

Tactic:
DFunLike.congr_fun this x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
this :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((gradedMul R 𝒜 ℬ :
          (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
⊢ (((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      x =
    r • x

Tactic:
exact DFunLike.congr_fun this x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
suffices :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((gradedMul R 𝒜 ℬ :
          (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
⊢ (((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      x =
    r • x

Tactic:
suffices gradedMul R 𝒜 ℬ (algebraMap R _ r ⊗ₜ 1) = DistribSMul.toLinearMap R _ r by
    exact DFunLike.congr_fun this x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
a :
  ∀ (ia : ι) (a : 𝒜 ia) (ib : ι) (b : ℬ ib),
    Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      (((((AlgebraTensorModule.curry
                          ((gradedMul R 𝒜 ℬ :
                              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                            ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1)) ∘ₗ
                        lof R ι 𝒜 ia :
                      𝒜 ia →ₗ[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                    (a : 𝒜 ia) → DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                  a ∘ₗ
                lof R ι ℬ ib :
              ℬ ib →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
            (a : ℬ ib) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
          b :
        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      (((((AlgebraTensorModule.curry (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r) ∘ₗ lof R ι 𝒜 ia :
                      𝒜 ia →ₗ[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                    (a : 𝒜 ia) → DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                  a ∘ₗ
                lof R ι ℬ ib :
              ℬ ib →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
            (a : ℬ ib) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
          b :
        DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
⊢ Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((gradedMul R 𝒜 ℬ :
          (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)

Tactic:
ext ia a ib b
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
a₁ :
  HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (0 * ia))
      (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r : DirectSum ι 𝒜)
          ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) (GradedMonoid.GOne.one (A := ℬ)) : ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b : ⨁ (i : ι), ℬ i)) =
    HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r
      ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
        (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
⊢ (((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b) =
    HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r
      ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
        (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)

Tactic:
erw [tmul_of_gradedMul_of_tmul]

Premises used: TensorProduct.tmul_of_gradedMul_of_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
a₁ :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r : DirectSum ι 𝒜)
        ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) (GradedMonoid.GOne.one (A := ℬ)) : ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b : ⨁ (i : ι), ℬ i))
    (HSMul.hSMul (β := ⨁ (i : ι), 𝒜 i) r ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b)
⊢ HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (0 * ia))
      (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r : DirectSum ι 𝒜)
          ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) (GradedMonoid.GOne.one (A := ℬ)) : ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b : ⨁ (i : ι), ℬ i)) =
    HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r
      ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
        (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)

Tactic:
rw [zero_mul, uzpow_zero, one_smul, smul_tmul']

Premises used: uzpow_zero, MulZeroClass.zero_mul, one_smul, TensorProduct.smul_tmul'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
a₁ :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r : DirectSum ι 𝒜)
          ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
      (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
    (HSMul.hSMul (β := ⨁ (i : ι), 𝒜 i) r ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
      (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
a₂ a₃ :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r : DirectSum ι 𝒜)
          ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
      (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((algebraMap R (⨁ (i : ι), 𝒜 i) : (a : R) → ⨁ (i : ι), 𝒜 i) r : ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b :
      (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
⊢ Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r : DirectSum ι 𝒜)
        ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) (GradedMonoid.GOne.one (A := ℬ)) : ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b : ⨁ (i : ι), ℬ i))
    (HSMul.hSMul (β := ⨁ (i : ι), 𝒜 i) r ((lof R ι 𝒜 ia : (a : 𝒜 ia) → ⨁ (i : ι), 𝒜 i) a : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      (lof R ι ℬ ib : (a : ℬ ib) → ⨁ (i : ι), ℬ i) b)

Tactic:
erw [one_mul, _root_.Algebra.smul_def]

Premises used: Algebra.smul_def, one_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
⊢ ((gradedMul R 𝒜 ℬ :
            (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
          1 :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      x =
    x

Tactic:
simpa only [RingHom.map_one, one_smul] using algebraMap_gradedMul 𝒜 ℬ 1 x

Premises used: RingHom.map_one, TensorProduct.algebraMap_gradedMul, one_smul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
this :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((LinearMap.flip (gradedMul R 𝒜 ℬ) :
          (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
⊢ (((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            x :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) =
    r • x

Tactic:
DFunLike.congr_fun this x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
this :
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    ((LinearMap.flip (gradedMul R 𝒜 ℬ) :
          (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
            DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
⊢ (((gradedMul R 𝒜 ℬ :
              (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            x :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) =
    r • x

Tactic:
exact DFunLike.congr_fun this x

Premises used: DFunLike.congr_fun