Theorem: lengthOf_insert_leq_plus (Pdl/Setsimp.lean)

State before:
X : Finset Formula
ϕ : Formula
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
cases' em (ϕ ∈ X) with in_x not_in_x
State after:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ

case inr
X : Finset Formula
ϕ : Formula
not_in_x : ϕ ∉ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ

State before:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
rw [Finset.insert_eq_of_mem in_x]
State after:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf X ≤ lengthOf X + lengthOfFormula ϕ

State before:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf X ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
simp
State after:
no goals

State before:
case inr
X : Finset Formula
ϕ : Formula
not_in_x : ϕ ∉ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
rw [lengthAdd not_in_x]
State after:
no goals