Theorem: Language.empty_mul (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 α
h : w✝¹ ∈ ∅
left✝ : w✝ ∈ L
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