rw [hasSliceRankLE_iff_exists_sum]
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Fintype (α i)
f : ((i : ι) → α i) → R
⊢ HasSliceRankLE (Fintype.card ((i : ι) → α i)) f
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Fintype (α i)
f : ((i : ι) → α i) → R
⊢ ∃ i g h, f = ∑ k : Fin (Fintype.card ((i : ι) → α i)), fun x => g k (x (i k)) * h k fun j x_1 => x j