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
ι : Type u_5
inst_7 : DecidableEq ι
i : ι
m : M
⊢ Eq (α := M ⊗[R] (ι →₀ R))
    (((LinearEquiv.symm (finsuppScalarRight R S M ι) : (ι →₀ M) ≃ₗ[S] M ⊗[R] (ι →₀ R)) : (a : ι →₀ M) → M ⊗[R] (ι →₀ R))
        (Finsupp.single i m) :
      M ⊗[R] (ι →₀ R))
    (m ⊗ₜ[R] Finsupp.single i 1 : M ⊗[R] (ι →₀ R))

Tactic:
simp [finsuppScalarRight, finsuppRight_symm_apply_single]

Premises used: TensorProduct.finsuppRight_symm_apply_single, 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 ι
s : S
t : M ⊗[R] (ι →₀ R)
⊢ ((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (s • t) =
    HSMul.hSMul (β := ι →₀ M) s
      (((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) t : ι →₀ 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 ι
⊢ Eq (α := (a : M ⊗[R] (ι →₀ R)) → ι →₀ M)
    (⇑(finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M)
    (⇑(finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : DecidableEq ι
v : ι → M
h :
  ∀ (a : ι) (x : S),
    Eq (α := S ⊗[R] M)
      (((↑R :
                  {S : Type u_2} →
                    {M : Type (max u_2 u_5)} →
                      {M₂ : Type (max u_2 u_3)} →
                        [inst : Semiring R] →
                          [inst_6 : Semiring S] →
                            [inst_7 : AddCommMonoid M] →
                              [inst_8 : AddCommMonoid M₂] →
                                [inst_9 : Module R M] →
                                  [inst_10 : Module R M₂] →
                                    [inst_11 : Module S M] →
                                      [inst_12 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (linearCombination S fun (x : ι) ↦ 1 ⊗ₜ[R] v x) ∘ₗ
              lsingle a :
            (a : S) → S ⊗[R] M)
          x :
        S ⊗[R] M)
      (((lTensor S (linearCombination R v) ∘ₗ
                (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) ∘ₗ
              lsingle a :
            (a : S) → S ⊗[R] M)
          x :
        S ⊗[R] M)
⊢ Eq (α := (ι →₀ S) →ₗ[R] S ⊗[R] M)
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_2 u_5)} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (linearCombination S fun (x : ι) ↦ 1 ⊗ₜ[R] v x))
    (lTensor S (linearCombination R v) ∘ₗ
      (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R)))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : DecidableEq ι
v : ι → M
a : ι
x : S
⊢ Eq (α := S ⊗[R] M)
    (((↑R :
                {S : Type u_2} →
                  {M : Type (max u_2 u_5)} →
                    {M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (linearCombination S fun (x : ι) ↦ 1 ⊗ₜ[R] v x) ∘ₗ
            lsingle a :
          (a : S) → S ⊗[R] M)
        x :
      S ⊗[R] M)
    (((lTensor S (linearCombination R v) ∘ₗ
              (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) ∘ₗ
            lsingle a :
          (a : S) → S ⊗[R] M)
        x :
      S ⊗[R] M)

Tactic:
simp [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
m : M
k : κ
n : N
⊢ Eq (α := ι × κ →₀ M ⊗[R] N)
    (((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
          (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
        (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) :
      ι × κ →₀ M ⊗[R] N)
    (Finsupp.single (i, k) (m ⊗ₜ[R] n) : ι × κ →₀ M ⊗[R] N)

Tactic:
simp [finsuppTensorFinsupp]

Premises used: finsuppTensorFinsupp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
g : κ →₀ N
i : ι
k : κ
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (0 ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((0 : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
g : κ →₀ N
i : ι
k : κ
f₁ f₂ : ι →₀ M
hf₁ :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (f₁ ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f₁ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
hf₂ :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (f₂ ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f₂ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              ((f₁ + f₂) ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f₁ + f₂ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)

Tactic:
simp [add_tmul, hf₁, hf₂]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] 0) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (0 : (a : κ) → N) k : M ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
g₁ g₂ : κ →₀ N
hg₁ :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] g₁) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₁ : (a : κ) → N) k : M ⊗[R] N)
hg₂ :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] g₂) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₂ : (a : κ) → N) k : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] (g₁ + g₂)) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₁ + g₂ : (a : κ) → N) k : M ⊗[R] N)

Tactic:
simp [tmul_add, hg₁, hg₂]

Premises used: TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
single :
  Eq (α := M ⊗[R] N) (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (Finsupp.single k' n : (a : κ) → N) k : M ⊗[R] N)

Tactic:
simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]

Premises used: Prod.mk_inj, finsuppTensorFinsupp_single, Finsupp.single_apply, ite_and
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
pos : i' = i → k' = k → Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
neg : i' = i → ¬k' = k → Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] 0)
pos₁ : ¬i' = i → k' = k → Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] n)
neg₁ : ¬i' = i → ¬k' = k → Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)
⊢ Eq (α := M ⊗[R] N) (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)

Tactic:
split_ifs
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h : i' = i
h_1 : k' = k
⊢ Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h : i' = i
h_1 : ¬k' = k
⊢ Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h : ¬i' = i
h_1 : k' = k
⊢ Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] n)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h : ¬i' = i
h_1 : ¬k' = k
⊢ Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
single :
  Eq (α := M ⊗[R] N) ((Finsupp.single (i', k') (m ⊗ₜ[R] n) : (a : ι × κ) → M ⊗[R] N) (i, k) : M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (Finsupp.single k' n : (a : κ) → N) k : M ⊗[R] N)
single₁ :
  Eq (α := M ⊗[R] N) (if (i', k') = (i, k) then m ⊗ₜ[R] n else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
single₂ :
  Eq (α := M ⊗[R] N) (if i' = i ∧ k' = k then m ⊗ₜ[R] n else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
single₃ :
  Eq (α := M ⊗[R] N) (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (Finsupp.single k' n : (a : κ) → N) k : M ⊗[R] N)

Tactic:
classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp

Premises used: Prod.mk_inj, finsuppTensorFinsupp_single, Finsupp.single_apply, ite_and
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι × κ
m : M
n : N
⊢ Eq (α := (ι →₀ M) ⊗[R] (κ →₀ N))
    (((LinearEquiv.symm (finsuppTensorFinsupp 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))
    (Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 n : (ι →₀ M) ⊗[R] (κ →₀ N))

Tactic:
Prod.casesOn i fun _ _ =>
    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsupp_single _ _ _ _ _ _ _ _ _ _).symm

Premises used: Prod.casesOn
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
f : ι →₀ R
g : κ →₀ N
a : ι
b : κ
⊢ (((finsuppTensorFinsuppLid R N ι κ : (a : (ι →₀ R) ⊗[R] (κ →₀ N)) → ι × κ →₀ N) (f ⊗ₜ[R] g) : ι × κ →₀ N) :
        (a : ι × κ) → N)
      (a, b) =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := N) ((f : (a : ι) → R) a : R) ((g : (a : κ) → N) b : N)

Tactic:
simp [finsuppTensorFinsuppLid]

Premises used: finsuppTensorFinsuppLid
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
a : ι
b : κ
r : R
n : N
⊢ Eq (α := ι × κ →₀ N)
    ((finsuppTensorFinsuppLid R N ι κ : (a : (ι →₀ R) ⊗[R] (κ →₀ N)) → ι × κ →₀ N)
        (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) :
      ι × κ →₀ N)
    (Finsupp.single (a, b) (r • n) : ι × κ →₀ N)

Tactic:
simp [finsuppTensorFinsuppLid]

Premises used: finsuppTensorFinsuppLid
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
i : ι × κ
r : R
n : N
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ N))
    ((LinearEquiv.symm (finsuppTensorFinsuppLid R N ι κ) : (a : ι × κ →₀ N) → (ι →₀ R) ⊗[R] (κ →₀ N))
        (Finsupp.single i (r • n)) :
      (ι →₀ R) ⊗[R] (κ →₀ N))
    (Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 n : (ι →₀ R) ⊗[R] (κ →₀ N))

Tactic:
Prod.casesOn i fun _ _ =>
    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppLid_single_tmul_single ..).symm

Premises used: Prod.casesOn
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι →₀ M
g : κ →₀ R
a : ι
b : κ
⊢ (((finsuppTensorFinsuppRid R M ι κ : (a : (ι →₀ M) ⊗[R] (κ →₀ R)) → ι × κ →₀ M) (f ⊗ₜ[R] g) : ι × κ →₀ M) :
        (a : ι × κ) → M)
      (a, b) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((g : (a : κ) → R) b : R) ((f : (a : ι) → M) a : M)

Tactic:
simp [finsuppTensorFinsuppRid]

Premises used: finsuppTensorFinsuppRid
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : ι
b : κ
m : M
r : R
⊢ Eq (α := ι × κ →₀ M)
    ((finsuppTensorFinsuppRid R M ι κ : (a : (ι →₀ M) ⊗[R] (κ →₀ R)) → ι × κ →₀ M)
        (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) :
      ι × κ →₀ M)
    (Finsupp.single (a, b) (r • m) : ι × κ →₀ M)

Tactic:
simp [finsuppTensorFinsuppRid]

Premises used: finsuppTensorFinsuppRid
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ι × κ
m : M
r : R
⊢ Eq (α := (ι →₀ M) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsuppRid R M ι κ) : (a : ι × κ →₀ M) → (ι →₀ M) ⊗[R] (κ →₀ R))
        (Finsupp.single i (r • m)) :
      (ι →₀ M) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ M) ⊗[R] (κ →₀ R))

