-- 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 => (↑i).1) ∘ ⇑e) i = 0 ↔
    ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • (fun i => ↑(↑(e i)).1) i = 0

Tactic:
symm

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 => ↑(↑(e i)).1) i = 0 ↔
    ∑ i : Fin (Fintype.card { x // x ∈ s }), x✝¹ i a✝ • ((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)
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

Tactic:
rw [← e.vanishesTrivially_comp]

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) ∘ ⇑e) ((fun i => (↑i).2) ∘ ⇑e)

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
x : ↥M' ⊗[R] N
hx : (rTensor N M'.subtype) x = 0
⊢ x = 0

Tactic:
obtain ⟨s, rfl⟩ := exists_finset x

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
⊢ ∑ i ∈ s, i.1 ⊗ₜ[R] i.2 = 0

Proof state:
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)

Tactic:
simp

Result:
no goals

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

Tactic:
rintro x hx

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
x : ↥M' ⊗[R] N
hx : (rTensor N M'.subtype) x = 0
⊢ x = 0

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

Tactic:
apply sum_tmul_eq_zero_of_vanishesTrivially

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