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

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

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

State before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ ↔ w ∈ ∅
Tactic:
constructor
State after:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅

State before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Tactic:
. intro n
  match n with
  | ⟨_,_,_,h,_⟩ =>
    apply False.elim h
State after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅

State before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Tactic:
. intro n
  apply False.elim n
State after:
no goals

State before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L ∘ₗ ∅ → w ∈ ∅
Tactic:
intro n
State after:
case h.mp
α : Type u_1
L : Language α
w : Word α
n : w ∈ L ∘ₗ ∅
⊢ w ∈ ∅

State before:
case h.mp
α : Type u_1
L : Language α
w : Word α
n : w ∈ L ∘ₗ ∅
⊢ w ∈ ∅
Tactic:
match n with
| ⟨_,_,_,h,_⟩ =>
  apply False.elim h
State after:
no goals

State before:
α : Type u_1
L : Language α
w : Word α
n : w ∈ L ∘ₗ ∅
w✝¹ w✝ : Word α
left✝ : w✝¹ ∈ L
h : w✝ ∈ ∅
right✝ : w = w✝¹ * w✝
⊢ w ∈ ∅
Tactic:
apply False.elim h
State after:
no goals

State before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ L ∘ₗ ∅
Tactic:
intro n
State after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅
⊢ w ∈ L ∘ₗ ∅

State before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
n : w ∈ ∅
⊢ w ∈ L ∘ₗ ∅
Tactic:
apply False.elim n
State after:
no goals