Theorem: Language.concat_dist_union_l (FormalSystems/Preliminaries/Language.lean)

State before:
α : Type u_1
L1 L2 L3 : Language α
⊢ L1 ∘ₗ (L2 ∪ L3) = L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
apply Set.ext
State after:
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ L1 ∘ₗ (L2 ∪ L3) ↔ x ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3

State before:
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ L1 ∘ₗ (L2 ∪ L3) ↔ x ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
intro w
State after:
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) ↔ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3

State before:
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) ↔ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
constructor
State after:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)

State before:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
. intro
  | ⟨u,v,h1,h2,h3⟩ =>
    cases h2 with
    | inl hl => apply Or.inl; exists u; exists v
    | inr hr => apply Or.inr; exists u; exists v
State after:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)

State before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
. intro
  | Or.inl hl => cases hl with | intro u pu => cases pu with | intro v pv =>
      match pv with
      | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
  | Or.inr hr => cases hr with | intro u pu => cases pu with | intro v pv =>
      match pv with
      | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
State after:
no goals

State before:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
intro
| ⟨u,v,h1,h2,h3⟩ =>
  cases h2 with
  | inl hl => apply Or.inl; exists u; exists v
  | inr hr => apply Or.inr; exists u; exists v
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h2 : v ∈ L2 ∪ L3
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
cases h2 with
| inl hl => apply Or.inl; exists u; exists v
| inr hr => apply Or.inr; exists u; exists v
State after:
no goals

State before:
case inl
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
apply Or.inl
State after:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ w ∈ L1 ∘ₗ L2

State before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ w ∈ L1 ∘ₗ L2
Tactic:
exists u
State after:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ ∃ v, u ∈ L1 ∧ v ∈ L2 ∧ w = u * v

State before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ ∃ v, u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
Tactic:
exists v
State after:
no goals

State before:
case inr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
apply Or.inr
State after:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ w ∈ L1 ∘ₗ L3

State before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ w ∈ L1 ∘ₗ L3
Tactic:
exists u
State after:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v

State before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
Tactic:
exists v
State after:
no goals

State before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
intro
| Or.inl hl => cases hl with | intro u pu => cases pu with | intro v pv =>
    match pv with
    | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
| Or.inr hr => cases hr with | intro u pu => cases pu with | intro v pv =>
    match pv with
    | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
hl : w ∈ L1 ∘ₗ L2
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases hl with | intro u pu => cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
State after:
no goals

State before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
State after:
no goals

State before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
exists u, v
State after:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v
Tactic:
exact ⟨h1, Or.inl h2, h3⟩
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
hr : w ∈ L1 ∘ₗ L3
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases hr with | intro u pu => cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
State after:
no goals

State before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
State after:
no goals

State before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
exists u, v
State after:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v
Tactic:
exact ⟨h1, Or.inr h2, h3⟩
State after:
no goals