Theorem: hasSliceRankLE_succ (LeanCamCombi/SliceRank.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE (n + 1) f ↔ ∃ f' i g h, HasSliceRankLE n f' ∧ f = f' + fun x => g (x i) * h fun j x_1 => x j
Tactic:
rw [hasSliceRankLE_iff]
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (n + 1 = 0 ∧ f = 0 ∨
      ∃ n_1 f_1 i g h, HasSliceRankLE n_1 f_1 ∧ n + 1 = n_1 + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ f' i g h, HasSliceRankLE n f' ∧ f = f' + fun x => g (x i) * h fun j x_1 => x j

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (n + 1 = 0 ∧ f = 0 ∨
      ∃ n_1 f_1 i g h, HasSliceRankLE n_1 f_1 ∧ n + 1 = n_1 + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ f' i g h, HasSliceRankLE n f' ∧ f = f' + fun x => g (x i) * h fun j x_1 => x j
Tactic:
sorry
State after:
no goals