Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
⊢ (TensorProduct.comm R A B) 0 =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      0

pp: case tmul
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ : A
y✝ : B
⊢ (TensorProduct.comm R A B) (x✝ ⊗ₜ[R] y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ ⊗ₜ[R] y✝)

pp: case add
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ y✝ : A ⊗[R] B
a✝¹ :
  (TensorProduct.comm R A B) x✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      x✝
a✝ :
  (TensorProduct.comm R A B) y✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      y✝
⊢ (TensorProduct.comm R A B) (x✝ + y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ + y✝)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
⊢ (TensorProduct.comm R A B) 0 =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      0

case tmul
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ : A
y✝ : B
⊢ (TensorProduct.comm R A B) (x✝ ⊗ₜ[R] y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ ⊗ₜ[R] y✝)

case add
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ y✝ : A ⊗[R] B
a✝¹ :
  (TensorProduct.comm R A B) x✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      x✝
a✝ :
  (TensorProduct.comm R A B) y✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      y✝
⊢ (TensorProduct.comm R A B) (x✝ + y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ + y✝)