Theorem: projectionUnion (Bml/Tableau.lean)

State before:
X Y : Finset Formula
⊢ projection (X ∪ Y) = projection X ∪ projection Y
Tactic:
unfold projection
State after:
X Y : Finset Formula
⊢ (let X := X ∪ Y;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := Y;
      X.biUnion fun x => (formProjection x).toFinset

State before:
X Y : Finset Formula
⊢ (let X := X ∪ Y;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := Y;
      X.biUnion fun x => (formProjection x).toFinset
Tactic:
aesop
State after:
no goals