awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
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 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : AddCommMonoid N
inst_8 : Module R N
b : Basis ι S M
c : Basis κ R N
i : ι × κ
⊢ Eq (α := M ⊗[R] N) (((b.tensorProduct c : Basis (ι × κ) S (M ⊗[R] N)) : (a : ι × κ) → M ⊗[R] N) i : M ⊗[R] N)
    ((b : (a : ι) → M) i.1 ⊗ₜ[R] (c : (a : κ) → N) i.2 : M ⊗[R] N)

Tactic:
simp [tensorProduct]

Premises used: Module.Basis.tensorProduct
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
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 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : AddCommMonoid N
inst_8 : Module R N
b : Basis ι S M
c : Basis κ R N
m : M
n : N
i : ι
j : κ
⊢ ((((repr (b.tensorProduct c) : M ⊗[R] N ≃ₗ[S] ι × κ →₀ S) : (a : M ⊗[R] N) → ι × κ →₀ S) (m ⊗ₜ[R] n) : ι × κ →₀ S) :
        (a : ι × κ) → S)
      (i, j) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((c.repr : (a : N) → κ →₀ R) n : κ →₀ R) : (a : κ) → R) j : R)
      ((((b.repr : (a : M) → ι →₀ S) m : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
simp [tensorProduct]

Premises used: Module.Basis.tensorProduct
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
inst_3 : Semiring S
inst_4 : Algebra R S
b : Basis ι R M
x : S
y : M
i : ι
⊢ (((repr (baseChange S b) : (a : S ⊗[R] M) → ι →₀ S) (x ⊗ₜ[R] y) : ι →₀ S) : (a : ι) → S) i =
    HSMul.hSMul.{u_1, u_7, u_7} (α := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R) x

Tactic:
simp [baseChange, tensorProduct]

Premises used: Module.Basis.baseChange, Module.Basis.tensorProduct
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
inst_3 : Semiring S
inst_4 : Algebra R S
b : Basis ι R M
i : ι
⊢ Eq (α := S ⊗[R] M) ((baseChange S b : (a : ι) → S ⊗[R] M) i : S ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) i : S ⊗[R] M)

Tactic:
simp [baseChange, tensorProduct]

Premises used: Module.Basis.baseChange, Module.Basis.tensorProduct
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
h :
  ∀ (a : κ),
    Eq.{u_3 + 1} (α := M)
      ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (m ⊗ₜ[R] n) : κ →₀ M) : (a : κ) → M) a : M)
      ((Finsupp.mapRange (fun (x : R) ↦ x • m) ⋯ ((𝒞.repr : (a : N) → κ →₀ R) n) : (a : κ) → M) a : M)
⊢ Eq (α := κ →₀ M) ((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (m ⊗ₜ[R] n) : κ →₀ M)
    (Finsupp.mapRange (fun (x : R) ↦ x • m) ⋯ ((𝒞.repr : (a : N) → κ →₀ R) n) : κ →₀ M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
a : κ
⊢ Eq.{u_3 + 1} (α := M)
    ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (m ⊗ₜ[R] n) : κ →₀ M) : (a : κ) → M) a : M)
    ((Finsupp.mapRange (fun (x : R) ↦ x • m) ⋯ ((𝒞.repr : (a : N) → κ →₀ R) n) : (a : κ) → M) a : M)

Tactic:
simp [equivFinsuppOfBasisRight]

Premises used: TensorProduct.equivFinsuppOfBasisRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
i : κ
⊢ (((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (m ⊗ₜ[R] n) : κ →₀ M) : (a : κ) → M) i =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((((𝒞.repr : (a : N) → κ →₀ R) n : κ →₀ R) : (a : κ) → R) i : R) m

Tactic:
simp only [equivFinsuppOfBasisRight_apply_tmul, Finsupp.mapRange_apply]

Premises used: Finsupp.mapRange_apply, TensorProduct.equivFinsuppOfBasisRight_apply_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
h :
  ∀ (a : κ) (x : M),
    Eq (α := M ⊗[R] N)
      (((↑(LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞)) : (κ →₀ M) →ₗ[R] M ⊗[R] N) ∘ₗ Finsupp.lsingle a :
            (a : M) → M ⊗[R] N)
          x :
        M ⊗[R] N)
      ((((Finsupp.lsum R : (a : κ → M →ₗ[R] M ⊗[R] N) → (κ →₀ M) →ₗ[R] M ⊗[R] N) fun (i : κ) ↦
                (LinearMap.flip (mk R M N) : (a : N) → M →ₗ[R] M ⊗[R] N) ((𝒞 : (a : κ) → N) i)) ∘ₗ
              Finsupp.lsingle a :
            (a : M) → M ⊗[R] N)
          x :
        M ⊗[R] N)
