Theorem: hasSliceRankLE_zero (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 0 f ↔ f = 0
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
⊢ (0 = 0 ∧ f = 0 ∨ ∃ n f_1 i g h, HasSliceRankLE n f_1 ∧ 0 = n + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    f = 0

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
⊢ (0 = 0 ∧ f = 0 ∨ ∃ n f_1 i g h, HasSliceRankLE n f_1 ∧ 0 = n + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    f = 0
Tactic:
simp [@eq_comm _ 0]
State after:
no goals