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)
a : 𝒜 0
b : ⨁ (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] b) :
      (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)
    (b ⊗ₜ[R] (lof R ι 𝒜 0 : (a : 𝒜 0) → ⨁ (i : ι), 𝒜 i) 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) ∘ₗ
    (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: 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
-- 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 : 𝒜 0
b : ⨁ (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))
have 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)
Tactic: ext i b
-- 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 : 𝒜 0
b_1 : ⨁ (i : ι), ℬ i
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)
have 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)
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 : 𝒜 0
b_1 : ⨁ (i : ι), ℬ i
i : ι
b : ℬ 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)
have 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
Tactic: rw [gradedComm_of_tmul_of, mul_zero, 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 : 𝒜 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
⊢ 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)
have 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
Tactic: rw [gradedComm_of_tmul_of, mul_zero, 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 : 𝒜 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
⊢ 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)
have 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
Tactic: rw [gradedComm_of_tmul_of, mul_zero, 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 : 𝒜 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
⊢ 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)
have 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)
Tactic: rw [gradedComm_of_tmul_of, mul_zero, 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)
inst_8 : DirectSum.GRing 𝒜
inst_9 : DirectSum.GRing ℬ
inst_10 : DirectSum.GAlgebra R 𝒜
inst_11 : DirectSum.GAlgebra R ℬ
⊢ DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
have refine : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
Tactic: refine TensorProduct.curry ?_
-- 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 ℬ
⊢ DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
have refine : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
  ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)
Tactic: refine map (LinearMap.mul' R (⨁ i, 𝒜 i)) (LinearMap.mul' R (⨁ i, ℬ i)) ∘ₗ ?_
-- 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 ℬ
⊢ DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
    ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)
have refine : DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)
Tactic: refine (assoc R _ _ _).symm.toLinearMap ∘ₗ .lTensor _ ?_ ∘ₗ (assoc R _ _ _).toLinearMap
-- 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 ℬ
⊢ DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
    (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)
have refine : DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
Tactic: refine (assoc R _ _ _).toLinearMap ∘ₗ .rTensor _ ?_ ∘ₗ (assoc R _ _ _).symm.toLinearMap
-- 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
⊢ (((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
have 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 ι ℬ)
Tactic: suffices gradedMul R 𝒜 ℬ (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 ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
⊢ 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 ι ℬ)
have 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 ι ℬ)
Tactic: ext ia a ib b
-- 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
⊢ (((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)
have 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)
Tactic: erw [tmul_of_gradedMul_of_tmul]