awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
f g : ι →₀ N
hf :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] f) :
      ι →₀ M ⊗[R] N)
    (f.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
hg :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] g) :
      ι →₀ M ⊗[R] N)
    (g.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] (f + g)) :
      ι →₀ M ⊗[R] N)
    ((f + g).sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]

Premises used: map_add, TensorProduct.tmul_add, Finsupp.sum_add_index
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
a : ι
b : N
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] Finsupp.single a b) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum (Finsupp.single a b) fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
simp [finsuppRight]

Premises used: TensorProduct.finsuppRight
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
p : ι →₀ N
zero :
  Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] 0) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
add :
  ∀ (f g : ι →₀ N)
    (hf :
      Eq (α := ι →₀ M ⊗[R] N)
        (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
            (m ⊗ₜ[R] f) :
          ι →₀ M ⊗[R] N)
        (f.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N))
    (hg :
      Eq (α := ι →₀ M ⊗[R] N)
        (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
            (m ⊗ₜ[R] g) :
          ι →₀ M ⊗[R] N)
        (g.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)),
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
          (m ⊗ₜ[R] (f + g)) :
        ι →₀ M ⊗[R] N)
      ((f + g).sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
single :
  ∀ (a : ι) (b : N),
    Eq (α := ι →₀ M ⊗[R] N)
      (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
          (m ⊗ₜ[R] Finsupp.single a b) :
        ι →₀ M ⊗[R] N)
      (Finsupp.sum (Finsupp.single a b) fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] p) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]

Premises used: TensorProduct.finsuppRight, LinearMap.single, map_add, TensorProduct.tmul_add, Submodule.zero, Finsupp.sum_add_index, Submodule.add
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
p : ι →₀ N
i : ι
⊢ Eq.{u_4 + 1} (α := N) ((p : (a : ι) → N) i : N) (0 : N) →
    Eq (α := M ⊗[R] N) ((Finsupp.single i (m ⊗ₜ[R] 0) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N) (0 : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
p : ι →₀ N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
rw₁ :
  Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : N) ↦ (Finsupp.single a₁ (m ⊗ₜ[R] b) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
rw₂ :
  Eq (α := M ⊗[R] N)
    (((Finsupp.single i (m ⊗ₜ[R] (p : (a : ι) → N) i) : ι →₀ M ⊗[R] N) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
rw₃ rw₄ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N) (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
              (m ⊗ₜ[R] p) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)

Tactic:
rw [finsuppRight_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.sum_eq_single, Finsupp.sum_apply, TensorProduct.finsuppRight_apply_tmul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
⊢ Eq (α := M ⊗[R] N)
    ((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) 0 :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
m : M
f : ι →₀ N
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
              (m ⊗ₜ[R] f) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) (m ⊗ₜ[R] f) : M ⊗[R] N)

Tactic:
simp [finsuppRight_apply_tmul_apply]

Premises used: TensorProduct.finsuppRight_apply_tmul_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
x y : M ⊗[R] (ι →₀ N)
hx :
  Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) x :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) x : M ⊗[R] N)
hy :
  Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) y :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) y : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
              (x + y) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) (x + y) : M ⊗[R] N)

Tactic:
simp [map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
t : M ⊗[R] (ι →₀ N)
i : ι
zero :
  Eq (α := M ⊗[R] N)
    ((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) 0 :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) 0 : M ⊗[R] N)
tmul :
  ∀ (m : M) (f : ι →₀ N),
    Eq (α := M ⊗[R] N)
      (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
                (m ⊗ₜ[R] f) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) (m ⊗ₜ[R] f) : M ⊗[R] N)
add :
  ∀ (x y : M ⊗[R] (ι →₀ N))
    (hx :
      Eq (α := M ⊗[R] N)
        (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) x :
                ι →₀ M ⊗[R] N) :
              (a : ι) → M ⊗[R] N)
            i :
          M ⊗[R] N)
        ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) x : M ⊗[R] N))
    (hy :
      Eq (α := M ⊗[R] N)
        (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) y :
                ι →₀ M ⊗[R] N) :
              (a : ι) → M ⊗[R] N)
            i :
          M ⊗[R] N)
        ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) y : M ⊗[R] N)),
    Eq (α := M ⊗[R] N)
      (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
                (x + y) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) (x + y) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) t :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) t : M ⊗[R] N)

Tactic:
induction t with
  | zero => simp
  | tmul m f => simp [finsuppRight_apply_tmul_apply]
  | add x y hx hy => simp [map_add, hx, hy]

