simp only [ne_eq, Pi.add_apply, Finset.sum_apply, add_comm (_ * _), Fin.sum_univ_succ,
  Fin.cons_zero, Fin.cons_succ]
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro.h
ι : 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
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) x =
    (∑ k : Fin (n + 1), fun x => Fin.cons gₙ g k (x (Fin.cons iₙ i k)) * Fin.cons hₙ h k fun j x_1 => x j) x
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro.h
ι : 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
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ c : Fin n, g c (x (i c)) * h c fun j x_1 => x j) + gₙ (x iₙ) * hₙ fun j x_1 => x j) =
    (∑ x_1 : Fin n, g x_1 (x (Fin.cons iₙ i x_1.succ)) * h x_1 fun j x_2 => x j) +
      gₙ (x (Fin.cons iₙ i 0)) * hₙ fun j x_1 => x j