⊢ Eq (α := (κ →₀ M) →ₗ[R] M ⊗[R] N) (↑(LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞)) : (κ →₀ M) →ₗ[R] M ⊗[R] N)
    ((Finsupp.lsum R : (a : κ → M →ₗ[R] M ⊗[R] N) → (κ →₀ M) →ₗ[R] M ⊗[R] N) fun (i : κ) ↦
      (LinearMap.flip (mk R M N) : (a : N) → M →ₗ[R] M ⊗[R] N) ((𝒞 : (a : κ) → N) i))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
a : κ
x : M
⊢ Eq (α := M ⊗[R] N)
    (((↑(LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞)) : (κ →₀ M) →ₗ[R] M ⊗[R] N) ∘ₗ Finsupp.lsingle a :
          (a : M) → M ⊗[R] N)
        x :
      M ⊗[R] N)
    ((((Finsupp.lsum R : (a : κ → M →ₗ[R] M ⊗[R] N) → (κ →₀ M) →ₗ[R] M ⊗[R] N) fun (i : κ) ↦
              (LinearMap.flip (mk R M N) : (a : N) → M →ₗ[R] M ⊗[R] N) ((𝒞 : (a : κ) → N) i)) ∘ₗ
            Finsupp.lsingle a :
          (a : M) → M ⊗[R] N)
        x :
      M ⊗[R] N)

Tactic:
simp [equivFinsuppOfBasisRight]

Premises used: TensorProduct.equivFinsuppOfBasisRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
b : κ →₀ M
⊢ Eq (α := M ⊗[R] N) ((LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞) : (a : κ →₀ M) → M ⊗[R] N) b : M ⊗[R] N)
    (b.sum fun (i : κ) (m : M) ↦ m ⊗ₜ[R] (𝒞 : (a : κ) → N) i : M ⊗[R] N)

Tactic:
congr($(TensorProduct.equivFinsuppOfBasisRight_symm 𝒞) b)

Premises used: congrArg, id, TensorProduct.equivFinsuppOfBasisRight_symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
𝒞 : Basis κ R N
⊢ Function.Injective (α := κ →₀ M) (β := M ⊗[R] N)
    (⇑((Finsupp.lsum R : (a : κ → M →ₗ[R] M ⊗[R] N) → (κ →₀ M) →ₗ[R] M ⊗[R] N) fun (i : κ) ↦
          (LinearMap.flip (mk R M N) : (a : N) → M →ₗ[R] M ⊗[R] N) ((𝒞 : (a : κ) → N) i)) :
      (a : κ →₀ M) → M ⊗[R] N)

Tactic:
have := Classical.decEq κ
  (equivFinsuppOfBasisRight_symm (M := M) 𝒞).symm ▸
    (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.injective

Premises used: LinearEquiv.symm, Eq.rec, TensorProduct.equivFinsuppOfBasisRight, TensorProduct.equivFinsuppOfBasisRight_symm, LinearEquiv.injective, Eq.symm, Classical.decEq
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
𝒞 : Basis κ R N
b : κ →₀ M
h : Eq (α := M ⊗[R] N) (b.sum fun (i : κ) (m : M) ↦ m ⊗ₜ[R] (𝒞 : (a : κ) → N) i) 0
this : DecidableEq κ
⊢ Eq (α := M ⊗[R] N) ((LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞) : (a : κ →₀ M) → M ⊗[R] N) b : M ⊗[R] N)
    ((LinearEquiv.symm (equivFinsuppOfBasisRight 𝒞) : (a : κ →₀ M) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
⊢ Eq (α := ι →₀ N) ((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (m ⊗ₜ[R] n) : ι →₀ N)
    (Finsupp.mapRange (fun (x : R) ↦ x • n) ⋯ ((ℬ.repr : (a : M) → ι →₀ R) m) : ι →₀ N)

Tactic:
simp [equivFinsuppOfBasisLeft]

Premises used: TensorProduct.equivFinsuppOfBasisLeft
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
i : ι
⊢ (((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (m ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((((ℬ.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R) n

Tactic:
simp only [equivFinsuppOfBasisLeft_apply_tmul, Finsupp.mapRange_apply]

Premises used: Finsupp.mapRange_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
x : M ⊗[R] N
i : κ
zero :
  Eq.{u_3 + 1} (α := M) (((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) 0 : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) 0) : M)
tmul :
  ∀ (x : M) (y : N),
    Eq.{u_3 + 1} (α := M)
      ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x ⊗ₜ[R] y) : κ →₀ M) : (a : κ) → M) i : M)
      ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
          ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x ⊗ₜ[R] y) : M ⊗[R] R) :
        M)
add :
  ∀ (x y : M ⊗[R] N),
    Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
        ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
            ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
          M) →
      Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) y : κ →₀ M) : (a : κ) → M) i : M)
          ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
              ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) y : M ⊗[R] R) :
            M) →
        Eq.{u_3 + 1} (α := M)
          ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x + y) : κ →₀ M) : (a : κ) → M) i : M)
          ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
              ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x + y) : M ⊗[R] R) :
            M)
