awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
⊢ VanishesTrivially R m n
have en_mem_range : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (range (rTensor N G.ker.subtype)) en
Tactic: have en_mem_range : en ∈ range (rTensor N (ker G).subtype) :=
    exact_rTensor_ker_subtype.linearMap_ker_eq ▸ en_mem_ker
-- 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)
en_mem_range : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (range (rTensor N G.ker.subtype)) en
⊢ VanishesTrivially R m n
have obtain : ∀ (kn : ↥G.ker ⊗[R] N) (hkn : (rTensor N G.ker.subtype : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N) kn = en),
  VanishesTrivially R m n
Tactic: obtain ⟨kn, hkn⟩ := en_mem_range
Cleared hypotheses: en_mem_range
-- 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)
kn : ↥G.ker ⊗[R] N
hkn : (rTensor N G.ker.subtype : (a : ↥G.ker ⊗[R] N) → (ι →₀ R) ⊗[R] N) kn = en
⊢ VanishesTrivially R m n
have obtain : ∀ (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),
  VanishesTrivially R m n
Tactic: obtain ⟨ma, rfl : kn = ∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2⟩ := exists_finset kn
Cleared hypotheses: kn, hkn
-- 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
⊢ VanishesTrivially R m n
have refine_1 : ∀ (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)
Tactic: refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_
-- 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
refine_1 :
  ∀ (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)
⊢ VanishesTrivially R m n
have refine_2 : ∀ (j : ↥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 j)
        (m i))
    0
Tactic: refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_
-- 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 : 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 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)
Tactic: apply_fun finsuppScalarLeft R N ι at hkn
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 : 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 (α := ι →₀ 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)
have 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)
Tactic: apply_fun (· i) at hkn
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 : 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)
            ((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)
have 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)
Tactic: symm at hkn
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 : 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 =
    ∑ 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 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
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
Cleared hypotheses: hkn
-- 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
⊢ 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 : n i = ∑ x ∈ ma, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2
Tactic: simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]
-- 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
⊢ n i = ∑ x ∈ ma, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (((↑x.1 : ι →₀ R) : (a : ι) → R) i : R) x.2
have 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
Tactic: convert! hkn using 2 with x _
-- 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
⊢ 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 = 0
Tactic: split