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

State before:
α : Type u_1
X Y Z : Language α
⊢ X ∘ₗ Y ∘ₗ Z = X ∘ₗ (Y ∘ₗ Z)
Tactic:
apply Set.ext
State after:
case h
α : Type u_1
X Y Z : Language α
⊢ ∀ (x : Word α), x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)

State before:
case h
α : Type u_1
X Y Z : Language α
⊢ ∀ (x : Word α), x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
intro x
State after:
case h
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)

State before:
case h
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
constructor
State after:
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)

case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z

State before:
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)

case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
. intro
  | ⟨u, v, ⟨u1, u2, pu1, pu2, pu⟩, pv, px⟩ =>
    rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
    exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
State after:
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z

State before:
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
. intro
  | ⟨u, v, pu, ⟨v1, v2, pv1, pv2, pv⟩, px⟩ =>
    rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
    exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
State after:
no goals

State before:
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
intro
| ⟨u, v, ⟨u1, u2, pu1, pu2, pu⟩, pv, px⟩ =>
  rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
  exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
State after:
no goals

State before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u * v
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
State after:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u1 * (u2 * v)
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)

State before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u1 * (u2 * v)
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
State after:
no goals

State before:
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
intro
| ⟨u, v, pu, ⟨v1, v2, pv1, pv2, pv⟩, px⟩ =>
  rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
  exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
State after:
no goals

State before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ (Y ∘ₗ Z)
u v : Word α
pu : u ∈ X
v1 v2 : Word α
pv1 : v1 ∈ Y
pv2 : v2 ∈ Z
pv : v = v1 * v2
px : x = u * v
⊢ x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
State after:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ (Y ∘ₗ Z)
u v : Word α
pu : u ∈ X
v1 v2 : Word α
pv1 : v1 ∈ Y
pv2 : v2 ∈ Z
pv : v = v1 * v2
px : x = u * v1 * v2
⊢ x ∈ X ∘ₗ Y ∘ₗ Z

State before:
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ (Y ∘ₗ Z)
u v : Word α
pu : u ∈ X
v1 v2 : Word α
pv1 : v1 ∈ Y
pv2 : v2 ∈ Z
pv : v = v1 * v2
px : x = u * v1 * v2
⊢ x ∈ X ∘ₗ Y ∘ₗ Z
Tactic:
exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
State after:
no goals