awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
i : ι
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 =
    ∑ 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

Tactic:
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

Premises used: Finsupp.mem_support_iff, Finset.mem_univ, Finset.sum_ite_eq', LinearMap.rTensor_tmul, Finsupp.sum_single_index, Finsupp.sum_ite_eq', map_sum, ne_eq, one_smul, zero_smul, TensorProduct.finsuppScalarLeft_apply_tmul, Submodule.coe_subtype, ite_not, reduceIte, Finsupp.single_apply, Finsupp.finsetSum_apply, Finsupp.sum_apply, Finsupp.single_zero
-- 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)
i : ι
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
refine_1 : n i = ∑ x ∈ ma, 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:
simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]

Premises used: Finset.sum_attach, Prod.fst, Finset.univ_eq_attach, HSMul.hSMul, Subtype.val, Prod.snd, DFunLike.coe
-- 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)
i : ι
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,
      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

Tactic:
hkn
-- 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)
i : ι
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
h :
  ∀ 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
⊢ n i = ∑ x ∈ ma, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2

Tactic:
convert! hkn using 2 with x _
-- 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)
i : ι
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 : ↥G.ker × N
h_1 : x ∈ ma
h :
  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₁ :
  ¬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
⊢ 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

Tactic:
split
-- 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)
i : ι
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 : ↥G.ker × N
h : x ∈ ma
h'x : Eq.{u_1 + 1} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x.2 = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := N) 0 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2 = 0

Tactic:
rw [h'x, zero_smul]

Premises used: zero_smul
-- 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)
i : ι
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 : ↥G.ker × N
h : x ∈ ma
h_1 : ¬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

Tactic:
rfl
-- 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
snd : N
k : ι →₀ R
hk : k ∈ G.ker
property : (Subtype.mk (p := fun (x : ι →₀ R) ↦ x ∈ G.ker) k hk, snd) ∈ ma
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((fun (i : ι) (x : ↥ma) ↦
            (match (motive := ↥ma → R) x with
              | ⟨(kj, snd), property⟩ => ((↑kj : ι →₀ R) : (a : ι) → R) i :
              R))
          i
          (Subtype.mk (p := fun (x : ↥G.ker × N) ↦ x ∈ ma) (Subtype.mk (p := fun (x : ι →₀ R) ↦ x ∈ G.ker) k hk, snd)
            property))
        (m i))
    0

Tactic:
simpa only [hG, linearCombination_apply, zero_smul, implies_true, Finsupp.sum_fintype] using
      mem_ker.mp hk

Premises used: Finsupp.sum_fintype, Finsupp.linearCombination_apply, LinearMap.mem_ker, zero_smul, Iff.mp, implies_true
-- 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)) ⊤
⊢ VanishesTrivially R m n ↔ Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0

Tactic:
⟨sum_tmul_eq_zero_of_vanishesTrivially R, vanishesTrivially_of_sum_tmul_eq_zero R hm⟩

Premises used: TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero, TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially, Iff.intro
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
⊢ ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)

Tactic:
have mem_M' i : m i ∈ span R (Set.range m) := subset_span ⟨i, rfl⟩
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
mem_M' : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)
⊢ let m' := Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M';
  m' = Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'

Tactic:
set m' : ι → span R (Set.range m) := Subtype.coind m mem_M' with m'_eq

Premises used: Subtype.coind
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
mem_M' : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)
m' : ι → ↥(span R (Set.range m)) :=
  Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
m'_eq : m' = Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
a :
  Submodule.map (Submodule.subtype (span R (Set.range m))) (span R (Set.range m')) =
    Submodule.map (M := ↥(span R (Set.range m))) (Submodule.subtype (span R (Set.range m))) ⊤
⊢ Eq (α := Submodule R ↥(span R (Set.range m))) (span R (Set.range m')) ⊤

Tactic:
apply map_injective_of_injective (injective_subtype (span R (Set.range m)))

Premises used: Submodule.injective_subtype, Submodule.span, Set.range, Submodule.map_injective_of_injective
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
mem_M' : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)
m' : ι → ↥(span R (Set.range m)) :=
  Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
m'_eq : m' = Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
a :
  Eq (α := Submodule R M)
    (span R
      (Set.range (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) ∘ m')))
    (span R (Set.range m))
⊢ Submodule.map (Submodule.subtype (span R (Set.range m))) (span R (Set.range m')) =
    Submodule.map (M := ↥(span R (Set.range m))) (Submodule.subtype (span R (Set.range m))) ⊤

Tactic:
rw [Submodule.map_span, Submodule.map_top, range_subtype, coe_subtype, ← Set.range_comp]

Premises used: Set.range_comp, Submodule.map_top, Submodule.coe_subtype, Submodule.map_span, Submodule.range_subtype
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
mem_M' : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)
m' : ι → ↥(span R (Set.range m)) :=
  Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
m'_eq : m' = Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
⊢ Eq (α := Submodule R M)
    (span R
      (Set.range (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) ∘ m')))
    (span R (Set.range m))

Tactic:
rfl
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
mem_M' : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)
m' : ι → ↥(span R (Set.range m)) :=
  Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
m'_eq : m' = Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
⊢ Eq (α := Submodule R ↥(span R (Set.range m))) (span R (Set.range m')) ⊤

Tactic:
have hm' : span R (Set.range m') = ⊤ := by
    apply map_injective_of_injective (injective_subtype (span R (Set.range m)))
    rw [Submodule.map_span, Submodule.map_top, range_subtype, coe_subtype, ← Set.range_comp]
    rfl
-- 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 :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (β := M ⊗[R] N)
    (⇑(rTensor N (Submodule.subtype (span R (Set.range m)))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
hmn : Eq (α := M ⊗[R] N) (∑ i : ι, m i ⊗ₜ[R] n i) 0
mem_M' : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (Set.range m)) (m i)
m' : ι → ↥(span R (Set.range m)) :=
  Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
m'_eq : m' = Subtype.coind m (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range m)) x) mem_M'
hm' : Eq (α := Submodule R ↥(span R (Set.range m))) (span R (Set.range m')) ⊤
a :
  Eq (α := M ⊗[R] N)
    ((rTensor N (Submodule.subtype (span R (Set.range m))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N)
      (∑ i : ι, m' i ⊗ₜ[R] n i))
    ((rTensor N (Submodule.subtype (span R (Set.range m))) : (a : ↥(span R (Set.range m)) ⊗[R] N) → M ⊗[R] N) 0)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0

Tactic:
apply hm