internlm/Lean-Github huggingface dataset:
Theorem: Language.concat_dist_union_r
Proof state before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inr h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨Or.inr h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L2
h2 : v ∈ L3
h3 : w = u * v
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3
Tactic:
exists u, v
Proof state after:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L2
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∪ L2 ∧ v ∈ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_r
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
u v : Word α
pv : u ∈ L2 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L2
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∪ L2 ∧ v ∈ L3 ∧ w = u * v
Tactic:
exact ⟨Or.inr h1, h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
⊢ L1 ∘ₗ (L2 ∪ L3) = L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ L1 ∘ₗ (L2 ∪ L3) ↔ x ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Theorem: Language.concat_dist_union_l
Proof state before:
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ L1 ∘ₗ (L2 ∪ L3) ↔ x ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) ↔ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Theorem: Language.concat_dist_union_l
Proof state before:
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) ↔ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Theorem: Language.concat_dist_union_l
Proof state before:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
. intro
  | ⟨u,v,h1,h2,h3⟩ =>
    cases h2 with
    | inl hl => apply Or.inl; exists u; exists v
    | inr hr => apply Or.inr; exists u; exists v
Proof state after:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Theorem: Language.concat_dist_union_l
Proof state before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
. intro
  | Or.inl hl => cases hl with | intro u pu => cases pu with | intro v pv =>
      match pv with
      | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
  | Or.inr hr => cases hr with | intro u pu => cases pu with | intro v pv =>
      match pv with
      | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
intro
| ⟨u,v,h1,h2,h3⟩ =>
  cases h2 with
  | inl hl => apply Or.inl; exists u; exists v
  | inr hr => apply Or.inr; exists u; exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h2 : v ∈ L2 ∪ L3
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
cases h2 with
| inl hl => apply Or.inl; exists u; exists v
| inr hr => apply Or.inr; exists u; exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case inl
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
apply Or.inl
Proof state after:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ w ∈ L1 ∘ₗ L2
Theorem: Language.concat_dist_union_l
Proof state before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ w ∈ L1 ∘ₗ L2
Tactic:
exists u
Proof state after:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ ∃ v, u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
Theorem: Language.concat_dist_union_l
Proof state before:
case inl.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hl : v ∈ L2
⊢ ∃ v, u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
Tactic:
exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case inr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
Tactic:
apply Or.inr
Proof state after:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ w ∈ L1 ∘ₗ L3
Theorem: Language.concat_dist_union_l
Proof state before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ w ∈ L1 ∘ₗ L3
Tactic:
exists u
Proof state after:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_l
Proof state before:
case inr.h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ (L2 ∪ L3)
u v : Word α
h1 : u ∈ L1
h3 : w = u * v
hr : v ∈ L3
⊢ ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
Tactic:
exists v
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
intro
| Or.inl hl => cases hl with | intro u pu => cases pu with | intro v pv =>
    match pv with
    | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
| Or.inr hr => cases hr with | intro u pu => cases pu with | intro v pv =>
    match pv with
    | ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
hl : w ∈ L1 ∘ₗ L2
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases hl with | intro u pu => cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inl h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
exists u, v
Proof state after:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v
Tactic:
exact ⟨h1, Or.inl h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
hr : w ∈ L1 ∘ₗ L3
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases hr with | intro u pu => cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
case intro.intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
Proof state after:
no goals
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
Tactic:
exists u, v
Proof state after:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v
Theorem: Language.concat_dist_union_l
Proof state before:
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L3
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v
Tactic:
exact ⟨h1, Or.inr h2, h3⟩
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
α : Type u_1
L : Language α
⊢ L⁺ ∪ {ε} = L∗
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ L⁺ ∪ {ε} ↔ x ∈ L∗
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ L⁺ ∪ {ε} ↔ x ∈ L∗
Tactic:
intro w
Proof state after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} ↔ w ∈ L∗
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} ↔ w ∈ L∗
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Tactic:
. intro
  | Or.inl h =>
    cases h with
    | intro n r =>
      exists n
      exact r.right
  | Or.inr e => exists 0
Proof state after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Tactic:
. simp [KStar.kstar]
  intro
  | Exists.intro nn r =>
    cases nn with
    | succ m =>
      apply Or.inl
      unfold Language.plus
      exists (Nat.succ m)
      exact ⟨Nat.succ_ne_zero m, r⟩
    | zero =>
      apply Or.inr
      exact r
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗
Tactic:
intro
| Or.inl h =>
  cases h with
  | intro n r =>
    exists n
    exact r.right
