-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedComm_symm : (gradedComm R 𝒜 ℬ).symm = gradedComm R ℬ 𝒜

Proof state:
case 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)
x✝ : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i
⊢ ((TensorProduct.directSum R R ℬ 𝒜).trans
        ((TensorProduct.directSum R R 𝒜 ℬ).trans
            (LinearEquiv.ofLinear (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).symm)
      x✝ =
    (((TensorProduct.directSum R R ℬ 𝒜).trans
            (LinearEquiv.ofLinear (gradedCommAux R ℬ 𝒜) (gradedCommAux R 𝒜 ℬ) ⋯ ⋯)).trans
        (TensorProduct.directSum R R 𝒜 ℬ).symm)
      x✝

Tactic:
rfl

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)
⊢ (gradedComm R 𝒜 ℬ).symm = gradedComm R ℬ 𝒜

Tactic:
rw [gradedComm, gradedComm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]

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)
⊢ (TensorProduct.directSum R R ℬ 𝒜).trans
      ((TensorProduct.directSum R R 𝒜 ℬ).trans
          (LinearEquiv.ofLinear (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).symm =
    ((TensorProduct.directSum R R ℬ 𝒜).trans
          (LinearEquiv.ofLinear (gradedCommAux R ℬ 𝒜) (gradedCommAux R 𝒜 ℬ) ⋯ ⋯)).trans
      (TensorProduct.directSum R R 𝒜 ℬ).symm

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)
⊢ (TensorProduct.directSum R R ℬ 𝒜).trans
      ((TensorProduct.directSum R R 𝒜 ℬ).trans
          (LinearEquiv.ofLinear (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).symm =
    ((TensorProduct.directSum R R ℬ 𝒜).trans
          (LinearEquiv.ofLinear (gradedCommAux R ℬ 𝒜) (gradedCommAux R 𝒜 ℬ) ⋯ ⋯)).trans
      (TensorProduct.directSum R R 𝒜 ℬ).symm

Tactic:
ext

Result:
case 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)
x✝ : (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i
⊢ ((TensorProduct.directSum R R ℬ 𝒜).trans
        ((TensorProduct.directSum R R 𝒜 ℬ).trans
            (LinearEquiv.ofLinear (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).symm)
      x✝ =
    (((TensorProduct.directSum R R ℬ 𝒜).trans
            (LinearEquiv.ofLinear (gradedCommAux R ℬ 𝒜) (gradedCommAux R 𝒜 ℬ) ⋯ ⋯)).trans
        (TensorProduct.directSum R R 𝒜 ℬ).symm)
      x✝