-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma LinearMap.rTensor_exact_iff_lTensor_exact :
    Function.Exact (f.rTensor Q) (g.rTensor Q) ↔
    Function.Exact (f.lTensor Q) (g.lTensor Q) :=
  Function.Exact.iff_of_ladder_linearEquiv (e₁ := TensorProduct.comm _ _ _)
    (e₂ := TensorProduct.comm _ _ _) (e₃ := TensorProduct.comm _ _ _)
    (by ext; simp) (by ext; simp)

Proof state:
case a.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : N
⊢ ((AlgebraTensorModule.curry (rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g)) x✝¹) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M) = ↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f

Tactic:
ext

Result:
case a.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f)) x✝¹) x✝

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = ↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g

Tactic:
ext

Result:
case a.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : N
⊢ ((AlgebraTensorModule.curry (rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g)) x✝¹) x✝

Proof state:
case a.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f)) x✝¹) x✝

Tactic:
simp

Result:
no goals