refine ⟨_, i 0, g 0, h 0, ⟨Fin.tail i, Fin.tail g, Fin.tail h, rfl⟩, ?_⟩
case succ.mpr.intro.intro.intro
ι : 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 : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
⊢ ∃ f' i_1 g_1 h_1,
    (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
      (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) =
        f' + fun x => g_1 (x i_1) * h_1 fun j x_1 => x j
case succ.mpr.intro.intro.intro
ι : 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 : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
⊢ (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) =
    (∑ k : Fin n, fun x => Fin.tail g k (x (Fin.tail i k)) * Fin.tail h k fun j x_1 => x j) + fun x =>
      g 0 (x (i 0)) * h 0 fun j x_1 => x j