-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma lTensor_reflects_exact [fl : FaithfullyFlat R M]
    (ex : Function.Exact (l12.lTensor M) (l23.lTensor M)) :
    Function.Exact l12 l23 :=
  rTensor_reflects_exact R M _ _ <| ex.of_ladder_linearEquiv_of_exact
    (e₁ := TensorProduct.comm _ _ _) (e₂ := TensorProduct.comm _ _ _)
    (e₃ := TensorProduct.comm _ _ _) (by ext; rfl) (by ext; rfl)

Proof state:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
⊢ LinearMap.rTensor M l23 ∘ₗ ↑(TensorProduct.comm R M N2) = ↑(TensorProduct.comm R M N3) ∘ₗ LinearMap.lTensor M l23

Tactic:
ext

Result:
case a.h.h
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N2
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l23 ∘ₗ ↑(TensorProduct.comm R M N2))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N3) ∘ₗ LinearMap.lTensor M l23)) x✝¹) x✝

Proof state:
case a.h.h
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N1
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l12 ∘ₗ ↑(TensorProduct.comm R M N1))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N2) ∘ₗ LinearMap.lTensor M l12)) x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
⊢ LinearMap.rTensor M l12 ∘ₗ ↑(TensorProduct.comm R M N1) = ↑(TensorProduct.comm R M N2) ∘ₗ LinearMap.lTensor M l12

Tactic:
ext

Result:
case a.h.h
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N1
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l12 ∘ₗ ↑(TensorProduct.comm R M N1))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N2) ∘ₗ LinearMap.lTensor M l12)) x✝¹) x✝

Proof state:
case a.h.h
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
x✝¹ : M
x✝ : N2
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M l23 ∘ₗ ↑(TensorProduct.comm R M N2))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R M N3) ∘ₗ LinearMap.lTensor M l23)) x✝¹) x✝

Tactic:
rfl

Result:
no goals