⊢ Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
      M)

Tactic:
induction x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
i : κ
⊢ Eq.{u_3 + 1} (α := M) (((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) 0 : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) 0) : M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x : M
y : N
⊢ Eq.{u_3 + 1} (α := M)
    ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x ⊗ₜ[R] y) : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
        ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x ⊗ₜ[R] y) : M ⊗[R] R) :
      M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : 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 : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x y : M ⊗[R] N
h :
  Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) x : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) x : M ⊗[R] R) :
      M)
h_1 :
  Eq.{u_3 + 1} (α := M) ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) y : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M) ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) y : M ⊗[R] R) :
      M)
⊢ Eq.{u_3 + 1} (α := M)
    ((((equivFinsuppOfBasisRight 𝒞 : (a : M ⊗[R] N) → κ →₀ M) (x + y) : κ →₀ M) : (a : κ) → M) i : M)
    ((TensorProduct.rid R M : (a : M ⊗[R] R) → M)
        ((lTensor M (𝒞.coord i) : (a : M ⊗[R] N) → M ⊗[R] R) (x + y) : M ⊗[R] R) :
      M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
x : M ⊗[R] N
i : ι
zero :
  Eq.{u_4 + 1} (α := N) (((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) 0 : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) 0) : N)
tmul :
  ∀ (x : M) (y : N),
    Eq.{u_4 + 1} (α := N)
      ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x ⊗ₜ[R] y) : ι →₀ N) : (a : ι) → N) i : N)
      ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
          ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x ⊗ₜ[R] y) : R ⊗[R] N) :
        N)
add :
  ∀ (x y : M ⊗[R] N),
    Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
        ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
            ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
          N) →
      Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) y : ι →₀ N) : (a : ι) → N) i : N)
          ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
              ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) y : R ⊗[R] N) :
            N) →
        Eq.{u_4 + 1} (α := N)
          ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x + y) : ι →₀ N) : (a : ι) → N) i : N)
          ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
              ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x + y) : R ⊗[R] N) :
            N)
⊢ Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
      N)

Tactic:
induction x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
i : ι
⊢ Eq.{u_4 + 1} (α := N) (((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) 0 : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) 0) : N)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
i : ι
x : M
y : N
⊢ Eq.{u_4 + 1} (α := N)
    ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x ⊗ₜ[R] y) : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
        ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x ⊗ₜ[R] y) : R ⊗[R] N) :
      N)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
i : ι
x y : M ⊗[R] N
h :
  Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) x : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) x : R ⊗[R] N) :
      N)
h_1 :
  Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) y : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N) ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) y : R ⊗[R] N) :
      N)
⊢ Eq.{u_4 + 1} (α := N) ((((equivFinsuppOfBasisLeft ℬ : (a : M ⊗[R] N) → ι →₀ N) (x + y) : ι →₀ N) : (a : ι) → N) i : N)
    ((TensorProduct.lid R N : (a : R ⊗[R] N) → N)
        ((rTensor N (ℬ.coord i) : (a : M ⊗[R] N) → R ⊗[R] N) (x + y) : R ⊗[R] N) :
      N)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
