internlm/Lean-Github huggingface dataset:
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
s : Str α
⊢ ∃ n, List.reverse s ∈ exp α n
Tactic:
induction s
Proof state after:
case nil
α : Type
⊢ ∃ n, [].reverse ∈ exp α n

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : ∃ n, tail✝.reverse ∈ exp α n
⊢ ∃ n, (head✝ :: tail✝).reverse ∈ exp α n
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
⊢ ∃ n, [].reverse ∈ exp α n
Tactic:
case nil =>
  apply Exists.intro 0
  exact exp.zero
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
case cons hd tl ih =>
  apply Exists.elim ih
  intro n a1
  apply Exists.intro (n + 1)
  simp
  exact exp.succ n hd tl.reverse a1
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
⊢ ∃ n, [].reverse ∈ exp α n
Tactic:
apply Exists.intro 0
Proof state after:
α : Type
⊢ [].reverse ∈ exp α 0
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
⊢ [].reverse ∈ exp α 0
Tactic:
exact exp.zero
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
apply Exists.elim ih
Proof state after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∀ (a : ℕ), tl.reverse ∈ exp α a → ∃ n, (hd :: tl).reverse ∈ exp α n
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∀ (a : ℕ), tl.reverse ∈ exp α a → ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
intro n a1
Proof state after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
apply Exists.intro (n + 1)
Proof state after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ (hd :: tl).reverse ∈ exp α (n + 1)
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ (hd :: tl).reverse ∈ exp α (n + 1)
Tactic:
simp
Proof state after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ tl.reverse ++ [hd] ∈ exp α (n + 1)
Theorem: Strings.rev_str_mem_exp
Proof state before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ tl.reverse ++ [hd] ∈ exp α (n + 1)
Tactic:
exact exp.succ n hd tl.reverse a1
Proof state after:
no goals
Theorem: Strings.str_mem_exp
Proof state before:
α : Type
s : Str α
⊢ ∃ n, s ∈ exp α n
Tactic:
obtain s1 := rev_str_mem_exp s.reverse
Proof state after:
α : Type
s : Str α
s1 : ∃ n, (List.reverse s).reverse ∈ exp α n
⊢ ∃ n, s ∈ exp α n
Theorem: Strings.str_mem_exp
Proof state before:
α : Type
s : Str α
s1 : ∃ n, (List.reverse s).reverse ∈ exp α n
⊢ ∃ n, s ∈ exp α n
Tactic:
simp only [List.reverse_reverse] at s1
Proof state after:
α : Type
s : Str α
s1 : ∃ n, s ∈ exp α n
⊢ ∃ n, s ∈ exp α n
Theorem: Strings.str_mem_exp
Proof state before:
α : Type
s : Str α
s1 : ∃ n, s ∈ exp α n
⊢ ∃ n, s ∈ exp α n
Tactic:
exact s1
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
s : Str α
⊢ List.reverse s ∈ exp α (List.length s)
Tactic:
induction s
Proof state after:
case nil
α : Type
⊢ [].reverse ∈ exp α [].length

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.reverse ∈ exp α tail✝.length
⊢ (head✝ :: tail✝).reverse ∈ exp α (head✝ :: tail✝).length
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
⊢ [].reverse ∈ exp α [].length
Tactic:
case nil =>
  simp
  exact exp.zero
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ (hd :: tl).reverse ∈ exp α (hd :: tl).length
Tactic:
case cons hd tl ih =>
  simp
  exact exp.succ tl.length hd tl.reverse ih
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
⊢ [].reverse ∈ exp α [].length
Tactic:
simp
Proof state after:
α : Type
⊢ [] ∈ exp α 0
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
⊢ [] ∈ exp α 0
Tactic:
exact exp.zero
Proof state after:
no goals
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ (hd :: tl).reverse ∈ exp α (hd :: tl).length
Tactic:
simp
Proof state after:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ tl.reverse ++ [hd] ∈ exp α (tl.length + 1)
Theorem: Strings.rev_str_mem_exp_str_len
Proof state before:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ tl.reverse ++ [hd] ∈ exp α (tl.length + 1)
Tactic:
exact exp.succ tl.length hd tl.reverse ih
Proof state after:
no goals
Theorem: Strings.str_mem_exp_str_len
Proof state before:
α : Type
s : Str α
⊢ s ∈ exp α (List.length s)
Tactic:
obtain s1 := rev_str_mem_exp_str_len s.reverse
Proof state after:
α : Type
s : Str α
s1 : (List.reverse s).reverse ∈ exp α (List.reverse s).length
⊢ s ∈ exp α (List.length s)
Theorem: Strings.str_mem_exp_str_len
Proof state before:
α : Type
s : Str α
s1 : (List.reverse s).reverse ∈ exp α (List.reverse s).length
⊢ s ∈ exp α (List.length s)
Tactic:
simp at s1
Proof state after:
α : Type
s : Str α
s1 : s ∈ exp α (List.length s)
⊢ s ∈ exp α (List.length s)
Theorem: Strings.str_mem_exp_str_len
Proof state before:
α : Type
s : Str α
s1 : s ∈ exp α (List.length s)
⊢ s ∈ exp α (List.length s)
Tactic:
exact s1
Proof state after:
no goals
Theorem: Strings.mem_exp_imp_str_len_eq
Proof state before:
α : Type
s : Str α
n : ℕ
h1 : s ∈ exp α n
⊢ List.length s = n
Tactic:
induction h1
Proof state after:
case zero
α : Type
s : Str α
n : ℕ
⊢ [].length = 0

