Theorem: lengthAdd (Pdl/Setsimp.lean)

State before:
X : Finset Formula
ϕ : Formula
⊢ ϕ ∉ X → lengthOf (insert ϕ X) = lengthOf X + lengthOfFormula ϕ
Tactic:
intro notin
State after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOf (insert ϕ X) = lengthOf X + lengthOfFormula ϕ

State before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOf (insert ϕ X) = lengthOf X + lengthOfFormula ϕ
Tactic:
unfold lengthOf
State after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ setFormulaHasLength.1 (insert ϕ X) = setFormulaHasLength.1 X + lengthOfFormula ϕ

State before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ setFormulaHasLength.1 (insert ϕ X) = setFormulaHasLength.1 X + lengthOfFormula ϕ
Tactic:
simp
State after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (insert ϕ X).sum lengthOfFormula = X.sum lengthOfFormula + lengthOfFormula ϕ

State before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (insert ϕ X).sum lengthOfFormula = X.sum lengthOfFormula + lengthOfFormula ϕ
Tactic:
rw [Finset.sum_insert notin]
State after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x = X.sum lengthOfFormula + lengthOfFormula ϕ

State before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x = X.sum lengthOfFormula + lengthOfFormula ϕ
Tactic:
apply Nat.add_comm
State after:
no goals