awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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
⊢ 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
have 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
Tactic: split
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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)
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2 = 0
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x.2 = 0
Tactic: rw [h'x, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2 = 0
have rw₁ : Eq.{u_3 + 1} (α := N) 0 0
Tactic: rw [h'x, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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 : ι
⊢ 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)
have 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)
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
Cleared hypotheses: hkn
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
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
⊢ VanishesTrivially R m n
have mem_M' : ∀ (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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
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)
⊢ VanishesTrivially R m n
have m'_eq : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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')) ⊤
have 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))) ⊤
Tactic: apply map_injective_of_injective (injective_subtype (span R (Set.range m)))
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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'
⊢ 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))) ⊤
have 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))
Tactic: rw [Submodule.map_span, Submodule.map_top, range_subtype, coe_subtype, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
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'
⊢ VanishesTrivially R m n
have hm' : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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
have 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)
Tactic: apply hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
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')) ⊤
⊢ VanishesTrivially R m n
have hm'n : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (hypothesis)
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
have this : VanishesTrivially R m' n
Tactic: have : VanishesTrivially R m' n := vanishesTrivially_of_sum_tmul_eq_zero R hm' hm'n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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} (α := M) (∑ i : ι, a i j • m i) 0
have 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
Tactic: convert! this with κ _ a y j
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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.{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
have 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)
Tactic: convert! (injective_iff_map_eq_zero' _).mp (injective_subtype (span R (Set.range m))) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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
⊢ 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)
have 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
Tactic: apply (injective_iff_map_eq_zero _).mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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)
⊢ x = 0
have 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
Tactic: obtain ⟨s, rfl⟩ := exists_finset x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Vanishing (goal)
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 (α := TensorProduct.{u_1, u_2, u_3} R (↥M') N) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) 0
have 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
Tactic: rw [← Finset.sum_attach]