case succ
α : Type
s : Str α
n n✝ : ℕ
a✝¹ : α
s✝ : Str α
a✝ : s✝ ∈ exp α n✝
a_ih✝ : List.length s✝ = n✝
⊢ List.length (s✝ ++ [a✝¹]) = n✝ + 1
Theorem: Strings.mem_exp_imp_str_len_eq
Proof state before:
α : Type
s : Str α
n : ℕ
⊢ [].length = 0
Tactic:
case zero =>
  simp
Proof state after:
no goals
Theorem: Strings.mem_exp_imp_str_len_eq
Proof state before:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length (s ++ [a]) = m + 1
Tactic:
case succ m a s ih_1 ih_2 =>
  simp
  exact ih_2
Proof state after:
no goals
Theorem: Strings.mem_exp_imp_str_len_eq
Proof state before:
α : Type
s : Str α
n : ℕ
⊢ [].length = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Strings.mem_exp_imp_str_len_eq
Proof state before:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length (s ++ [a]) = m + 1
Tactic:
simp
Proof state after:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length s = m
Theorem: Strings.mem_exp_imp_str_len_eq
Proof state before:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length s = m
Tactic:
exact ih_2
Proof state after:
no goals
Theorem: Strings.all_str_mem_kleene_closure
Proof state before:
α : Type
s : Str α
⊢ s ∈ kleene_closure α
Tactic:
simp only [kleene_closure]
Proof state after:
α : Type
s : Str α
⊢ s ∈ ⋃ n, exp α n
Theorem: Strings.all_str_mem_kleene_closure
Proof state before:
α : Type
s : Str α
⊢ s ∈ ⋃ n, exp α n
Tactic:
simp
Proof state after:
α : Type
s : Str α
⊢ ∃ i, s ∈ exp α i
Theorem: Strings.all_str_mem_kleene_closure
Proof state before:
α : Type
s : Str α
⊢ ∃ i, s ∈ exp α i
Tactic:
exact str_mem_exp s
Proof state after:
no goals
Theorem: Strings.thm_2
Proof state before:
α : Type
s t u : Str α
⊢ s ++ (t ++ u) = s ++ t ++ u
Tactic:
symm
Proof state after:
α : Type
s t u : Str α
⊢ s ++ t ++ u = s ++ (t ++ u)
Theorem: Strings.thm_2
Proof state before:
α : Type
s t u : Str α
⊢ s ++ t ++ u = s ++ (t ++ u)
Tactic:
exact (List.append_assoc s t u)
Proof state after:
no goals
Theorem: Languages.thm_3_a
Proof state before:
α : Type
L : Language α
⊢ concat L ∅ = ∅
Tactic:
simp only [concat]
Proof state after:
α : Type
L : Language α
⊢ {x | ∃ s ∈ L, ∃ t ∈ ∅, s ++ t = x} = ∅
Theorem: Languages.thm_3_a
Proof state before:
α : Type
L : Language α
⊢ {x | ∃ s ∈ L, ∃ t ∈ ∅, s ++ t = x} = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Languages.thm_3_b
Proof state before:
α : Type
L : Language α
⊢ concat ∅ L = ∅
Tactic:
simp only [concat]
Proof state after:
α : Type
L : Language α
⊢ {x | ∃ s ∈ ∅, ∃ t ∈ L, s ++ t = x} = ∅
Theorem: Languages.thm_3_b
Proof state before:
α : Type
L : Language α
⊢ {x | ∃ s ∈ ∅, ∃ t ∈ L, s ++ t = x} = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Languages.thm_3_c
Proof state before:
α : Type
L1 L2 L3 : Language α
⊢ concat L1 (concat L2 L3) = concat (concat L1 L2) L3
Tactic:
simp only [concat]
Proof state after:
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ {x | ∃ s ∈ L2, ∃ t ∈ L3, s ++ t = x}, s ++ t = x} =
    {x | ∃ s ∈ {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x}, ∃ t ∈ L3, s ++ t = x}
