-- Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
/-- If `B` is a faithfully flat `A`-module and `M` is any `A`-module, the canonical
map `M →ₗ[A] B ⊗[A] M` is injective. -/
lemma Module.FaithfullyFlat.tensorProduct_mk_injective (M : Type*) [AddCommGroup M] [Module A M] :
    Function.Injective (TensorProduct.mk A B M 1)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))

Tactic:
have : (lTensor B <| TensorProduct.mk A B M 1) =
    (TensorProduct.leftComm A B B M).symm.comp (TensorProduct.mk A B (B ⊗[A] M) 1) := by
  apply TensorProduct.ext'
  intro x y
  simp

Result:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))

Proof state:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))

Tactic:
rw [this, coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective]

Result:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑((TensorProduct.mk A B (B ⊗[A] M)) 1)

Proof state:
case H
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ ∀ (x : B) (y : M),
    (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
      (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)

Tactic:
intro x y

Result:
case H
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x : B
y : M
⊢ (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
    (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1

Tactic:
apply TensorProduct.ext'

Result:
case H
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ ∀ (x : B) (y : M),
    (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
      (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑((TensorProduct.mk A B M) 1)

Tactic:
rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]

Result:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))

Proof state:
case H
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x : B
y : M
⊢ (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
    (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective ⇑((TensorProduct.mk A B (B ⊗[A] M)) 1)

Tactic:
exact Algebra.TensorProduct.mk_one_injective_of_isScalarTower _

Result:
no goals