Theorem: HasSliceRankLE.add (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
h₁ : HasSliceRankLE m f₁
⊢ HasSliceRankLE (m + 0) (f₁ + 0)
Tactic:
simpa
State after:
no goals

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
h₁ : HasSliceRankLE m f₁
n✝ : ℕ
f✝ : ((i : ι) → (fun i => α i) i) → R
i✝ : ι
g : α i✝ → R
h : ((j : ι) → j ≠ i✝ → α j) → R
h₂ : HasSliceRankLE n✝ f✝
⊢ HasSliceRankLE (m + (n✝ + 1)) (f₁ + (f✝ + fun x => g (x i✝) * h fun j x_1 => x j))
Tactic:
simpa [add_assoc] using (h₁.add h₂).succ g h
State after:
no goals