Theorem: Languages.thm_3_c
Proof state before:
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ {x | ∃ s ∈ L2, ∃ t ∈ L3, s ++ t = x}, s ++ t = x} =
    {x | ∃ s ∈ {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x}, ∃ t ∈ L3, s ++ t = x}
Tactic:
simp
Proof state after:
no goals
Theorem: Languages.thm_3_d
Proof state before:
α : Type
L1 L2 L3 : Language α
⊢ concat L1 (L2 ∪ L3) = concat L1 L2 ∪ concat L1 L3
Tactic:
simp only [concat]
Proof state after:
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ L2 ∪ L3, s ++ t = x} =
    {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x} ∪ {x | ∃ s ∈ L1, ∃ t ∈ L3, s ++ t = x}
Theorem: Languages.thm_3_d
Proof state before:
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ L2 ∪ L3, s ++ t = x} =
    {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x} ∪ {x | ∃ s ∈ L1, ∃ t ∈ L3, s ++ t = x}
Tactic:
aesop
Proof state after:
no goals
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
n : ℕ
⊢ exp L n ⊆ kleene_closure α L
Tactic:
simp only [Set.subset_def]
Proof state after:
α : Type
L : Language α
n : ℕ
⊢ ∀ x ∈ exp L n, x ∈ kleene_closure α L
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
n : ℕ
⊢ ∀ x ∈ exp L n, x ∈ kleene_closure α L
Tactic:
intro s a1
Proof state after:
α : Type
L : Language α
n : ℕ
s : Str α
a1 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
n : ℕ
s : Str α
a1 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
Tactic:
induction n generalizing s
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof state after:
no goals
Theorem: Languages.thm_4
Proof 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
Proof state after:
no goals
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
s : Str α
a1 : s ∈ exp L 0
⊢ s ∈ kleene_closure α L
Tactic:
simp only [exp] at a1
Proof state after:
α : Type
L : Language α
s : Str α
a1 : s ∈ {[]}
⊢ s ∈ kleene_closure α L
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
s : Str α
a1 : s ∈ {[]}
⊢ s ∈ kleene_closure α L
Tactic:
simp at a1
Proof state after:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ s ∈ kleene_closure α L
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ s ∈ kleene_closure α L
Tactic:
simp only [a1]
Proof state after:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ [] ∈ kleene_closure α L
Theorem: Languages.thm_4
Proof state before:
α : Type
L : Language α
s : Str α
a1 : s = []
⊢ [] ∈ kleene_closure α L
Tactic:
exact kleene_closure.eps L
Proof state after:
no goals
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof state after:
no goals
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof state after:
no goals
Theorem: Languages.thm_4
Proof 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]
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof 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
Theorem: Languages.thm_4
Proof 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
Proof state after:
no goals
Theorem: Languages.thm_5_left
Proof state before:
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L
Tactic:
simp only [Set.subset_def]
Proof state after:
α : Type
L : Language α
⊢ ∀ x ∈ ⋃ n, exp L n, x ∈ kleene_closure α L
Theorem: Languages.thm_5_left
Proof state before:
α : Type
L : Language α
⊢ ∀ x ∈ ⋃ n, exp L n, x ∈ kleene_closure α L
Tactic:
intro s a1
Proof state after:
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ kleene_closure α L
Theorem: Languages.thm_5_left
Proof state before:
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ kleene_closure α L
Tactic:
simp at a1
Proof state after:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ kleene_closure α L
Theorem: Languages.thm_5_left
Proof state before:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ kleene_closure α L
Tactic:
apply Exists.elim a1
Proof state after:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ ∀ (a : ℕ), s ∈ exp L a → s ∈ kleene_closure α L
Theorem: Languages.thm_5_left
Proof state before:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ ∀ (a : ℕ), s ∈ exp L a → s ∈ kleene_closure α L
Tactic:
intro n a2
Proof state after:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
n : ℕ
a2 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
Theorem: Languages.thm_5_left
Proof state before:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
n : ℕ
a2 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
Tactic:
exact Set.mem_of_subset_of_mem (thm_4 L n) a2
Proof state after:
no goals
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
⊢ kleene_closure α L ⊆ ⋃ n, exp L n
Tactic:
simp only [Set.subset_def]
Proof state after:
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ ⋃ n, exp L n
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ ⋃ n, exp L n
Tactic:
intro s a1
Proof state after:
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ ⋃ n, exp L n
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ ⋃ n, exp L n
Tactic:
induction a1
Proof state after:
case eps
α : Type
L : Language α
s : Str α
⊢ [] ∈ ⋃ n, exp L n

