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

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

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

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

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

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

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

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

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

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

State before:
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ L ∧ v ∈ epsilon ∧ 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 ∈ L
h2 : v ∈ epsilon
h3 : w = u * v
⊢ L w

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

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

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

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

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

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

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

State before:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ epsilon 1
Tactic:
simp [Language.epsilon]
State after:
case h.a.mpr
α : Type u_1
L : Language α
w : Word α
h : L w
⊢ 1 = ε

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