-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem forall_vanishesTrivially_iff_forall_fg_rTensor_injective :
    (∀ {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) (_ : M'.FG), Injective (rTensor N M'.subtype)

Proof state:
case mp
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
⊢ (∀ {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), M'.FG → Injective ⇑(rTensor N M'.subtype)

Tactic:
intro h M' _

Result:
case mp
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
h : ∀ {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'.FG
⊢ Injective ⇑(rTensor N M'.subtype)

Proof state:
case mp
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
h : ∀ {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'.FG
⊢ Injective ⇑(rTensor N M'.subtype)

Tactic:
exact rTensor_injective_of_forall_vanishesTrivially R h M'

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
⊢ (∀ {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), M'.FG → Injective ⇑(rTensor N M'.subtype)

Tactic:
constructor

Result:
case mp
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
⊢ (∀ {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), M'.FG → Injective ⇑(rTensor N M'.subtype)

case mpr
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
⊢ (∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i : Fin l, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Proof state:
case mpr
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
⊢ (∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i : Fin l, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
intro h k m n hmn

Result:
case mpr
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
h : ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : ∑ i : Fin k, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Proof state:
case mpr
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
h : ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : ∑ i : Fin k, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Tactic:
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R
  (h _ (fg_span (Set.finite_range _))) hmn

Result:
no goals