Theorem: Languages.thm_4 (FOL/Parsing/Text.lean)

State before:
α : Type
L : Language α
n : ℕ
⊢ exp L n ⊆ kleene_closure α L
Tactic:
simp only [Set.subset_def]
State after:
α : Type
L : Language α
n : ℕ
⊢ ∀ x ∈ exp L n, x ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
⊢ ∀ x ∈ exp L n, x ∈ kleene_closure α L
Tactic:
intro s a1
State after:
α : Type
L : Language α
n : ℕ
s : Str α
a1 : s ∈ exp L n
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
s : Str α
a1 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
Tactic:
induction n generalizing s
State after:
case zero
α : Type
L : Language α
s : Str α
a1 : s ∈ exp L 0
⊢ s ∈ kleene_closure α L

case succ
α : Type
L : Language α
n✝ : ℕ
a✝ : ∀ s ∈ exp L n✝, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ exp L (n✝ + 1)
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : s ∈ exp L 0
⊢ s ∈ kleene_closure α L
Tactic:
case zero =>
  simp only [exp] at a1
  simp at a1
  simp only [a1]
  exact kleene_closure.eps L
State after:
no goals

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ exp L (n + 1)
⊢ s ∈ kleene_closure α L
Tactic:
case succ n ih =>
  simp only [exp] at a1
  simp only [concat] at a1
  simp at a1
  apply Exists.elim a1
  intro xs a2
  clear a1
  cases a2
  case _ a2_left a2_right =>
    apply Exists.elim a2_right
    intro ys a3
    clear a2_right
    cases a3
    case _ a3_left a3_right =>
      simp only [← a3_right]
      apply kleene_closure.succ L
      apply ih xs a2_left
      exact a3_left
State after:
no goals

State before:
α : Type
L : Language α
s : Str α
a1 : s ∈ exp L 0
⊢ s ∈ kleene_closure α L
Tactic:
simp only [exp] at a1
State after:
α : Type
L : Language α
s : Str α
a1 : s ∈ {[]}
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : s ∈ {[]}
⊢ s ∈ kleene_closure α L
Tactic:
simp at a1
State after:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ s ∈ kleene_closure α L
Tactic:
simp only [a1]
State after:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ [] ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ [] ∈ kleene_closure α L
Tactic:
exact kleene_closure.eps L
State after:
no goals

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ exp L (n + 1)
⊢ s ∈ kleene_closure α L
Tactic:
simp only [exp] at a1
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ concat (exp L n) L
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ concat (exp L n) L
⊢ s ∈ kleene_closure α L
Tactic:
simp only [concat] at a1
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}
⊢ s ∈ kleene_closure α L
Tactic:
simp at a1
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : ∃ s_1 ∈ exp L n, ∃ t ∈ L, s_1 ++ t = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : ∃ s_1 ∈ exp L n, ∃ t ∈ L, s_1 ++ t = s
⊢ s ∈ kleene_closure α L
Tactic:
apply Exists.elim a1
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : ∃ s_1 ∈ exp L n, ∃ t ∈ L, s_1 ++ t = s
⊢ ∀ (a : Str α), (a ∈ exp L n ∧ ∃ t ∈ L, a ++ t = s) → s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : ∃ s_1 ∈ exp L n, ∃ t ∈ L, s_1 ++ t = s
⊢ ∀ (a : Str α), (a ∈ exp L n ∧ ∃ t ∈ L, a ++ t = s) → s ∈ kleene_closure α L
Tactic:
intro xs a2
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : ∃ s_1 ∈ exp L n, ∃ t ∈ L, s_1 ++ t = s
xs : Str α
a2 : xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : ∃ s_1 ∈ exp L n, ∃ t ∈ L, s_1 ++ t = s
xs : Str α
a2 : xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L
Tactic:
clear a1
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2 : xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2 : xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L
Tactic:
cases a2
State after:
case intro
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
left✝ : xs ∈ exp L n
right✝ : ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L
Tactic:
case _ a2_left a2_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    simp only [← a3_right]
    apply kleene_closure.succ L
    apply ih xs a2_left
    exact a3_left
State after:
no goals

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L
Tactic:
apply Exists.elim a2_right
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
⊢ ∀ (a : Str α), a ∈ L ∧ xs ++ a = s → s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
⊢ ∀ (a : Str α), a ∈ L ∧ xs ++ a = s → s ∈ kleene_closure α L
Tactic:
intro ys a3
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
ys : Str α
a3 : ys ∈ L ∧ xs ++ ys = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
ys : Str α
a3 : ys ∈ L ∧ xs ++ ys = s
⊢ s ∈ kleene_closure α L
Tactic:
clear a2_right
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3 : ys ∈ L ∧ xs ++ ys = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3 : ys ∈ L ∧ xs ++ ys = s
⊢ s ∈ kleene_closure α L
Tactic:
cases a3
State after:
case intro
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
left✝ : ys ∈ L
right✝ : xs ++ ys = s
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ s ∈ kleene_closure α L
Tactic:
case _ a3_left a3_right =>
  simp only [← a3_right]
  apply kleene_closure.succ L
  apply ih xs a2_left
  exact a3_left
State after:
no goals

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ s ∈ kleene_closure α L
Tactic:
simp only [← a3_right]
State after:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ xs ++ ys ∈ kleene_closure α L

State before:
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ xs ++ ys ∈ kleene_closure α L
Tactic:
apply kleene_closure.succ L
State after:
case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ xs ∈ kleene_closure α L

case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ ys ∈ L

State before:
case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ xs ∈ kleene_closure α L

case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ ys ∈ L
Tactic:
apply ih xs a2_left
State after:
case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ ys ∈ L

State before:
case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ ys ∈ L
Tactic:
exact a3_left
State after:
no goals