Tactic:
Prod.casesOn i fun _ _ =>
    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppRid_single_tmul_single ..).symm

Premises used: Prod.casesOn
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
f : ι →₀ R
g : κ →₀ R
a : ι
b : κ
⊢ (((finsuppTensorFinsupp' R ι κ : (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → ι × κ →₀ R) (f ⊗ₜ[R] g) : ι × κ →₀ R) :
        (a : ι × κ) → R)
      (a, b) =
    HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) a : R) ((g : (a : κ) → R) b : R)

Tactic:
finsuppTensorFinsuppLid_apply_apply R R ι κ f g a b

Premises used: finsuppTensorFinsuppLid_apply_apply
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
a : ι
b : κ
r₁ r₂ : R
⊢ Eq (α := ι × κ →₀ R)
    ((finsuppTensorFinsupp' R ι κ : (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → ι × κ →₀ R)
        (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) :
      ι × κ →₀ R)
    (Finsupp.single (a, b) (r₁ * r₂) : ι × κ →₀ R)

Tactic:
finsuppTensorFinsuppLid_single_tmul_single R R ι κ a b r₁ r₂

Premises used: finsuppTensorFinsuppLid_single_tmul_single
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r₁ r₂ : R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (r₁ * r₂)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 r₁ ⊗ₜ[R] Finsupp.single i.2 r₂ : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
finsuppTensorFinsuppLid_symm_single_smul R R ι κ i r₁ r₂

Premises used: finsuppTensorFinsuppLid_symm_single_smul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r : R
nth_rw :
  Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (1 * r)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ R) ⊗[R] (κ →₀ R))
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)) (Finsupp.single i r) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
nth_rw 1 [← one_mul r]

Premises used: one_mul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r : R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (1 * r)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Premises used: finsuppTensorFinsupp'_symm_single_mul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r : R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (1 * r)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Premises used: finsuppTensorFinsupp'_symm_single_mul