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

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

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

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

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 ∘ₗ L3 ∪ L2 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
. intro
  | ⟨u,v,h1,h2,h3⟩ =>
    cases h1 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 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3

State before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 ⟨Or.inl h1, 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 ⟨Or.inr h1, 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 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
intro
| ⟨u,v,h1,h2,h3⟩ =>
  cases h1 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 ∪ L2
h2 : v ∈ L3
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
Tactic:
cases h1 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 α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ w ∈ L1 ∘ₗ L3

State before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ w ∈ L1 ∘ₗ L3
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 α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ 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 α
h2 : v ∈ L3
h3 : w = u * v
hl : u ∈ L1
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ 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 α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ w ∈ L2 ∘ₗ L3

State before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ (L1 ∪ L2) ∘ₗ L3
u v : Word α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ w ∈ L2 ∘ₗ 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 α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ ∃ v, u ∈ L2 ∧ 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 α
h2 : v ∈ L3
h3 : w = u * v
hr : u ∈ L2
⊢ ∃ v, u ∈ L2 ∧ 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 ∘ₗ L3 ∪ L2 ∘ₗ 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 ⟨Or.inl h1, 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 ⟨Or.inr h1, h2, h3⟩
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
hl : w ∈ L1 ∘ₗ L3
⊢ 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 ⟨Or.inl h1, h2, h3⟩
State after:
no goals

State before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 ⟨Or.inl h1, h2, h3⟩
State after:
no goals

State before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 ⟨Or.inl h1, h2, h3⟩
State after:
no goals

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ 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 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∪ L2 ∧ v ∈ L3 ∧ w = u * v

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

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
hr : w ∈ L2 ∘ₗ 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 ⟨Or.inr h1, h2, h3⟩
State after:
no goals

State before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L2 ∧ 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 ⟨Or.inr h1, h2, h3⟩
State after:
no goals

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

State before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L2
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 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L2
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∪ L2 ∧ v ∈ L3 ∧ w = u * v

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