Theorem: Languages.thm_3_d (FOL/Parsing/Text.lean)

State before:
α : Type
L1 L2 L3 : Language α
⊢ concat L1 (L2 ∪ L3) = concat L1 L2 ∪ concat L1 L3
Tactic:
simp only [concat]
State after:
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ L2 ∪ L3, s ++ t = x} =
    {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x} ∪ {x | ∃ s ∈ L1, ∃ t ∈ L3, s ++ t = x}

State before:
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ L2 ∪ L3, s ++ t = x} =
    {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x} ∪ {x | ∃ s ∈ L1, ∃ t ∈ L3, s ++ t = x}
Tactic:
aesop
State after:
no goals