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

State before:
α : Type u_1
L : Language α
⊢ epsilon ∘ₗ L = L
Tactic:
apply funext
State after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), (epsilon ∘ₗ L) x = L x

State before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), (epsilon ∘ₗ L) x = L x
Tactic:
intro w
State after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w = L w

State before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w = L w
Tactic:
apply propext
State after:
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w ↔ L w

State before:
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w ↔ L w
Tactic:
constructor
State after:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w

State before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Tactic:
. rw [Language.concat]
  intro ⟨u,v, h1, h2, h3⟩
  simp [Language.epsilon, Membership.mem] at h1
  simp [h3, h1, Word.epsilon]
  exact h2
State after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Tactic:
. intro h
  simp [Language.concat]
  exists ε ; simp [Language.epsilon, Membership.mem]
  assumption
State after:
no goals

State before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (epsilon ∘ₗ L) w → L w
Tactic:
rw [Language.concat]
State after:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ epsilon ∧ v ∈ L ∧ w = u * v) → L w

State before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ epsilon ∧ v ∈ L ∧ w = u * v) → L w
Tactic:
intro ⟨u,v, h1, h2, h3⟩
State after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ epsilon
h2 : v ∈ L
h3 : w = u * v
⊢ L w

State before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ epsilon
h2 : v ∈ L
h3 : w = u * v
⊢ L w
Tactic:
simp [Language.epsilon, Membership.mem] at h1
State after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L w

State before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L w
Tactic:
simp [h3, h1, Word.epsilon]
State after:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L v

State before:
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L v
Tactic:
exact h2
State after:
no goals

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (epsilon ∘ₗ L) w
Tactic:
intro h
State after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ (epsilon ∘ₗ L) w

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ (epsilon ∘ₗ L) w
Tactic:
simp [Language.concat]
State after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ∃ u ∈ epsilon, ∃ x ∈ L, w = u * x

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ∃ u ∈ epsilon, ∃ x ∈ L, w = u * x
Tactic:
exists ε
State after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ε ∈ epsilon ∧ ∃ x ∈ L, w = ε * x

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ ε ∈ epsilon ∧ ∃ x ∈ L, w = ε * x
Tactic:
simp [Language.epsilon, Membership.mem]
State after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ L w

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ L w
Tactic:
assumption
State after:
no goals