awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (DirectSum.toModule R (ι × ι) (M := fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2))
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) fun (i : ι × ι) ↦
          have o :
            TensorProduct.{u_1, u_4, u_3} R (ℬ (i.2, i.1).1) (𝒜 (i.2, i.1).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) :=
            lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (i.2, i.1);
          have s := HPow.hPow (α := ℤˣ) (-1) (i.1 * i.2);
          (s • o) ∘ₗ (↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)) : 𝒜 i.1 ⊗[R] ℬ i.2 →ₗ[R] ℬ i.2 ⊗[R] 𝒜 i.1) :
        (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
      (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) (i, j) :
            TensorProduct.{u_1, u_3, u_4} R (𝒜 (i, j).1) (ℬ (i, j).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
          (a : 𝒜 (i, j).1 ⊗[R] ℬ (i, j).2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
        (a ⊗ₜ[R] b)) =
    HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (j, i) :
              TensorProduct.{u_1, u_4, u_3} R (ℬ (j, i).1) (𝒜 (j, i).2) →ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
            (a : ℬ (j, i).1 ⊗[R] 𝒜 (j, i).2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
          (b ⊗ₜ[R] a) :
        ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
have simp : (HSMul.hSMul (β :=
        TensorProduct.{u_1, u_4, u_3} R (ℬ j) (𝒜 i) →ₗ[R]
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
        (HPow.hPow (α := ℤˣ) (-1) (j * i))
        (lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (j, i) :
          TensorProduct.{u_1, u_4, u_3} R (ℬ (j, i).1) (𝒜 (j, i).2) →ₗ[R]
            ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
      (a : ℬ j ⊗[R] 𝒜 i) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
    (b ⊗ₜ[R] a) =
  HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (HPow.hPow (α := ℤˣ) (-1) (j * i))
    (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) (j, i) :
            TensorProduct.{u_1, u_4, u_3} R (ℬ (j, i).1) (𝒜 (j, i).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
          (a : ℬ j ⊗[R] 𝒜 i) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
        (b ⊗ₜ[R] a) :
      ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2))
Tactic: simp [mul_comm i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i_1 : ι × ι
⊢ (((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            ((gradedCommAux R ℬ 𝒜 : (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
              (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                    TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                      ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
                  (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
                (a ⊗ₜ[R] b))) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1 =
    ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
                TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
              (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
            (a ⊗ₜ[R] b) :
          ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
        (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
      i_1
have H : (((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
          (HSMul.hSMul (β := ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2))
            (HPow.hPow (α := ℤˣ) (-1) (i.2 * i.1))
            (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) (i.2, i.1) :
                    TensorProduct.{u_1, u_3, u_4} R (𝒜 (i.2, i.1).1) (ℬ (i.2, i.1).2) →ₗ[R]
                      ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
                  (a : 𝒜 (i.2, i.1).1 ⊗[R] ℬ (i.2, i.1).2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
                (b ⊗ₜ[R] a) :
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2))) :
        ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
      (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
    i_1 =
  ((((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) i :
              TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2) →ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
            (a : ℬ i.1 ⊗[R] 𝒜 i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
          (a ⊗ₜ[R] b) :
        ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) :
      (a : ι × ι) → ℬ a.1 ⊗[R] 𝒜 a.2)
    i_1
Tactic: rw [gradedCommAux_lof_tmul, LinearMap.map_smul_of_tower, gradedCommAux_lof_tmul, smul_smul,
    mul_comm i.2 i.1, Int.units_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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)
⊢ ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ≃ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i
have refine : (⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) ≃ₗ[R]
  ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)
Tactic: refine TensorProduct.directSum R R 𝒜 ℬ ≪≫ₗ ?_ ≪≫ₗ (TensorProduct.directSum R R ℬ 𝒜).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
          (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
            (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
        (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      ((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
        (((TensorProduct.directSum R R 𝒜 ℬ :
              ((⨁ (i₁ : ι), 𝒜 i₁) ⊗[R] ⨁ (i₂ : ι), ℬ i₂) ≃ₗ[R]
                ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
            (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
          ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j : (a : ℬ j) → ⨁ (i : ι), ℬ i) b))) =
    HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((lof R ι ℬ j : (a : ℬ j) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
        (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
have rw : ((LinearEquiv.symm (TensorProduct.directSum R R ℬ 𝒜) :
        (⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)) ≃ₗ[R]
          (⨁ (i₁ : ι), ℬ i₁) ⊗[R] ⨁ (i₂ : ι), 𝒜 i₂) :
      (a : ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedCommAux R 𝒜 ℬ : (a : ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2) → ⨁ (i : ι × ι), ℬ i.1 ⊗[R] 𝒜 i.2)
      (((lof R (ι × ι) (fun (i : ι × ι) ↦ TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) (i, j) :
            TensorProduct.{u_1, u_3, u_4} R (𝒜 (i, j).1) (ℬ (i, j).2) →ₗ[R]
              ⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) :
          (a : 𝒜 (i, j).1 ⊗[R] ℬ (i, j).2) → ⨁ (i : ι × ι), 𝒜 i.1 ⊗[R] ℬ i.2)
        (a ⊗ₜ[R] b))) =
  HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) (HPow.hPow (α := ℤˣ) (-1) (j * i))
    ((lof R ι ℬ j : (a : ℬ j) → ⨁ (i : ι), ℬ i) b ⊗ₜ[R] (lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) a :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
Tactic: rw [TensorProduct.directSum_lof_tmul_lof, gradedCommAux_lof_tmul, Units.smul_def,
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 specialized `map_smul` to `LinearEquiv.map_smul` to avoid timeouts.
    ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, TensorProduct.directSum_symm_lof_tmul,
    Int.cast_smul_eq_zsmul, ← Units.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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)
have 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))
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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))
have 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)
Tactic: ext i a
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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)
have 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
Tactic: rw [gradedComm_of_tmul_of, zero_mul, uzpow_zero, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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)
have 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
Tactic: rw [gradedComm_of_tmul_of, zero_mul, uzpow_zero, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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)
have 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
Tactic: rw [gradedComm_of_tmul_of, zero_mul, uzpow_zero, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.External (goal)
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
⊢ 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)
have 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)
Tactic: rw [gradedComm_of_tmul_of, zero_mul, uzpow_zero, one_smul]