Theorem: TensorProduct.exists_Finsupp (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
μ : S ⊗[R] M
⊢ ∃ m, μ = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
classical
induction μ using TensorProduct.induction_on with
| zero => use 0; simp
| tmul s m => use single s m; simp
| add x y hx hy =>
  obtain ⟨sx, rfl⟩ := hx
  obtain ⟨sy, rfl⟩ := hy
  use sx + sy
  rw [sum_add_index (fun _ ↦ by simp) (fun _ _ _ _ ↦ by rw [TensorProduct.tmul_add])]
State after:
no goals

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
μ : S ⊗[R] M
⊢ ∃ m, μ = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
induction μ using TensorProduct.induction_on with
| zero => use 0; simp
| tmul s m => use single s m; simp
| add x y hx hy =>
  obtain ⟨sx, rfl⟩ := hx
  obtain ⟨sy, rfl⟩ := hy
  use sx + sy
  rw [sum_add_index (fun _ ↦ by simp) (fun _ _ _ _ ↦ by rw [TensorProduct.tmul_add])]
State after:
no goals

State before:
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ ∃ m, 0 = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
use 0
State after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ 0 = sum 0 fun s x => s ⊗ₜ[R] x

State before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ 0 = sum 0 fun s x => s ⊗ₜ[R] x
Tactic:
simp
State after:
no goals

State before:
case tmul
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : S
m : M
⊢ ∃ m_1, s ⊗ₜ[R] m = m_1.sum fun s x => s ⊗ₜ[R] x
Tactic:
use single s m
State after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : S
m : M
⊢ s ⊗ₜ[R] m = (Finsupp.single s m).sum fun s x => s ⊗ₜ[R] x

State before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : S
m : M
⊢ s ⊗ₜ[R] m = (Finsupp.single s m).sum fun s x => s ⊗ₜ[R] x
Tactic:
simp
State after:
no goals

State before:
case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∃ m, x = m.sum fun s x => s ⊗ₜ[R] x
hy : ∃ m, y = m.sum fun s x => s ⊗ₜ[R] x
⊢ ∃ m, x + y = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
obtain ⟨sx, rfl⟩ := hx
State after:
case add.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
y : S ⊗[R] M
hy : ∃ m, y = m.sum fun s x => s ⊗ₜ[R] x
sx : S →₀ M
⊢ ∃ m, (sx.sum fun s x => s ⊗ₜ[R] x) + y = m.sum fun s x => s ⊗ₜ[R] x

State before:
case add.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
y : S ⊗[R] M
hy : ∃ m, y = m.sum fun s x => s ⊗ₜ[R] x
sx : S →₀ M
⊢ ∃ m, (sx.sum fun s x => s ⊗ₜ[R] x) + y = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
obtain ⟨sy, rfl⟩ := hy
State after:
case add.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ∃ m, ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = m.sum fun s x => s ⊗ₜ[R] x

State before:
case add.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ∃ m, ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
use sx + sy
State after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = (sx + sy).sum fun s x => s ⊗ₜ[R] x

State before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = (sx + sy).sum fun s x => s ⊗ₜ[R] x
Tactic:
rw [sum_add_index (fun _ ↦ by simp) (fun _ _ _ _ ↦ by rw [TensorProduct.tmul_add])]
State after:
no goals

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
x✝ : S
⊢ x✝ ∈ sx.support ∪ sy.support → x✝ ⊗ₜ[R] 0 = 0
Tactic:
simp
State after:
no goals

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
x✝³ : S
x✝² : x✝³ ∈ sx.support ∪ sy.support
x✝¹ x✝ : M
⊢ x✝³ ⊗ₜ[R] (x✝¹ + x✝) = x✝³ ⊗ₜ[R] x✝¹ + x✝³ ⊗ₜ[R] x✝
Tactic:
rw [TensorProduct.tmul_add]
State after:
no goals