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
⊢ ∀ (i : ι), (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i

Tactic:
have G_basis_eq (i : ι) : G (Finsupp.single i 1) = m i := by simp [hG]
-- 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
apply : G.range = ⊤
⊢ Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)

Tactic:
apply LinearMap.range_eq_top.mp

Premises used: LinearMap.range_eq_top, Iff.mp
-- 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
apply : ⊤ ≤ G.range
⊢ G.range = ⊤

Tactic:
apply top_le_iff.mp

Premises used: top_le_iff, Iff.mp
-- 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
rw : span R (Set.range m) ≤ G.range
⊢ ⊤ ≤ G.range

Tactic:
rw [← hm]
-- 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
apply : Set.range m ⊆ (↑G.range : Set M)
⊢ span R (Set.range m) ≤ G.range

Tactic:
apply Submodule.span_le.mpr

Premises used: Iff.mpr, Submodule.span_le
-- 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
i : ι
w : ι →₀ R
h : (G : (a : ι →₀ R) → M) (Finsupp.single i 1) = m i
⊢ m i ∈ (↑G.range : Set M)

Tactic:
use Finsupp.single i 1, G_basis_eq i

Premises used: OfNat.ofNat, Finsupp.single
-- 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
⊢ Surjective (α := ι →₀ R) (β := M) (⇑G : (a : ι →₀ R) → M)

Tactic:
have G_surjective : Surjective G := by
    apply LinearMap.range_eq_top.mp
    apply top_le_iff.mp
    rw [← hm]
    apply Submodule.span_le.mpr
    rintro _ ⟨i, rfl⟩
    use Finsupp.single i 1, G_basis_eq i
-- 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)
⊢ let en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i;
  en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i

Tactic:
set en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ n i with hen

Premises used: Finsupp
-- 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
⊢ Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (ker (rTensor N G)) en

Tactic:
simp [hen, G_basis_eq, 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 : 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
⊢ Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (ker (rTensor N G)) en

Tactic:
have en_mem_ker : en ∈ ker (rTensor N G) := by simp [hen, G_basis_eq, 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 : 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 (M := ↥G.ker) (N := ι →₀ R) (P := M) (⇑G.ker.subtype : (a : ↥G.ker) → ι →₀ R) (⇑G : (a : ι →₀ R) → M)

Tactic:
have exact_ker_subtype : Exact (ker G).subtype G := G.exact_subtype_ker_map
-- 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 (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)

Tactic:
have exact_rTensor_ker_subtype : Exact (rTensor N (ker G).subtype) (rTensor N G) :=
    rTensor_exact (M := ↥(ker G)) N exact_ker_subtype G_surjective
-- 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)
⊢ 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
-- 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)
en_mem_range : Membership.mem (γ := Submodule R ((ι →₀ R) ⊗[R] N)) (range (rTensor N G.ker.subtype)) en
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
⊢ VanishesTrivially R m n

Tactic:
obtain ⟨kn, hkn⟩ := en_mem_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 : 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
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
⊢ VanishesTrivially R m n

Tactic:
obtain ⟨ma, rfl : kn = ∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2⟩ := exists_finset kn

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

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

Premises used: _private.0.TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero.match_1, TensorProduct.VanishesTrivially.of_fintype, Subtype.val, 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)
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)
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
⊢ VanishesTrivially R m n

Tactic:
refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_
-- 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
i : ι
⊢ 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

Premises used: TensorProduct.finsuppScalarLeft
-- 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 (α := ι →₀ 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)
⊢ 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
-- 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)
            ((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)
⊢ 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