Premises used: map_add, Submodule.zero, TensorProduct.tmul, Submodule.add, TensorProduct.finsuppRight_apply_tmul_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
m : M
n : N
h :
  ∀ (a : ι),
    Eq (α := M ⊗[R] N)
      (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
                (m ⊗ₜ[R] Finsupp.single i n) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          a :
        M ⊗[R] N)
      ((Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) a : M ⊗[R] N)
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] Finsupp.single i n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
m : M
n : N
a : ι
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
              (m ⊗ₜ[R] Finsupp.single i n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        a :
      M ⊗[R] N)
    ((Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) a : M ⊗[R] N)

Tactic:
simp +contextual [Finsupp.single_apply, apply_ite]

Premises used: apply_ite, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
m : M
n : N
⊢ Eq (α := M ⊗[R] (ι →₀ N))
    (((LinearEquiv.symm (finsuppRight R S M N ι) : (ι →₀ M ⊗[R] N) ≃ₗ[S] M ⊗[R] (ι →₀ N)) :
          (a : ι →₀ M ⊗[R] N) → M ⊗[R] (ι →₀ N))
        (Finsupp.single i (m ⊗ₜ[R] n)) :
      M ⊗[R] (ι →₀ N))
    (m ⊗ₜ[R] Finsupp.single i n : M ⊗[R] (ι →₀ N))

Tactic:
simp [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
s : S
t : (ι →₀ M) ⊗[R] N
⊢ ((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) (s • t) =
    HSMul.hSMul (β := ι →₀ M ⊗[R] N) s
      (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) t :
        ι →₀ M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
x : (ι →₀ M) ⊗[R] N
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) x :
      ι →₀ M ⊗[R] N)
    (((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N) x :
      ι →₀ M ⊗[R] N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ (((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n

Tactic:
simp [finsuppScalarLeft]

Premises used: TensorProduct.finsuppScalarLeft
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
h :
  ∀ (i : ι),
    Eq.{u_4 + 1} (α := N)
      ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
      ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)
⊢ Eq (α := ι →₀ N) ((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N)
    (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : ι →₀ N)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((p : (a : ι) → R) i : R) (0 : R) →
    Eq.{u_4 + 1} (α := N) ((Finsupp.single i (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 n) : (a : ι) → N) i : N) (0 : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
h :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i
h₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • n) : (a : ι) → N) i
h₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    (Finsupp.single i (HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n) : (a : ι) → N) i
h₃ h₄ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n
⊢ Eq.{u_4 + 1} (α := N)
    ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
    ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)

Tactic:
rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, TensorProduct.finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_eq_single, Finsupp.sum_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
pn : (ι →₀ R) ⊗[R] N
i : ι
⊢ Eq.{u_4 + 1} (α := N) ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) pn : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
        ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ R) ⊗[R] N) → R ⊗[R] N) pn : R ⊗[R] N) :
      N)

Tactic:
simp [finsuppScalarLeft, finsuppLeft_apply]

Premises used: TensorProduct.finsuppScalarLeft, TensorProduct.finsuppLeft_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
i : ι
n : N
⊢ Eq (α := (ι →₀ R) ⊗[R] N)
    ((LinearEquiv.symm (finsuppScalarLeft R N ι) : (a : ι →₀ N) → (ι →₀ R) ⊗[R] N) (Finsupp.single i n) :
      (ι →₀ R) ⊗[R] N)
    (Finsupp.single i 1 ⊗ₜ[R] n : (ι →₀ R) ⊗[R] N)

Tactic:
simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]

Premises used: TensorProduct.finsuppScalarLeft, TensorProduct.finsuppLeft_symm_apply_single
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
          ι →₀ M) :
        (a : ι) → M)
      i =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m

Tactic:
simp [finsuppScalarRight]

Premises used: TensorProduct.finsuppScalarRight
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
h :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := M)
      (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
              ι →₀ M) :
            (a : ι) → M)
          i :
        M)
      ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)
⊢ Eq (α := ι →₀ M)
    (((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
      ι →₀ M)
    (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : ι →₀ M)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((p : (a : ι) → R) i : R) (0 : R) →
    Eq.{u_3 + 1} (α := M) ((Finsupp.single i (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 m) : (a : ι) → M) i : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
h :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i
h₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • m) : (a : ι) → M) i
h₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    (Finsupp.single i (HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m) : (a : ι) → M) i
h₃ h₄ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m
⊢ Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
            ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)

Tactic:
rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, TensorProduct.finsuppScalarRight_apply_tmul_apply, Finsupp.sum_eq_single, Finsupp.sum_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
t : M ⊗[R] (ι →₀ R)
i : ι
⊢ Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) t : ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    (((AlgebraTensorModule.rid R S M : M ⊗[R] R ≃ₗ[S] M) : (a : M ⊗[R] R) → M)
        ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ R)) → M ⊗[R] R) t : M ⊗[R] R) :
      M)

Tactic:
simp [finsuppScalarRight, finsuppRight_apply]

Premises used: TensorProduct.finsuppRight_apply, TensorProduct.finsuppScalarRight