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
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
h :
  ∀ (x : ℕ) (x_1 : Fin (Fintype.card ↥s) → Fin x → R) (x_2 : Fin x → N) (a : Fin x),
    Eq.{u_2 + 1} (α := ↥M')
        (∑ i : Fin (Fintype.card ↥s),
          HSMul.hSMul (β := ↥M') (x_1 i a)
            (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i))
        0 ↔
      Eq.{u_2 + 1} (α := M)
        (∑ i : Fin (Fintype.card ↥s),
          HSMul.hSMul (β := M) (x_1 i a)
            ((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 : ↥s) ↦ (↑i : ↥M' × N).2) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) 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 : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i))
          0

Tactic:
convert! 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
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
x : ℕ
x_1 : Fin (Fintype.card ↥s) → Fin x → R
x_2 : Fin x → N
a : Fin x
h :
  Eq.{u_2 + 1} (α := M)
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := M) (x_1 i a)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
            i))
      0 ↔
    Eq.{u_2 + 1} (α := ↥M')
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := ↥M') (x_1 i a)
          (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i))
      0
⊢ Eq.{u_2 + 1} (α := ↥M')
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := ↥M') (x_1 i a)
          (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i))
      0 ↔
    Eq.{u_2 + 1} (α := M)
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := M) (x_1 i a)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
            i))
      0

Tactic:
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)
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
x : ℕ
x_1 : Fin (Fintype.card ↥s) → Fin x → R
x_2 : Fin x → N
a : Fin x
⊢ Eq (α := M)
      ((M'.subtype : (a : ↥M') → M)
          (∑ i : Fin (Fintype.card ↥s),
            HSMul.hSMul (β := ↥M') (x_1 i a)
              (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i)) :
        M)
      (0 : M) ↔
    Eq.{u_2 + 1} (α := ↥M')
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := ↥M') (x_1 i a)
          (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i))
      0

Tactic:
(injective_iff_map_eq_zero' _).mp (injective_subtype M') _

Premises used: injective_iff_map_eq_zero', Submodule.injective_subtype, 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
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
x : ℕ
x_1 : Fin (Fintype.card ↥s) → Fin x → R
x_2 : Fin x → N
a : Fin x
h :
  Eq (α := M)
    (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := M) (x_1 i a)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
            i) :
      M)
    ((M'.subtype : (a : ↥M') → M)
        (∑ i : Fin (Fintype.card ↥s),
          HSMul.hSMul (β := ↥M') (x_1 i a)
            (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i)) :
      M)
⊢ Eq.{u_2 + 1} (α := M)
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := M) (x_1 i a)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
            i))
      0 ↔
    Eq.{u_2 + 1} (α := ↥M')
      (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := ↥M') (x_1 i a)
          (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i))
      0

Tactic:
convert! (injective_iff_map_eq_zero' _).mp (injective_subtype M') _

Premises used: injective_iff_map_eq_zero', Submodule.injective_subtype, 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
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
x : ℕ
x_1 : Fin (Fintype.card ↥s) → Fin x → R
x_2 : Fin x → N
a : Fin x
⊢ Eq (α := M)
    (∑ i : Fin (Fintype.card ↥s),
        HSMul.hSMul (β := M) (x_1 i a)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
            i) :
      M)
    ((M'.subtype : (a : ↥M') → M)
        (∑ i : Fin (Fintype.card ↥s),
          HSMul.hSMul (β := ↥M') (x_1 i a)
            (((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s)) i)) :
      M)

