-- 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:
case intro.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
ι : 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)
hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ VanishesTrivially R m n

Tactic:
refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_

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)
hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ ∀ (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

case intro.intro.refine_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
ι : 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)
hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ ∀ (j : { x // x ∈ ma }),
    ∑ i : ι,
        (fun i x =>
              match x with
              | ⟨(kj, snd), property⟩ => ↑kj i)
            i j •
          m i =
      0

Proof state:
case h.e'_3.a.isFalse
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.1 i = 0
⊢ ↑x.1 i • x.2 = ↑x.1 i • x.2

Tactic:
rfl

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)
hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ ∀ (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:
intro i

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)
hkn : (rTensor N (ker G).subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
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

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
i : ι
⊢ G (Finsupp.single i 1) = m i

Tactic:
simp [hG, toModule_lof]

Result:
no goals