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)
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
⊢ 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)
have 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)
Tactic: rw [zero_mul, uzpow_zero, one_smul, smul_tmul']
-- 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)
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
⊢ 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)
have 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)
Tactic: erw [one_mul, _root_.Algebra.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)
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)
⊢ 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)
have 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)
Tactic: erw [one_mul, _root_.Algebra.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)
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
⊢ (((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
have suffices : 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 ι ℬ)
Tactic: suffices (gradedMul R 𝒜 ℬ).flip (algebraMap R _ r ⊗ₜ 1) = DistribSMul.toLinearMap R _ r by
    exact DFunLike.congr_fun this x
-- 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)
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
⊢ 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 ι ℬ)
have a : ∀ (i : ι) (x : 𝒜 i) (i_1 : ι) (x_1 : ℬ i_1),
  Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (((((AlgebraTensorModule.curry
                        ((LinearMap.flip (gradedMul R 𝒜 ℬ) :
                            (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →
                              DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                          ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1)) ∘ₗ
                      lof R ι 𝒜 i :
                    𝒜 i →ₗ[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                  (a : 𝒜 i) → DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                x ∘ₗ
              lof R ι ℬ i_1 :
            ℬ i_1 →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
          (a : ℬ i_1) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        x_1 :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
    (((((AlgebraTensorModule.curry (DistribSMul.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r) ∘ₗ lof R ι 𝒜 i :
                    𝒜 i →ₗ[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
                  (a : 𝒜 i) → DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
                x ∘ₗ
              lof R ι ℬ i_1 :
            ℬ i_1 →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
          (a : ℬ i_1) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
        x_1 :
      DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
Tactic: ext
-- 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)
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
i : ι
x_1 : 𝒜 i
i_1 : ι
x_2 : ℬ i_1
⊢ (((gradedMul R 𝒜 ℬ :
              (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →
                DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
            ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 ⊗ₜ[R] (lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2) :
          DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) :
        (a : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) → DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
      ((algebraMap R (DirectSum ι 𝒜) : (a : R) → DirectSum ι 𝒜) r ⊗ₜ[R] 1) =
    HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r
      ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 ⊗ₜ[R] (lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 :
        (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
have a : HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (i_1 * 0))
    (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 : ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i)
            (((@DirectSum.GAlgebra.toFun.{u_2, u_1, u_3} _ R 𝒜 CommRing.toCommSemiring
                    (fun (i : ι) ↦ AddCommGroup.toAddCommMonoid) inst_6 AddMonoidWithOne.toAddMonoid
                    (DirectSum.GRing.toGSemiring (A := 𝒜)) _ :
                  AddMonoidHom.{u_1, u_3} R (𝒜 0)) :
                (a : R) → 𝒜 0)
              r) :
          ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 : ⨁ (i : ι), ℬ i) (1 : DirectSum ι ℬ)) =
  HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r
    ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 ⊗ₜ[R] (lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 :
      (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
Tactic: erw [tmul_of_gradedMul_of_tmul]
-- 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)
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
i : ι
x_1 : 𝒜 i
i_1 : ι
x_2 : ℬ i_1
⊢ HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) (HPow.hPow (α := ℤˣ) (-1) (i_1 * 0))
      (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 : ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i)
              (((@DirectSum.GAlgebra.toFun.{u_2, u_1, u_3} _ R 𝒜 CommRing.toCommSemiring
                      (fun (i : ι) ↦ AddCommGroup.toAddCommMonoid) inst_6 AddMonoidWithOne.toAddMonoid
                      (DirectSum.GRing.toGSemiring (A := 𝒜)) _ :
                    AddMonoidHom.{u_1, u_3} R (𝒜 0)) :
                  (a : R) → 𝒜 0)
                r) :
            ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 : ⨁ (i : ι), ℬ i) (1 : DirectSum ι ℬ)) =
    HSMul.hSMul (β := (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) r
      ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 ⊗ₜ[R] (lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 :
        (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
have a : Eq (α := DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)
  (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 : ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i)
            (((@DirectSum.GAlgebra.toFun.{u_2, u_1, u_3} _ R 𝒜 CommRing.toCommSemiring
                    (fun (i : ι) ↦ AddCommGroup.toAddCommMonoid) inst_6 AddMonoidWithOne.toAddMonoid
                    (DirectSum.GRing.toGSemiring (A := 𝒜)) _ :
                  AddMonoidHom.{u_1, u_3} R (𝒜 0)) :
                (a : R) → 𝒜 0)
              r) :
          ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      (lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 :
    (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
  (HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i : (a : 𝒜 i) → ⨁ (i : ι), 𝒜 i) x_1 : ⨁ (i : ι), 𝒜 i)
        ((algebraMap R (⨁ (i : ι), 𝒜 i) : (a : R) → ⨁ (i : ι), 𝒜 i) r : ⨁ (i : ι), 𝒜 i) ⊗ₜ[R]
      (lof R ι ℬ i_1 : (a : ℬ i_1) → ⨁ (i : ι), ℬ i) x_2 :
    (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
Tactic: rw [mul_zero, uzpow_zero, one_smul, smul_tmul',
      mul_one, _root_.Algebra.smul_def, Algebra.commutes]
-- 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)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ Eq (α := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
        ((((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 ι ℬ)
          y) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    ((((gradedMul R ℬ 𝒜 :
                (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) →
                  DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
              ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
                x) :
            DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) :
          (a : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) → DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
        ((gradedComm R 𝒜 ℬ : (a : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) → (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) y) :
      DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
have suffices : Eq (α :=
  DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
  (LinearMap.compr₂ (gradedMul R 𝒜 ℬ)
    (↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i))
  (LinearMap.compl₂
    (gradedMul R ℬ 𝒜 ∘ₗ
      (↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i))
    (↑(gradedComm R 𝒜 ℬ) : ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) →ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i))
Tactic: suffices (gradedMul R 𝒜 ℬ).compr₂ (gradedComm R 𝒜 ℬ).toLinearMap
      = (gradedMul R ℬ 𝒜 ∘ₗ (gradedComm R 𝒜 ℬ).toLinearMap).compl₂
        (gradedComm R 𝒜 ℬ).toLinearMap from
    LinearMap.congr_fun₂ this x y
-- 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)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
      (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂) * HPow.hPow (α := ℤˣ) (-1) ((j₁ + j₂) * (i₁ + i₂)))
      (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂ : ⨁ (i : ι), ℬ i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ : ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i)) =
    HSMul.hSMul (α := R) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j₂ * i₂)) : ℤ) : R)
      (HSMul.hSMul (β := DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜)
        (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₁) * HPow.hPow (α := ℤˣ) (-1) (i₁ * j₂))
        (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
            ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i)
            ((lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂ : ⨁ (i : ι), ℬ i) ⊗ₜ[R]
          HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
            ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ : ⨁ (i : ι), 𝒜 i)
            ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i)))
have a : HSMul.hSMul (β := (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₂ + (j₁ * i₁ + j₂ * i₁ + (j₁ * i₂ + j₂ * i₂))))
    (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i)
        ((lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂ : ⨁ (i : ι), ℬ i) ⊗ₜ[R]
      HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ : ⨁ (i : ι), 𝒜 i)
        ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i)) =
  HSMul.hSMul (α := R) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j₂ * i₂)) : ℤ) : R)
    (HSMul.hSMul (β := DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜) (HPow.hPow (α := ℤˣ) (-1) (j₁ * i₁ + j₂ * i₁))
      (HMul.hMul (α := ⨁ (i : ι), ℬ i) (β := ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ j₁ : (a : ℬ j₁) → ⨁ (i : ι), ℬ i) b₁ : ⨁ (i : ι), ℬ i)
          ((lof R ι ℬ j₂ : (a : ℬ j₂) → ⨁ (i : ι), ℬ i) b₂ : ⨁ (i : ι), ℬ i) ⊗ₜ[R]
        HMul.hMul (α := ⨁ (i : ι), 𝒜 i) (β := ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 i₁ : (a : 𝒜 i₁) → ⨁ (i : ι), 𝒜 i) a₁ : ⨁ (i : ι), 𝒜 i)
          ((lof R ι 𝒜 i₂ : (a : 𝒜 i₂) → ⨁ (i : ι), 𝒜 i) a₂ : ⨁ (i : ι), 𝒜 i)))
Tactic: simp_rw [← uzpow_add, mul_add, add_mul, mul_comm i₁ j₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
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 (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1
have 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
Tactic: rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
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
⊢ Eq (α := (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i))
    ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) 1) 1
have 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))
Tactic: rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]