Tactic:
simp
-- 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
mp :
  (∀ {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)
mpr :
  (∀ (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)) →
    ∀ {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
⊢ (∀ {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)

Tactic:
constructor
-- 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
h :
  ∀ {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)

Tactic:
rTensor_injective_of_forall_vanishesTrivially R h

Premises used: TensorProduct.rTensor_injective_of_forall_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
h :
  ∀ {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)

Tactic:
exact rTensor_injective_of_forall_vanishesTrivially R h

Premises used: TensorProduct.rTensor_injective_of_forall_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
h :
  ∀ (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)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : Eq (α := M ⊗[R] N) (∑ i : Fin k, m i ⊗ₜ[R] n i) 0
⊢ VanishesTrivially R m n

Tactic:
vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R (h _) hmn

Premises used: TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
h :
  ∀ (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)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : Eq (α := M ⊗[R] N) (∑ i : Fin k, m i ⊗ₜ[R] n i) 0
⊢ VanishesTrivially R m n

Tactic:
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R (h _) hmn

Premises used: TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
mp :
  (∀ {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),
      M'.FG →
        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)
mpr :
  (∀ (M' : Submodule R M),
      M'.FG →
        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)) →
    ∀ {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
⊢ (∀ {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),
      M'.FG →
        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:
constructor
-- 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
h :
  ∀ {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
mp :
  M'.FG →
    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)
⊢ M'.FG →
    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:
_
-- 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
h :
  ∀ {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
h_1 : M'.FG
⊢ 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:
rTensor_injective_of_forall_vanishesTrivially R h M'

Premises used: TensorProduct.rTensor_injective_of_forall_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
h :
  ∀ {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
h_1 : M'.FG
⊢ 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:
exact rTensor_injective_of_forall_vanishesTrivially R h M'

Premises used: TensorProduct.rTensor_injective_of_forall_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
h :
  ∀ (M' : Submodule R M),
    M'.FG →
      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)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : Eq (α := M ⊗[R] N) (∑ i : Fin k, m i ⊗ₜ[R] n i) 0
⊢ VanishesTrivially R m n

Tactic:
vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R
      (h _ (fg_span (Set.finite_range _))) hmn

Premises used: TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective, Set.finite_range, Submodule.fg_span
-- 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
h :
  ∀ (M' : Submodule R M),
    M'.FG →
      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)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : Eq (α := M ⊗[R] N) (∑ i : Fin k, m i ⊗ₜ[R] n i) 0
⊢ VanishesTrivially R m n

Tactic:
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R
      (h _ (fg_span (Set.finite_range _))) hmn

Premises used: TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective, Set.finite_range, Submodule.fg_span
-- 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 :
  ∀ (M' : Submodule R M),
    M'.FG →
      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)
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)

Tactic:
(forall_vanishesTrivially_iff_forall_rTensor_injective R).mp
    ((forall_vanishesTrivially_iff_forall_fg_rTensor_injective R).mpr hMN) M'

Premises used: TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective, Iff.mpr, TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective, Iff.mp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ Eq.{u + 1} (α := R) ((traceAux R b : (a : M →ₗ[R] M) → R) f : R)
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f) : R)

Tactic:
rfl

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, Matrix.trace, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
κ : Type u_1
inst_5 : DecidableEq κ
inst_6 : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R) (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) (f ∘ₗ id)))
rw₁ rw₂ :
  Eq.{u + 1} (α := R) (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
⊢ Eq.{u + 1} (α := R) (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) ((id ∘ₗ f) ∘ₗ id)))

Tactic:
rw [LinearMap.id_comp, LinearMap.comp_id]

Premises used: LinearMap.comp_id, LinearMap.id_comp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
κ : Type u_1
inst_5 : DecidableEq κ
inst_6 : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
rw :
  (HMul.hMul (α := Matrix ι κ R) (β := Matrix κ ι R)
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) (id ∘ₗ f) : Matrix ι κ R)
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R)).trace =
    (HMul.hMul (β := Matrix κ ι R)
        (HMul.hMul (α := Matrix ι κ R) (β := Matrix κ κ R)
          ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R))
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R)).trace
rw₁ rw₂ :
  (HMul.hMul (β := Matrix κ ι R)
        (HMul.hMul (α := Matrix ι κ R) (β := Matrix κ κ R)
          ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R))
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R)).trace =
    (HMul.hMul (β := Matrix κ ι R)
        (HMul.hMul (α := Matrix ι κ R) (β := Matrix κ κ R)
          ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R))
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R)).trace
⊢ Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) ((id ∘ₗ f) ∘ₗ id)) =
    (HMul.hMul (β := Matrix κ ι R)
        (HMul.hMul (α := Matrix ι κ R) (β := Matrix κ κ R)
          ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R))
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R)).trace

Tactic:
rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]

Premises used: LinearMap.toMatrix_comp