Theorem: lengthOf_insert_leq_plus (Bml/Setsimp.lean)

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

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

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

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

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