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)
a : ⨁ (i : ι), 𝒜 i
b : ℬ 0
R₁ :
  Eq (α := (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
      (LinearMap.flip (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) :
          (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b))
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i) :
        (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b))
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        (a ⊗ₜ[R] (lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] a : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
suffices
    (gradedComm R 𝒜 ℬ).toLinearMap ∘ₗ
        (TensorProduct.mk R (⨁ i, 𝒜 i) (⨁ i, ℬ i)).flip (lof R _ ℬ 0 b) =
      TensorProduct.mk R _ _ (lof R _ ℬ 0 b) from
    DFunLike.congr_fun this a
-- 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)
a : ⨁ (i : ι), 𝒜 i
b : ℬ 0
H :
  ∀ (i : ι) (a : 𝒜 i),
    Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      (((((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
                  (LinearMap.flip (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) :
                      (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
                    ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b)) ∘ₗ
                lof R ι 𝒜 i :
              𝒜 i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
            (a : 𝒜 i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
          a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i) :
                    (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                  ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b) ∘ₗ
                lof R ι 𝒜 i :
              𝒜 i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
            (a : 𝒜 i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
          a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
⊢ Eq (α := (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
      (LinearMap.flip (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) :
          (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b))
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i) :
        (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b))

Tactic:
ext i a
-- 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)
a_1 : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
H :
  Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (((((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
                (LinearMap.flip (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)) :
                    (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
                  ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b)) ∘ₗ
              lof R ι 𝒜 i :
            𝒜 i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
          (a : 𝒜 i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i) :
                  (a : ⨁ (i : ι), ℬ i) → (⨁ (i : ι), 𝒜 i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b) ∘ₗ
              lof R ι 𝒜 i :
            𝒜 i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
          (a : 𝒜 i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

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)
a_1 : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
H :
  HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow (α := ℤˣ) (-1) (0 * i))
      ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    (lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a
H₁ :
  HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    (lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a
H₂ :
  HSMul.hSMul (α := ℤˣ) (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) 1
      ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    (lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a
H₃ H₄ :
  Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ 0 : (a : ℬ 0) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

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

Premises used: uzpow_zero, MulZeroClass.zero_mul, one_smul, TensorProduct.gradedComm_of_tmul_of
-- 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)
a : 𝒜 0
b : ⨁ (i : ι), ℬ i
R₁ :
  Eq (α := (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
      (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) :
          (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a))
    ((LinearMap.flip (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) :
        (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a))
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
suffices
    (gradedComm R 𝒜 ℬ).toLinearMap ∘ₗ (TensorProduct.mk R (⨁ i, 𝒜 i) (⨁ i, ℬ i)) (lof R _ 𝒜 0 a) =
      (TensorProduct.mk R _ _).flip (lof R _ 𝒜 0 a) from
    DFunLike.congr_fun this 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)
a : 𝒜 0
b : ⨁ (i : ι), ℬ i
H :
  ∀ (i : ι) (b : ℬ i),
    Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      (((((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
                  (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) :
                      (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
                    ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a)) ∘ₗ
                lof R ι ℬ i :
              ℬ i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
            (a : ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
          b :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((((LinearMap.flip (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) :
                    (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                  ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a) ∘ₗ
                lof R ι ℬ i :
              ℬ i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
            (a : ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
          b :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
⊢ Eq (α := (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
      (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) :
          (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a))
    ((LinearMap.flip (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) :
        (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a))

Tactic:
ext i 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)
a : 𝒜 0
b_1 : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
H :
  Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (((((↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ∘ₗ
                (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) :
                    (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
                  ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a)) ∘ₗ
              lof R ι ℬ i :
            ℬ i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
          (a : ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        b :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((((LinearMap.flip (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) :
                  (a : ⨁ (i : ι), 𝒜 i) → (⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a) ∘ₗ
              lof R ι ℬ i :
            ℬ i →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) :
          (a : ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        b :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

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)
a : 𝒜 0
b_1 : ⨁ (i : ι), ℬ i
i : ι
b : ℬ i
H :
  HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow (α := ℤˣ) (-1) (i * 0))
      ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    (lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a
H₁ :
  HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow.{0, u_2, 0} (α := ℤˣ) (β := ι) (-1) 0)
      ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    (lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a
H₂ :
  HSMul.hSMul (α := ℤˣ) (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) 1
      ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) =
    (lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a
H₃ H₄ :
  Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((lof R ι ℬ i : (a : ℬ i) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

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

Premises used: uzpow_zero, one_smul, MulZeroClass.mul_zero, TensorProduct.gradedComm_of_tmul_of
-- 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 : GradedMonoid.GOne ℬ
a : ⨁ (i : ι), 𝒜 i
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        (a ⊗ₜ[R] 1) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (1 ⊗ₜ[R] a : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
gradedComm_tmul_of_zero _ _ _ _ _

Premises used: TensorProduct.gradedComm_tmul_of_zero
-- 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 : GradedMonoid.GOne 𝒜
b : ⨁ (i : ι), ℬ i
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        (1 ⊗ₜ[R] b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (b ⊗ₜ[R] 1 : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
gradedComm_of_zero_tmul _ _ _ _ _

Premises used: TensorProduct.gradedComm_of_zero_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.GSemiring 𝒜
inst_9 : DirectSum.GSemiring ℬ
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) 1) 1

Tactic:
gradedComm_one_tmul _ _ _ _

Premises used: TensorProduct.gradedComm_one_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.GSemiring ℬ
inst_9 : DirectSum.GAlgebra R ℬ
a : ⨁ (i : ι), 𝒜 i
r : R
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        (a ⊗ₜ[R] (algebraMap R (⨁ (i : ι), ℬ i) : (a : R) → ⨁ (i : ι), ℬ i) r) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((algebraMap R (⨁ (i : ι), ℬ i) : (a : R) → ⨁ (i : ι), ℬ i) r ⊗ₜ[R] a : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
gradedComm_tmul_of_zero _ _ _ _ _

Premises used: DFinsupp.single, TensorProduct.gradedComm_tmul_of_zero
-- 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.GSemiring 𝒜
inst_9 : DirectSum.GAlgebra R 𝒜
r : R
b : ⨁ (i : ι), ℬ i
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((algebraMap R (⨁ (i : ι), 𝒜 i) : (a : R) → ⨁ (i : ι), 𝒜 i) r ⊗ₜ[R] b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (b ⊗ₜ[R] (algebraMap R (⨁ (i : ι), 𝒜 i) : (a : R) → ⨁ (i : ι), 𝒜 i) r : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
gradedComm_of_zero_tmul _ _ _ _ _

Premises used: DFinsupp.single, TensorProduct.gradedComm_of_zero_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.GSemiring 𝒜
inst_9 : DirectSum.GSemiring ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
r : R
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((algebraMap R ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) : (a : R) → (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((algebraMap R ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) : (a : R) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) r :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)

Tactic:
(gradedComm_algebraMap_tmul R 𝒜 ℬ r 1).trans (Algebra.TensorProduct.algebraMap_apply' r).symm

Premises used: TensorProduct.gradedComm_algebraMap_tmul, Algebra.TensorProduct.algebraMap_apply', TensorProduct.tmul, OfNat.ofNat, Eq.symm, AddCon.toQuotient, Eq.trans
-- 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] DirectSum ι ℬ) →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ

Tactic:
refine TensorProduct.curry ?_

Premises used: TensorProduct.curry
-- 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] DirectSum ι ℬ) →ₗ[R]
    ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)
⊢ DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ

Tactic:
refine map (LinearMap.mul' R (⨁ i, 𝒜 i)) (LinearMap.mul' R (⨁ i, ℬ i)) ∘ₗ ?_

Premises used: TensorProduct.map, LinearMap.mul', DirectSum