simp_rw [hasSliceRankLE_succ, ih]
case succ
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ HasSliceRankLE (n + 1) f ↔ ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j
case succ
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j