| Or.inr e => exists 0
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
h : w ∈ L⁺
⊢ w ∈ L∗
Tactic:
cases h with
| intro n r =>
  exists n
  exact r.right
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case intro
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
n : ℕ
r : ¬n = 0 ∧ w ∈ L ^ n
⊢ w ∈ L∗
Tactic:
exists n
Proof state after:
case intro
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
n : ℕ
r : ¬n = 0 ∧ w ∈ L ^ n
⊢ w ∈ L ^ n
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case intro
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
n : ℕ
r : ¬n = 0 ∧ w ∈ L ^ n
⊢ w ∈ L ^ n
Tactic:
exact r.right
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
e : w ∈ {ε}
⊢ w ∈ L∗
Tactic:
exists 0
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Tactic:
simp [KStar.kstar]
Proof state after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ kstar L → w ∈ L⁺ ∪ {ε}
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ kstar L → w ∈ L⁺ ∪ {ε}
Tactic:
intro
| Exists.intro nn r =>
  cases nn with
  | succ m =>
    apply Or.inl
    unfold Language.plus
    exists (Nat.succ m)
    exact ⟨Nat.succ_ne_zero m, r⟩
  | zero =>
    apply Or.inr
    exact r
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
nn : ℕ
r : (fun n => w ∈ L ^ n) nn
⊢ w ∈ L⁺ ∪ {ε}
Tactic:
cases nn with
| succ m =>
  apply Or.inl
  unfold Language.plus
  exists (Nat.succ m)
  exact ⟨Nat.succ_ne_zero m, r⟩
| zero =>
  apply Or.inr
  exact r
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case succ
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺ ∪ {ε}
Tactic:
apply Or.inl
Proof state after:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺
Tactic:
unfold Language.plus
Proof state after:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ fun w => ∃ n, ¬n = 0 ∧ w ∈ L ^ n
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ fun w => ∃ n, ¬n = 0 ∧ w ∈ L ^ n
Tactic:
exists (Nat.succ m)
Proof state after:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ ¬Nat.succ m = 0 ∧ w ∈ L ^ Nat.succ m
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ ¬Nat.succ m = 0 ∧ w ∈ L ^ Nat.succ m
Tactic:
exact ⟨Nat.succ_ne_zero m, r⟩
Proof state after:
no goals
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case zero
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
r : w ∈ L ^ Nat.zero
⊢ w ∈ L⁺ ∪ {ε}
Tactic:
apply Or.inr
Proof state after:
case zero.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
r : w ∈ L ^ Nat.zero
⊢ w ∈ {ε}
Theorem: Language.kleene_eq_plus_eps
Proof state before:
case zero.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
r : w ∈ L ^ Nat.zero
⊢ w ∈ {ε}
Tactic:
exact r
Proof state after:
no goals
Theorem: Language.Sigma.kleene_contains_all
Proof state before:
α : Type u_1
⊢ [] ∈ (Σ)∗
Tactic:
exists 0
Proof state after:
no goals
Theorem: Language.Sigma.kleene_contains_all
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ x :: xs ∈ (Σ)∗
Tactic:
have ⟨n, hn⟩ := Sigma.kleene_contains_all xs
Proof state after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ)∗
Theorem: Language.Sigma.kleene_contains_all
Proof state before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ)∗
Tactic:
exists (1 + n)
Proof state after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) ^ (1 + n)
Theorem: Language.Sigma.kleene_contains_all
Proof state before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) ^ (1 + n)
Tactic:
simp [pow_add]
Proof state after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) * (Σ) ^ n
Theorem: Language.Sigma.kleene_contains_all
Proof state before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) * (Σ) ^ n
Tactic:
exists [x]
Proof state after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ ∃ v, [x] ∈ (Σ) ∧ v ∈ (Σ) ^ n ∧ x :: xs = [x] * v
Theorem: Language.Sigma.kleene_contains_all
Proof state before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ ∃ v, [x] ∈ (Σ) ∧ v ∈ (Σ) ^ n ∧ x :: xs = [x] * v
Tactic:
exists xs
Proof state after:
no goals
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
α : Type u_1
⊢ univ = (Σ)∗
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
⊢ ∀ (x : Word α), x ∈ univ ↔ x ∈ (Σ)∗
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h
α : Type u_1
⊢ ∀ (x : Word α), x ∈ univ ↔ x ∈ (Σ)∗
Tactic:
intro w
Proof state after:
case h
α : Type u_1
w : Word α
⊢ w ∈ univ ↔ w ∈ (Σ)∗
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h
α : Type u_1
w : Word α
⊢ w ∈ univ ↔ w ∈ (Σ)∗
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗

case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗

