-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
ι : Type u_4
inst_5 : Fintype ι
m : ι → M
n : ι → N
hm : Eq (α := Submodule R M) (span R (Set.range m)) ⊤
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
G_surjective : Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)
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 : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (ker (rTensor N G)) en
exact_ker_subtype :
  Exact (M := ↥G.ker) (N := ι →₀ R) (P := M) (⇑G.ker.subtype : (a : ↥G.ker) → ι →₀ R) (⇑G : (a : ι →₀ R) → M)
exact_rTensor_ker_subtype :
  Exact (M := ↥G.ker ⊗[R] N) (N := (ι →₀ R) ⊗[R] N) (P := M ⊗[R] N)
    (⇑(rTensor N G.ker.subtype) : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N)
    (⇑(rTensor N G) : (a : (ι →₀ R) ⊗[R] N) → M ⊗[R] N)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
i : ι
refine_1 :
  ∀
    (hkn :
      Eq (α := ι →₀ N)
        ((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N)
            ((rTensor N G.ker.subtype : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2)) :
          ι →₀ N)
        ((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) en : ι →₀ N)),
    n i =
      ∑ j : ↥ma,
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N)
          ((fun (i : ι) (x : ↥ma) ↦
              (match (motive := ↥ma → R) x with
                | ⟨(kj, snd), property⟩ => ((↑kj : ι →₀ R) : (a : ι) → R) i :
                R))
            i j)
          ((fun (x : ↥ma) ↦
              (match (motive := ↥ma → N) x with
                | ⟨(fst, yj), property⟩ => yj :
                N))
            j)
refine_1₁ :
  ∀
    (hkn :
      Eq.{u_3 + 1} (α := N)
        (((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N)
                ((rTensor N G.ker.subtype : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2)) :
              (a : ι) → N)
            i :
          N)
        ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) en : ι →₀ N) : (a : ι) → N) i : N)),
    n i =
      ∑ j : ↥ma,
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N)
          ((fun (i : ι) (x : ↥ma) ↦
              (match (motive := ↥ma → R) x with
                | ⟨(kj, snd), property⟩ => ((↑kj : ι →₀ R) : (a : ι) → R) i :
                R))
            i j)
          ((fun (x : ↥ma) ↦
              (match (motive := ↥ma → N) x with
                | ⟨(fst, yj), property⟩ => yj :
                N))
            j)
refine_1₂ :
  ∀
    (hkn :
      Eq.{u_3 + 1} (α := N)
        ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) en : ι →₀ N) : (a : ι) → N) i : N)
        (((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N)
                ((rTensor N G.ker.subtype : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2)) :
              (a : ι) → N)
            i :
          N)),
    n i =
      ∑ j : ↥ma,
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N)
          ((fun (i : ι) (x : ↥ma) ↦
              (match (motive := ↥ma → R) x with
                | ⟨(kj, snd), property⟩ => ((↑kj : ι →₀ R) : (a : ι) → R) i :
                R))
            i j)
          ((fun (x : ↥ma) ↦
              (match (motive := ↥ma → N) x with
                | ⟨(fst, yj), property⟩ => yj :
                N))
            j)
refine_1₃ :
  ∀
    (hkn :
      n i =
        ∑ x ∈ ma,
          if Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) then 0
          else HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2),
    n i =
      ∑ j : ↥ma,
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N)
          ((fun (i : ι) (x : ↥ma) ↦
              (match (motive := ↥ma → R) x with
                | ⟨(kj, snd), property⟩ => ((↑kj : ι →₀ R) : (a : ι) → R) i :
                R))
            i j)
          ((fun (x : ↥ma) ↦
              (match (motive := ↥ma → N) x with
                | ⟨(fst, yj), property⟩ => yj :
                N))
            j)
refine_1₄ :
  ∀
    (hkn :
      n i =
        ∑ x ∈ ma,
          if Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) then 0
          else HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2),
    n i = ∑ x ∈ ma, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2
h :
  ∀
    (hkn :
      n i =
        ∑ x ∈ ma,
          if Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) then 0
          else HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2),
    ∀ x ∈ ma,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2 =
        if Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) then 0
        else HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2
h₁ :
  ∀
    (hkn :
      n i =
        ∑ x ∈ ma,
          if Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) then 0
          else HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2),
    ∀ x ∈ ma,
      Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) →
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2 = 0
h₂ h₃ :
  ∀
    (hkn :
      n i =
        ∑ x ∈ ma,
          if Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) then 0
          else HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2),
    ∀ x ∈ ma,
      ¬Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R) →
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2 =
          HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2
⊢ n i =
    ∑ j : ↥ma,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := N)
        ((fun (i : ι) (x : ↥ma) ↦
            (match (motive := ↥ma → R) x with
              | ⟨(kj, snd), property⟩ => ((↑kj : ι →₀ R) : (a : ι) → R) i :
              R))
          i j)
        ((fun (x : ↥ma) ↦
            (match (motive := ↥ma → N) x with
              | ⟨(fst, yj), property⟩ => yj :
              N))
          j)

Tactic:
classical
    apply_fun finsuppScalarLeft R N ι at hkn
    apply_fun (· i) at hkn
    symm at hkn
    simp only [map_sum, finsuppScalarLeft_apply_tmul, zero_smul, Finsupp.single_zero,
      Finsupp.sum_single_index, one_smul, Finsupp.finsetSum_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
    simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]
    convert! hkn using 2 with x _
    split
    · next h'x => rw [h'x, zero_smul]
    · rfl

Premises used: Finsupp.mem_support_iff, Finset.mem_univ, Finset.sum_ite_eq', LinearMap.rTensor_tmul, Finsupp.sum_single_index, Finsupp.sum_ite_eq', Finset.sum_attach, map_sum, ne_eq, Prod.fst, one_smul, zero_smul, Finset.univ_eq_attach, TensorProduct.finsuppScalarLeft_apply_tmul, Submodule.coe_subtype, ite_not, reduceIte, Finsupp.single_apply, HSMul.hSMul, Finsupp.finsetSum_apply, Finsupp.sum_apply, Finsupp.single_zero, Subtype.val, Prod.snd, DFunLike.coe