-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_finsupp_left (x : M ⊗[R] N) :
    ∃ S : M →₀ N, x = S.sum fun m n ↦ m ⊗ₜ[R] n

Proof state:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ∃ S, 0 = S.sum fun m n => m ⊗ₜ[R] n

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ ((Sx.sum fun m n => m ⊗ₜ[R] n) + Sy.sum fun m n => m ⊗ₜ[R] n) = (Sx + Sy).sum fun m n => m ⊗ₜ[R] n

Tactic:
exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ ∀ (a : M), a ⊗ₜ[R] 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case add.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n => m ⊗ₜ[R] n

Tactic:
use Sx + Sy

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ x + y = (Sx + Sy).sum fun m n => m ⊗ₜ[R] n

Proof state:
case tmul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ ∃ S, x ⊗ₜ[R] y = S.sum fun m n => m ⊗ₜ[R] n

Tactic:
exact ⟨Finsupp.single x y, by simp⟩

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ x + y = (Sx + Sy).sum fun m n => m ⊗ₜ[R] n

Tactic:
rw [hx, hy]

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ ((Sx.sum fun m n => m ⊗ₜ[R] n) + Sy.sum fun m n => m ⊗ₜ[R] n) = (Sx + Sy).sum fun m n => m ⊗ₜ[R] n

Proof state:
case add.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
hy : ∃ S, y = S.sum fun m n => m ⊗ₜ[R] n
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n => m ⊗ₜ[R] n

Tactic:
obtain ⟨Sy, hy⟩ := hy

Result:
case add.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n => m ⊗ₜ[R] n

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ ∃ S, x = S.sum fun m n => m ⊗ₜ[R] n

Tactic:
induction x with
| zero => exact ⟨0, by simp⟩
| tmul x y => exact ⟨Finsupp.single x y, by simp⟩
| add x y hx hy =>
  obtain ⟨Sx, hx⟩ := hx
  obtain ⟨Sy, hy⟩ := hy
  use Sx + Sy
  rw [hx, hy]
  exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

Result:
no goals

Proof state:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
hx : ∃ S, x = S.sum fun m n => m ⊗ₜ[R] n
hy : ∃ S, y = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n => m ⊗ₜ[R] n

Tactic:
obtain ⟨Sx, hx⟩ := hx

Result:
case add.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
hy : ∃ S, y = S.sum fun m n => m ⊗ₜ[R] n
Sx : M →₀ N
hx : x = Sx.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n => m ⊗ₜ[R] n

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ 0 = Finsupp.sum 0 fun m n => m ⊗ₜ[R] n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ x ⊗ₜ[R] y = (Finsupp.single x y).sum fun m n => m ⊗ₜ[R] n

Tactic:
simp

Result:
no goals