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
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) (∑ x ∈ s.attach, (↑x : ↥M' × N).1 ⊗ₜ[R] (↑x : ↥M' × N).2) 0
have hmn : VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
Tactic: apply sum_tmul_eq_zero_of_vanishesTrivially
-- 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
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
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
have hx₁ : Eq (α := M ⊗[R] N) (∑ x ∈ s, (↑x.1 : M) ⊗ₜ[R] x.2) 0
Tactic: simp only [map_sum, rTensor_tmul, coe_subtype] at hx
Cleared hypotheses: 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) (∑ x ∈ s, (↑x.1 : M) ⊗ₜ[R] x.2) 0
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
have hmn : ∀ (e : Fin (Fintype.card ↥s) ≃ ↥s),
  VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
Tactic: have e := (Fintype.equivFin s).symm
-- 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) (∑ x ∈ s, (↑x.1 : M) ⊗ₜ[R] x.2) 0
e : Fin (Fintype.card ↥s) ≃ ↥s
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
have hmn : ∀ (e : Fin (Fintype.card ↥s) ≃ ↥s)
  (hx :
    Eq (α := M ⊗[R] N)
      (∑ i : Fin (Fintype.card ↥s),
        (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
          (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
      0),
  VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
Tactic: rw [← Finset.sum_coe_sort, ← e.sum_comp] at hx
Cleared hypotheses: hx, e
-- 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
hMN :
  ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, Eq (α := M ⊗[R] N) (∑ i : Fin l, m i ⊗ₜ[R] n i) 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (Prod.{u_2, u_3} (↥M') N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx :
  Eq (α := M ⊗[R] N)
    (∑ i : Fin (Fintype.card ↥s),
      (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
        (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
    0
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
have this : VanishesTrivially.{u_1, u_2, u_3, 0} R (M := M) (N := N)
  (fun (i : Fin (Fintype.card ↥s)) ↦ (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M))
  fun (i : Fin (Fintype.card ↥s)) ↦ (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2
Tactic: have := hMN 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)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx :
  Eq (α := M ⊗[R] N)
    (∑ i : Fin (Fintype.card ↥s),
      (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
        (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
    0
this :
  VanishesTrivially.{u_1, u_2, u_3, 0} R (M := M) (N := N)
    (fun (i : Fin (Fintype.card ↥s)) ↦ (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M))
    fun (i : Fin (Fintype.card ↥s)) ↦ (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2
⊢ VanishesTrivially R (M := ↥M') (N := N) (fun (i : ↥s) ↦ (↑i : ↥M' × N).1) fun (i : ↥s) ↦ (↑i : ↥M' × N).2
have hmn : VanishesTrivially.{u_1, u_2, u_3, 0} R (M := ↥M') (N := N) (ι := Fin (Fintype.card ↥s))
  ((fun (i : ↥s) ↦ (↑i : ↥M' × N).1) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s))
  ((fun (i : ↥s) ↦ (↑i : ↥M' × N).2) ∘ (⇑e : (a : Fin (Fintype.card ↥s)) → ↥s))
Tactic: rw [← e.vanishesTrivially_comp]
-- 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)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx :
  Eq (α := M ⊗[R] N)
    (∑ i : Fin (Fintype.card ↥s),
      (↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) ⊗ₜ[R]
        (↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2)
    0
this :
  ∃ (k : ℕ) (a : Fin (Fintype.card ↥s) → Fin k → R) (y : Fin k → N),
    (∀ (i : Fin (Fintype.card ↥s)),
        Eq.{u_3 + 1} (α := N)
          ((fun (i : Fin (Fintype.card ↥s)) ↦ ((↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).2 : N)) i)
          (∑ j : Fin k, a i j • y j)) ∧
      ∀ (j : Fin k),
        Eq.{u_2 + 1} (α := M)
          (∑ i : Fin (Fintype.card ↥s),
            HSMul.hSMul (β := M) (a i j)
              ((fun (i : Fin (Fintype.card ↥s)) ↦
                  ((↑(↑((e : (a : Fin (Fintype.card ↥s)) → ↥s) i) : ↥M' × N).1 : M) : M))
                i))
          0
⊢ ∃ (k : ℕ) (a : Fin (Fintype.card ↥s) → Fin k → R) (y : Fin k → N),
    (∀ (i : Fin (Fintype.card ↥s)),
        Eq.{u_3 + 1} (α := N) (((fun (i : ↥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
have 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
Tactic: convert! this
-- 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)
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.{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
have 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
Tactic: symm
-- 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)
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.{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
have 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)
Tactic: convert! (injective_iff_map_eq_zero' _).mp (injective_subtype 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
⊢ (∀ {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 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)
Tactic: constructor
-- 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
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)
⊢ (∀ {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 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
Tactic: constructor
-- 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
⊢ (∀ {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)
have 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)
Tactic: constructor
-- 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
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)
⊢ (∀ {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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [LinearMap.id_comp, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)))
⊢ 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)))
have 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))
Tactic: rw [LinearMap.id_comp, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ 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
have 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
Tactic: rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ 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
have 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
Tactic: rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ (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 c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace
have rw : (HMul.hMul (α := Matrix ι κ R) ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
      (HMul.hMul (α := Matrix κ κ R) (β := 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 c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
      ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace
Tactic: rw [Matrix.mul_assoc, Matrix.trace_mul_comm]