simp [hasSliceRankLE_succ]
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE 1 f ↔ ∃ i g h, f = fun x => g (x i) * h fun j x_1 => x j
no goals