-- 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:
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
⊢ Injective ⇑(rTensor N M'.subtype)

Tactic:
apply (injective_iff_map_eq_zero _).mpr

Result:
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
⊢ ∀ (a : ↥M' ⊗[R] N), (rTensor N M'.subtype) a = 0 → a = 0

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)
hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

Tactic:
simp only [map_sum, rTensor_tmul, coe_subtype] at hx

Result:
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)
hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

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
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

Tactic:
have := hMN hx

Result:
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 : VanishesTrivially R (fun i => ↑(↑(e i)).1) fun i => (↑(e i)).2
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

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 : VanishesTrivially R (fun i => ↑(↑(e i)).1) fun i => (↑(e i)).2
⊢ VanishesTrivially R ((fun i => (↑i).1) ∘ ⇑e) ((fun i => (↑i).2) ∘ ⇑e)

Tactic:
unfold VanishesTrivially at this ⊢

Result:
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

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)
hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0
e : Fin (Fintype.card { x // x ∈ s }) ≃ { x // x ∈ s }
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

Tactic:
rw [← Finset.sum_coe_sort, ← e.sum_comp] at hx

Result:
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
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

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)
hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

Tactic:
have e := (Fintype.equivFin s).symm

Result:
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)
hx : ∑ x ∈ s, ↑x.1 ⊗ₜ[R] x.2 = 0
e : Fin (Fintype.card { x // x ∈ s }) ≃ { x // x ∈ s }
⊢ VanishesTrivially R (fun i => (↑i).1) fun i => (↑i).2

Proof state:
case intro
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)
hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0
⊢ ∑ i ∈ s, i.1 ⊗ₜ[R] i.2 = 0

Tactic:
rw [← Finset.sum_attach]

Result:
case intro
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)
hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0
⊢ ∑ x ∈ s.attach, (↑x).1 ⊗ₜ[R] (↑x).2 = 0