-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem vanishesTrivially_of_sum_tmul_eq_zero (hm : Submodule.span R (Set.range m) = ⊤)
    (hmn : ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N)) : VanishesTrivially R m n

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
⊢ range G = ⊤

Tactic:
apply top_le_iff.mp

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
⊢ ⊤ ≤ range G

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
⊢ VanishesTrivially R m n

Tactic:
set en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ n i with hen

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
⊢ VanishesTrivially R m n

Proof state:
case intro.intro.refine_1
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ ker (rTensor N G)
exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)
ma : Finset (↥(ker G) × N)
i : ι
hkn :
  ((finsuppScalarLeft R N ι) en) i =
    ((finsuppScalarLeft R N ι) ((rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2))) i
⊢ n i =
    ∑ j : { x // x ∈ ma },
      (fun i x =>
            match x with
            | ⟨(kj, snd), property⟩ => ↑kj i)
          i j •
        (fun x =>
            match x with
            | ⟨(fst, yj), property⟩ => yj)
          j

Tactic:
simp only [map_sum, finsuppScalarLeft_apply_tmul, zero_smul, Finsupp.single_zero,
  Finsupp.sum_single_index, one_smul, Finsupp.finset_sum_apply, Finsupp.single_apply,
  Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, rTensor_tmul, coe_subtype, Finsupp.sum_apply,
  Finsupp.sum_ite_eq', Finsupp.mem_support_iff, ne_eq, ite_not, en] at hkn

Result:
case intro.intro.refine_1
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ ker (rTensor N G)
exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)
ma : Finset (↥(ker G) × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
⊢ n i =
    ∑ j : { x // x ∈ ma },
      (fun i x =>
            match x with
            | ⟨(kj, snd), property⟩ => ↑kj i)
          i j •
        (fun x =>
            match x with
            | ⟨(fst, yj), property⟩ => yj)
          j

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ ker (rTensor N G)
exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)
ma : Finset (↥(ker G) × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
x : ↥(ker G) × N
a✝ : x ∈ ma
h'x : ↑x.1 i = 0
⊢ ↑x.1 i • x.2 = 0

Tactic:
rw [h'x, zero_smul]

Result:
no goals

Proof state:
case intro.intro.refine_1
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ ker (rTensor N G)
exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)
ma : Finset (↥(ker G) × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
⊢ n i =
    ∑ j : { x // x ∈ ma },
      (fun i x =>
            match x with
            | ⟨(kj, snd), property⟩ => ↑kj i)
          i j •
        (fun x =>
            match x with
            | ⟨(fst, yj), property⟩ => yj)
          j

Tactic:
simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]

Result:
case intro.intro.refine_1
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ ker (rTensor N G)
exact_ker_subtype : Exact ⇑(ker G).subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N (ker G).subtype) ⇑(rTensor N G)
ma : Finset (↥(ker G) × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
⊢ n i = ∑ x ∈ ma, ↑x.1 i • x.2