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 :
  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')) ⊤
⊢ 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)

Tactic:
simp only [m'_eq, map_sum, rTensor_tmul, coe_subtype, Subtype.coind_coe, map_zero, hmn]

Premises used: LinearMap.rTensor_tmul, map_zero, map_sum, Subtype.coind_coe, Submodule.coe_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'
hm' : Eq (α := Submodule R ↥(span R (Set.range m))) (span R (Set.range m')) ⊤
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0

Tactic:
have hm'n : ∑ i, m' i ⊗ₜ n i = (0 : span R (Set.range m) ⊗[R] N) := by
    apply hm
    simp only [m'_eq, map_sum, rTensor_tmul, coe_subtype, Subtype.coind_coe, map_zero, hmn]
-- 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')) ⊤
hm'n : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0
⊢ VanishesTrivially R m' n

Tactic:
have : VanishesTrivially R m' n := vanishesTrivially_of_sum_tmul_eq_zero R hm' hm'n
-- 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')) ⊤
hm'n : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0
this :
  ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, a i j • m' i) 0
⊢ ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, a i j • m' i) 0

Tactic:
this
-- 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')) ⊤
hm'n : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0
this :
  ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, a i j • m' i) 0
h :
  ∀ (κ : ℕ) (x : ι → Fin κ → R) (a : Fin κ → N) (y : Fin κ),
    Eq.{u_2 + 1} (α := M) (∑ i : ι, x i y • m i) 0 ↔
      Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, x i y • m' i) 0
⊢ ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧ ∀ (j : Fin k), Eq.{u_2 + 1} (α := M) (∑ i : ι, a i j • m i) 0

Tactic:
convert! this with κ _ a y j
-- 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')) ⊤
hm'n : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0
this :
  ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, a i j • m' i) 0
κ : ℕ
x : ι → Fin κ → R
a : Fin κ → N
y : Fin κ
⊢ Eq (α := M)
      ((Submodule.subtype (span R (Set.range m)) : (a : ↥(span R (Set.range m))) → M) (∑ i : ι, x i y • m' i) : M)
      (0 : M) ↔
    Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, x i y • m' i) 0

Tactic:
(injective_iff_map_eq_zero' _).mp (injective_subtype (span R (Set.range m))) _

Premises used: injective_iff_map_eq_zero', Submodule.injective_subtype, Submodule.span, Iff.mp, Set.range
-- 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')) ⊤
hm'n : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0
this :
  ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, a i j • m' i) 0
κ : ℕ
x : ι → Fin κ → R
a : Fin κ → N
y : Fin κ
h :
  Eq (α := M) (∑ i : ι, x i y • m i : M)
    ((Submodule.subtype (span R (Set.range m)) : (a : ↥(span R (Set.range m))) → M) (∑ i : ι, x i y • m' i) : M)
⊢ Eq.{u_2 + 1} (α := M) (∑ i : ι, x i y • m i) 0 ↔ Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, x i y • m' i) 0

Tactic:
convert! (injective_iff_map_eq_zero' _).mp (injective_subtype (span R (Set.range m))) _

Premises used: injective_iff_map_eq_zero', Submodule.injective_subtype, Submodule.span, Iff.mp, Set.range
-- 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')) ⊤
hm'n : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥(span R (Set.range m))) N) (∑ i : ι, m' i ⊗ₜ[R] n i) 0
this :
  ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N),
    (∀ (i : ι), n i = ∑ j : Fin k, a i j • y j) ∧
      ∀ (j : Fin k), Eq.{u_2 + 1} (α := ↥(span R (Set.range m))) (∑ i : ι, a i j • m' i) 0
κ : ℕ
x : ι → Fin κ → R
a : Fin κ → N
y : Fin κ
⊢ Eq (α := M) (∑ i : ι, x i y • m i : M)
    ((Submodule.subtype (span R (Set.range m)) : (a : ↥(span R (Set.range m))) → M) (∑ i : ι, x i y • m' i) : M)

Tactic:
simp [m'_eq]
-- 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)
⊢ 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_of_rTensor_injective R hm⟩

Premises used: TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective, 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
apply :
  ∀ (a : TensorProduct.{u_1, u_2, u_3} R (↥M') N),
    Eq (α := M ⊗[R] N) ((rTensor N M'.subtype : (a : ↥M' ⊗[R] N) → M ⊗[R] N) a : M ⊗[R] N) (0 : M ⊗[R] N) → a = 0
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R (↥M') N) (β := M ⊗[R] N)
    (⇑(rTensor N M'.subtype) : (a : ↥M' ⊗[R] N) → M ⊗[R] N)

Tactic:
apply (injective_iff_map_eq_zero _).mpr

Premises used: Iff.mpr, injective_iff_map_eq_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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
x : TensorProduct.{u_1, u_2, u_3} R (↥M') N
hx : Eq (α := M ⊗[R] N) ((rTensor N M'.subtype : (a : ↥M' ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N) (0 : M ⊗[R] N)
obtain :
  ∀ (s : Finset (Prod.{u_2, u_3} (↥M') N))
    (hx : Eq (α := M ⊗[R] N) ((rTensor N M'.subtype : (a : ↥M' ⊗[R] N) → M ⊗[R] N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2)) 0),
    Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥M') N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) 0
⊢ x = 0

Tactic:
obtain ⟨s, rfl⟩ := exists_finset x

Premises used: TensorProduct.exists_finset, 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
hx : Eq (α := M ⊗[R] N) ((rTensor N M'.subtype : (a : ↥M' ⊗[R] N) → M ⊗[R] N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2)) 0
rw : Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥M') N) (∑ x ∈ s.attach, (↑x : ↥M' × N).1 ⊗ₜ[R] (↑x : ↥M' × N).2) 0
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥M') N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) 0

Tactic:
rw [← Finset.sum_attach]

Premises used: Finset.sum_attach
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
hx : Eq (α := M ⊗[R] N) ((rTensor N M'.subtype : (a : ↥M' ⊗[R] N) → M ⊗[R] N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2)) 0
hmn : VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (↥M') N) (∑ x ∈ s.attach, (↑x : ↥M' × N).1 ⊗ₜ[R] (↑x : ↥M' × N).2) 0

Tactic:
apply sum_tmul_eq_zero_of_vanishesTrivially

Premises used: TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
hx : Eq (α := M ⊗[R] N) ((rTensor N M'.subtype : (a : ↥M' ⊗[R] N) → M ⊗[R] N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2)) 0
⊢ Eq (α := M ⊗[R] N) (∑ x ∈ s, (↑x.1 : M) ⊗ₜ[R] x.2) 0

Tactic:
simp only [map_sum, rTensor_tmul, coe_subtype] at hx

Premises used: LinearMap.rTensor_tmul, map_sum, Submodule.coe_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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
hx : Eq (α := M ⊗[R] N) (∑ x ∈ s, (↑x.1 : M) ⊗ₜ[R] x.2) 0
hmn :
  ∀ (e : Fin (Fintype.card ↥s) ≃ ↥s),
    VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2

Tactic:
have e := (Fintype.equivFin s).symm
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
hx : Eq (α := M ⊗[R] N) (∑ x ∈ s, (↑x.1 : M) ⊗ₜ[R] x.2) 0
e : Fin (Fintype.card ↥s) ≃ ↥s
hmn :
  ∀ (e : Fin (Fintype.card ↥s) ≃ ↥s)
    (hx :
      Eq (α := M ⊗[R] N)
        (∑ i : Fin (Fintype.card ↥s),
          (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
            (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
        0),
    VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2

Tactic:
rw [← Finset.sum_coe_sort, ← e.sum_comp] at hx

Premises used: Equiv.sum_comp, Finset.sum_coe_sort
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx :
  Eq (α := M ⊗[R] N)
    (∑ i : Fin (Fintype.card ↥s),
      (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
        (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
    0
⊢ VanishesTrivially.{u_1, u_2, u_3, 0} R (M := M) (N := N)
    (fun (i : Fin (Fintype.card ↥s)) ↦ (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M))
    fun (i : Fin (Fintype.card ↥s)) ↦ (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2

Tactic:
have := hMN hx
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx :
  Eq (α := M ⊗[R] N)
    (∑ i : Fin (Fintype.card ↥s),
      (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
        (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
    0
this :
  VanishesTrivially.{u_1, u_2, u_3, 0} R (M := M) (N := N)
    (fun (i : Fin (Fintype.card ↥s)) ↦ (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M))
    fun (i : Fin (Fintype.card ↥s)) ↦ (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2
hmn :
  VanishesTrivially.{u_1, u_2, u_3, 0} R (M := ↥M') (N := N) (ι := Fin (Fintype.card ↥s))
    ((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s))
    ((fun (i : ↥s) ↦ (↑i : ↥M' × N).2) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s))
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2

Tactic:
rw [← e.vanishesTrivially_comp]

Premises used: Equiv.vanishesTrivially_comp
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx :
  Eq (α := M ⊗[R] N)
    (∑ i : Fin (Fintype.card ↥s),
      (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
        (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
    0
this :
  ∃ (k : ℕ) (a : Fin (Fintype.card ↥s) → Fin k → R) (y : Fin k → N),
    (∀ (i : Fin (Fintype.card ↥s)),
        Eq.{u_3 + 1} (α := N)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2 : N)) i)
          (∑ j : Fin k, a i j • y j)) ∧
      ∀ (j : Fin k),
        Eq.{u_2 + 1} (α := M)
          (∑ i : Fin (Fintype.card ↥s),
            HSMul.hSMul (β := M) (a i j)
              ((fun (i : Fin (Fintype.card ↥s)) ↦
                  ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
                i))
          0
⊢ ∃ (k : ℕ) (a : Fin (Fintype.card ↥s) → Fin k → R) (y : Fin k → N),
    (∀ (i : Fin (Fintype.card ↥s)),
        Eq.{u_3 + 1} (α := N)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2 : N)) i)
          (∑ j : Fin k, a i j • y j)) ∧
      ∀ (j : Fin k),
        Eq.{u_2 + 1} (α := M)
          (∑ i : Fin (Fintype.card ↥s),
            HSMul.hSMul (β := M) (a i j)
              ((fun (i : Fin (Fintype.card ↥s)) ↦
                  ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
                i))
          0

Tactic:
this