case succ
α : Type
L : Language α
s s✝ t✝ : Str α
a✝¹ : s✝ ∈ kleene_closure α L
a✝ : t✝ ∈ L
a_ih✝ : s✝ ∈ ⋃ n, exp L n
⊢ s✝ ++ t✝ ∈ ⋃ n, exp L n
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ ⋃ n, exp L n
Tactic:
case eps =>
  simp
  apply Exists.intro 0
  simp only [exp]
  simp
Proof state after:
no goals
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ ⋃ n, exp L n
Tactic:
simp
Proof state after:
α : Type
L : Language α
s : Str α
⊢ ∃ i, [] ∈ exp L i
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s : Str α
⊢ ∃ i, [] ∈ exp L i
Tactic:
apply Exists.intro 0
Proof state after:
α : Type
L : Language α
s : Str α
⊢ [] ∈ exp L 0
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ exp L 0
Tactic:
simp only [exp]
Proof state after:
α : Type
L : Language α
s : Str α
⊢ [] ∈ {[]}
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ {[]}
Tactic:
simp
Proof state after:
no goals
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : xs ∈ ⋃ n, exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
simp at ih_3
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ xs ++ ys ∈ ⋃ n, exp L n
Theorem: Languages.thm_5_right
Proof state before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
apply Exists.elim ih_3
Proof state after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ ∀ (a : ℕ), xs ∈ exp L a → xs ++ ys ∈ ⋃ n, exp L n