h :
  ∀ (a : ι) (x : N),
    Eq (α := M ⊗[R] N)
      (((↑(LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ)) : (ι →₀ N) →ₗ[R] M ⊗[R] N) ∘ₗ Finsupp.lsingle a :
            (a : N) → M ⊗[R] N)
          x :
        M ⊗[R] N)
      ((((Finsupp.lsum R : (a : ι → N →ₗ[R] M ⊗[R] N) → (ι →₀ N) →ₗ[R] M ⊗[R] N) fun (i : ι) ↦
                (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) ((ℬ : (a : ι) → M) i)) ∘ₗ
              Finsupp.lsingle a :
            (a : N) → M ⊗[R] N)
          x :
        M ⊗[R] N)
⊢ Eq (α := (ι →₀ N) →ₗ[R] M ⊗[R] N) (↑(LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ)) : (ι →₀ N) →ₗ[R] M ⊗[R] N)
    ((Finsupp.lsum R : (a : ι → N →ₗ[R] M ⊗[R] N) → (ι →₀ N) →ₗ[R] M ⊗[R] N) fun (i : ι) ↦
      (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) ((ℬ : (a : ι) → M) i))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
a : ι
x : N
⊢ Eq (α := M ⊗[R] N)
    (((↑(LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ)) : (ι →₀ N) →ₗ[R] M ⊗[R] N) ∘ₗ Finsupp.lsingle a :
          (a : N) → M ⊗[R] N)
        x :
      M ⊗[R] N)
    ((((Finsupp.lsum R : (a : ι → N →ₗ[R] M ⊗[R] N) → (ι →₀ N) →ₗ[R] M ⊗[R] N) fun (i : ι) ↦
              (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) ((ℬ : (a : ι) → M) i)) ∘ₗ
            Finsupp.lsingle a :
          (a : N) → M ⊗[R] N)
        x :
      M ⊗[R] N)

Tactic:
simp [equivFinsuppOfBasisLeft]

Premises used: TensorProduct.equivFinsuppOfBasisLeft
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
ℬ : Basis ι R M
b : ι →₀ N
⊢ Eq (α := M ⊗[R] N) ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) b : M ⊗[R] N)
    (b.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)

Tactic:
congr($(TensorProduct.equivFinsuppOfBasisLeft_symm ℬ) b)

Premises used: congrArg, TensorProduct.equivFinsuppOfBasisLeft_symm, id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ (b : κ →₀ M), (b.sum fun (i : κ) (m : M) ↦ m ⊗ₜ[R] (𝒞 : (a : κ) → N) i) = x

Tactic:
simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

Premises used: LinearEquiv.symm, LinearEquiv.surjective, TensorProduct.equivFinsuppOfBasisRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ (b : κ →₀ M), (b.sum fun (i : κ) (m : M) ↦ m ⊗ₜ[R] (𝒞 : (a : κ) → N) i) = x

Tactic:
classical simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
obtain :
  ∀ (c : ι →₀ N),
    ∃ (c_1 : ι →₀ N),
      Eq (α := M ⊗[R] N) (c_1.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
        ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) c : M ⊗[R] N)
⊢ ∃ (c : ι →₀ N), (c.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n) = x

Tactic:
obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x

Premises used: LinearEquiv.symm, LinearEquiv.surjective, TensorProduct.equivFinsuppOfBasisLeft, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
classical :
  ∀ (c : ι →₀ N),
    ∃ (c_1 : ι →₀ N),
      Eq (α := M ⊗[R] N) (c_1.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
        ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) c : M ⊗[R] N)
⊢ ∃ (c : ι →₀ N), (c.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n) = x

Tactic:
classical obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ Eq (α := N ⊗[R] M)
    ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (c.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n) :
      N ⊗[R] M)
    ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M)
        ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) c) :
      N ⊗[R] M)

Tactic:
simp [Finsupp.sum]

Premises used: Finsupp.sum
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basis
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ ∃ (c_1 : ι →₀ N),
    Eq (α := M ⊗[R] N) (c_1.sum fun (i : ι) (n : N) ↦ (ℬ : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
      ((LinearEquiv.symm (equivFinsuppOfBasisLeft ℬ) : (a : ι →₀ N) → M ⊗[R] N) c : M ⊗[R] N)

Tactic:
exact ⟨c, (TensorProduct.comm R M N).injective <| by simp [Finsupp.sum]⟩