Theorem: TensorProduct.exists_Fin (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✝¹ : CommRing S
inst✝ : Algebra R S
sm : S ⊗[R] M
⊢ ∃ n s m, sm = ∑ i : Fin n, s i ⊗ₜ[R] m i
Tactic:
obtain ⟨m, rfl⟩ := TensorProduct.exists_Finsupp S sm
State after:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i

State before:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i
Tactic:
let e : m.support ≃ Fin (m.support.card) := Finset.equivFin _
State after:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i

State before:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i
Tactic:
use m.support.card, fun i ↦ e.symm i, fun i ↦ m (e.symm i)
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✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)

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✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)
Tactic:
rw [sum, ← Finset.sum_attach]
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✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∑ x ∈ m.support.attach, ↑x ⊗ₜ[R] m ↑x = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)

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✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∑ x ∈ m.support.attach, ↑x ⊗ₜ[R] m ↑x = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)
Tactic:
apply Finset.sum_equiv e <;> simp
State after:
no goals