-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem rTensor_injective_of_forall_vanishesTrivially
    (hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N},
      ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N) → VanishesTrivially R m n)
    (M' : Submodule R M) : Injective (rTensor N M'.subtype)

Proof state:
case h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i : Fin l, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card { x // x ∈ s }) ≃ { x // x ∈ s }
hx : ∑ i : Fin (Fintype.card { x // x ∈ s }), ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card { x // x ∈ s })), (fun i => (↑(e i)).2) i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i : Fin (Fintype.card { x // x ∈ s }), a i j • (fun i => ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card { x // x ∈ s }) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • (fun i => ↑(↑(e i)).1) i = 0 ↔
    ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • ((fun i => (↑i).1) ∘ ⇑e) i = 0

Tactic:
convert (injective_iff_map_eq_zero' _).mp (injective_subtype M') _

Result:
case h.e'_1.h.e'_2
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i : Fin l, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card { x // x ∈ s }) ≃ { x // x ∈ s }
hx : ∑ i : Fin (Fintype.card { x // x ∈ s }), ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card { x // x ∈ s })), (fun i => (↑(e i)).2) i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i : Fin (Fintype.card { x // x ∈ s }), a i j • (fun i => ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card { x // x ∈ s }) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • (fun i => ↑(↑(e i)).1) i =
    M'.subtype (∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • ((fun i => (↑i).1) ∘ ⇑e) i)

Proof state:
case intro.hmn
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i : Fin l, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card { x // x ∈ s }) ≃ { x // x ∈ s }
hx : ∑ i : Fin (Fintype.card { x // x ∈ s }), ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card { x // x ∈ s })), (fun i => (↑(e i)).2) i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i : Fin (Fintype.card { x // x ∈ s }), a i j • (fun i => ↑(↑(e i)).1) i = 0
⊢ ∃ k a y,
    (∀ (i : Fin (Fintype.card { x // x ∈ s })), ((fun i => (↑i).2) ∘ ⇑e) i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i : Fin (Fintype.card { x // x ∈ s }), a i j • ((fun i => (↑i).1) ∘ ⇑e) i = 0

Tactic:
convert this

Result:
case h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i : Fin l, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card { x // x ∈ s }) ≃ { x // x ∈ s }
hx : ∑ i : Fin (Fintype.card { x // x ∈ s }), ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card { x // x ∈ s })), (fun i => (↑(e i)).2) i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i : Fin (Fintype.card { x // x ∈ s }), a i j • (fun i => ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card { x // x ∈ s }) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • ((fun i => (↑i).1) ∘ ⇑e) i = 0 ↔
    ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • (fun i => ↑(↑(e i)).1) i = 0