-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_multiset (x : M ⊗[R] N) :
    ∃ S : Multiset (M × N), x = (S.map fun i ↦ i.1 ⊗ₜ[R] i.2).sum

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) 0).sum

Tactic:
simp

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
hy : ∃ S, y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
⊢ ∃ S, x + y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sx).sum
⊢ ∃ S, x + y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

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 : Multiset (M × N)
hx : x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ x + y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) (Sx + Sy)).sum

Tactic:
rw [Multiset.map_add, Multiset.sum_add, hx, hy]

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 : Multiset (M × N)
hx : x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ ∃ S, x + y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) {(x, y)}).sum

Tactic:
simp

Result:
no goals

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
exact ⟨0, by 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 ⊗[R] N
⊢ ∃ S, x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
induction x with
| zero => exact ⟨0, by simp⟩
| tmul x y => exact ⟨{(x, y)}, by simp⟩
| add x y hx hy =>
  obtain ⟨Sx, hx⟩ := hx
  obtain ⟨Sy, hy⟩ := hy
  exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩

Result:
no goals

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sx).sum
⊢ ∃ S, x + y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

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 : Multiset (M × N)
hx : x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ ∃ S, x + y = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

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 = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
exact ⟨{(x, y)}, by simp⟩

Result:
no goals