-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedComm_tmul_of_zero (a : ⨁ i, 𝒜 i) (b : ℬ 0) :
    gradedComm R 𝒜 ℬ (a ⊗ₜ lof R _ ℬ 0 b) = lof R _ ℬ _ b ⊗ₜ a

Proof state:
case H.h
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ ((↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)).flip ((lof R ι ℬ 0) b)) ∘ₗ lof R ι 𝒜 i) a =
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) ((lof R ι ℬ 0) b) ∘ₗ lof R ι 𝒜 i) a

Tactic:
dsimp

Result:
case H.h
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ (gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ 0) b) = (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Proof state:
case H.h
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ (gradedComm R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ 0) b) = (lof R ι ℬ 0) b ⊗ₜ[R] (lof R ι 𝒜 i) a

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

Result:
no goals

Proof state:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : ⨁ (i : ι), 𝒜 i
b : ℬ 0
⊢ ↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)).flip ((lof R ι ℬ 0) b) =
    (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) ((lof R ι ℬ 0) b)

Tactic:
ext i a

Result:
case H.h
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a✝ : ⨁ (i : ι), 𝒜 i
b : ℬ 0
i : ι
a : 𝒜 i
⊢ ((↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)).flip ((lof R ι ℬ 0) b)) ∘ₗ lof R ι 𝒜 i) a =
    ((mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) ((lof R ι ℬ 0) b) ∘ₗ lof R ι 𝒜 i) a

Proof state:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : ⨁ (i : ι), 𝒜 i
b : ℬ 0
⊢ (gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (lof R ι ℬ 0) b) = (lof R ι ℬ 0) b ⊗ₜ[R] a

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

Result:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
a : ⨁ (i : ι), 𝒜 i
b : ℬ 0
⊢ ↑(gradedComm R 𝒜 ℬ) ∘ₗ (mk R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i)).flip ((lof R ι ℬ 0) b) =
    (mk R (⨁ (i : ι), ℬ i) (⨁ (i : ι), 𝒜 i)) ((lof R ι ℬ 0) b)