Theorem: lengthAdd (Bml/Setsimp.lean)

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

State before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ
Tactic:
unfold lengthOfSet
State after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (let X := insert ϕ X;
    X.sum lengthOfFormula) =
    (let X := X;
      X.sum lengthOfFormula) +
      lengthOfFormula ϕ

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

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