case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Tactic:
. intros; exact Sigma.kleene_contains_all w
Proof state after:
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Tactic:
. intros; simp [Language.univ, Set.mem_univ]
Proof state after:
no goals
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗
Tactic:
intros
Proof state after:
case h.mp
α : Type u_1
w : Word α
a✝ : w ∈ univ
⊢ w ∈ (Σ)∗
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h.mp
α : Type u_1
w : Word α
a✝ : w ∈ univ
⊢ w ∈ (Σ)∗
Tactic:
exact Sigma.kleene_contains_all w
Proof state after:
no goals
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Tactic:
intros
Proof state after:
case h.mpr
α : Type u_1
w : Word α
a✝ : w ∈ (Σ)∗
⊢ w ∈ univ
Theorem: Language.Sigma.kleene_eq_univ
Proof state before:
case h.mpr
α : Type u_1
w : Word α
a✝ : w ∈ (Σ)∗
⊢ w ∈ univ
Tactic:
simp [Language.univ, Set.mem_univ]
Proof state after:
no goals
Theorem: Language.Sigma.maximal_language
Proof state before:
α : Type u_1
⊢ ∀ (L : Language α), L ⊆ (Σ)∗
Tactic:
intro _ w _
Proof state after:
α : Type u_1
L✝ : Language α
w : Word α
a✝ : w ∈ L✝
⊢ w ∈ (Σ)∗
Theorem: Language.Sigma.maximal_language
Proof state before:
α : Type u_1
L✝ : Language α
w : Word α
a✝ : w ∈ L✝
⊢ w ∈ (Σ)∗
Tactic:
exact Sigma.kleene_contains_all w
Proof state after:
no goals
Theorem: Alphabet.card_pos
Proof state before:
α : Type u_1
alphabet : Alphabet α
⊢ Fintype.card α > 0
Tactic:
apply Finset.card_pos.mpr
Proof state after:
α : Type u_1
alphabet : Alphabet α
⊢ Finset.univ.Nonempty
Theorem: Alphabet.card_pos
Proof state before:
α : Type u_1
alphabet : Alphabet α
⊢ Finset.univ.Nonempty
Tactic:
exists alphabet.default
Proof state after:
α : Type u_1
alphabet : Alphabet α
⊢ default ∈ Finset.univ
Theorem: Alphabet.card_pos
Proof state before:
α : Type u_1
alphabet : Alphabet α
⊢ default ∈ Finset.univ
Tactic:
exact alphabet.complete alphabet.default
Proof state after:
no goals
Theorem: RegularProduction.rhs_eq_deconstr_rhs
Proof state before:
α✝¹ : Type
Z : Finset α✝¹
α✝ : Type
V : Finset α✝
p : RegularProduction Z V
⊢ Production.rhs p = Word.mk (Sum.inr <$> Option.toList (getRhs p).1) * Word.mk (Sum.inl <$> Option.toList (getRhs p).2)
Tactic:
cases p <;> rfl
Proof state after:
no goals
Theorem: RegularProduction.lhs_eq_production_lhs
Proof state before:
α✝¹ : Type
Z : Finset α✝¹
α✝ : Type
V : Finset α✝
p : RegularProduction Z V
⊢ Production.lhs p = [Sum.inl (lhs p)]
Tactic:
rfl
Proof state after:
no goals
Theorem: RegularProduction.eps_step_result
Proof state before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
⊢ ↑p = eps v → DerivationStep.result (DerivationStep.fromRule p) = ε
Tactic:
intro h
Proof state after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ DerivationStep.result (DerivationStep.fromRule p) = ε
Theorem: RegularProduction.eps_step_result
Proof state before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ DerivationStep.result (DerivationStep.fromRule p) = ε
Tactic:
simp [DerivationStep.fromRule, DerivationStep.result, h]
Proof state after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ Production.rhs (eps v) = ε
Theorem: RegularProduction.eps_step_result
Proof state before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ Production.rhs (eps v) = ε
Tactic:
rfl
Proof state after:
no goals
Theorem: RegularProduction.cons_step_result
Proof state before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
⊢ ↑p = cons v (w, b) → DerivationStep.result (DerivationStep.fromRule p) = [Sum.inr w, Sum.inl b]
Tactic:
intro h
Proof state after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ DerivationStep.result (DerivationStep.fromRule p) = [Sum.inr w, Sum.inl b]
Theorem: RegularProduction.cons_step_result
Proof state before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ DerivationStep.result (DerivationStep.fromRule p) = [Sum.inr w, Sum.inl b]
Tactic:
simp [DerivationStep.fromRule, DerivationStep.result, h]
Proof state after:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ Production.rhs (cons v (w, b)) = [Sum.inr w, Sum.inl b]
Theorem: RegularProduction.cons_step_result
Proof state before:
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
w : { x // x ∈ G.Z }
b : { x // x ∈ G.V }
h : ↑p = cons v (w, b)
⊢ Production.rhs (cons v (w, b)) = [Sum.inr w, Sum.inl b]
Tactic:
rfl
Proof state after:
no goals
Theorem: RegularProduction.eq_eps_from_isEps
Proof state before:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
⊢ isEps p → p = eps (lhs p)
Tactic:
intro h
Proof state after:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
h : isEps p
⊢ p = eps (lhs p)
Theorem: RegularProduction.eq_eps_from_isEps
Proof state before:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
h : isEps p
⊢ p = eps (lhs p)
Tactic:
match p with
| .eps _ => rfl
Proof state after:
no goals