[GOAL]
α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
a : α
⊢ evalFrom M s (x ++ [a]) = step M (evalFrom M s x) a
[PROOFSTEP]
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ accepts M ↔ evalFrom M M.start x ∈ M.accept
[PROOFSTEP]
rfl
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
obtain ⟨n, m, hneq, heq⟩ :=
  Fintype.exists_ne_map_eq_of_card_lt (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by norm_num)
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
⊢ Fintype.card σ < Fintype.card (Fin (Fintype.card σ + 1))
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
wlog hle : (n : ℕ) ≤ m
[GOAL]
case intro.intro.intro.inr
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
this :
  ∀ {α : Type u} {σ : Type v} (M : DFA α σ) [inst : Fintype σ] {x : List α} {s t : σ},
    Fintype.card σ ≤ List.length x →
      evalFrom M s x = t →
        ∀ (n m : Fin (Fintype.card σ + 1)),
          n ≠ m →
            evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x) →
              ↑n ≤ ↑m →
                ∃ q a b c,
                  x = a ++ b ++ c ∧
                    List.length a + List.length b ≤ Fintype.card σ ∧
                      b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
hle : ¬↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
exact this _ hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle)
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
have hm : (m : ℕ) ≤ Fintype.card σ := Fin.is_le m
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
refine' ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, _, _, _, by rfl, _⟩
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ evalFrom M s (List.take (↑n) (List.take (↑m) x)) = evalFrom M s (List.take (↑n) (List.take (↑m) x))
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ x = List.take (↑n) (List.take (↑m) x) ++ List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x
[PROOFSTEP]
rw [List.take_append_drop, List.take_append_drop]
[GOAL]
case refine'_2
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ List.length (List.take (↑n) (List.take (↑m) x)) + List.length (List.drop (↑n) (List.take (↑m) x)) ≤ Fintype.card σ
[PROOFSTEP]
simp only [List.length_drop, List.length_take]
[GOAL]
case refine'_2
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ min (↑n) (min (↑m) (List.length x)) + (min (↑m) (List.length x) - ↑n) ≤ Fintype.card σ
[PROOFSTEP]
rw [min_eq_left (hm.trans hlen), min_eq_left hle, add_tsub_cancel_of_le hle]
[GOAL]
case refine'_2
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ ↑m ≤ Fintype.card σ
[PROOFSTEP]
exact hm
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ List.drop (↑n) (List.take (↑m) x) ≠ []
[PROOFSTEP]
intro h
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
⊢ False
[PROOFSTEP]
have hlen' := congr_arg List.length h
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : List.length (List.drop (↑n) (List.take (↑m) x)) = List.length []
⊢ False
[PROOFSTEP]
simp only [List.length_drop, List.length, List.length_take] at hlen' 
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : min (↑m) (List.length x) - ↑n = 0
⊢ False
[PROOFSTEP]
rw [min_eq_left, tsub_eq_zero_iff_le] at hlen' 
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ False
[PROOFSTEP]
apply hneq
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ n = m
[PROOFSTEP]
apply le_antisymm
[GOAL]
case refine'_3.a
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ n ≤ m
case refine'_3.a
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ m ≤ n
[PROOFSTEP]
assumption'
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : min (↑m) (List.length x) - ↑n = 0
⊢ ↑m ≤ List.length x
[PROOFSTEP]
exact hm.trans hlen
[GOAL]
case refine'_4
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
      evalFrom M s (List.take (↑n) (List.take (↑m) x)) ∧
    evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
[PROOFSTEP]
have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) = M.evalFrom s ((x.take m).take n) := by
  rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ← List.take_take, min_eq_left hle,
    List.take_append_drop]
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    evalFrom M s (List.take (↑n) (List.take (↑m) x))
[PROOFSTEP]
rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ← List.take_take, min_eq_left hle,
  List.take_append_drop]
[GOAL]
case refine'_4
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
hq :
  evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    evalFrom M s (List.take (↑n) (List.take (↑m) x))
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
      evalFrom M s (List.take (↑n) (List.take (↑m) x)) ∧
    evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
[PROOFSTEP]
use hq
[GOAL]
case right
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
hq :
  evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    evalFrom M s (List.take (↑n) (List.take (↑m) x))
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
[PROOFSTEP]
rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc, List.take_append_drop,
  List.take_append_drop]
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : y ∈ {x}∗
⊢ evalFrom M s y = s
[PROOFSTEP]
rw [Language.mem_kstar] at hy 
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : ∃ L, y = List.join L ∧ ∀ (y : List α), y ∈ L → y ∈ {x}
⊢ evalFrom M s y = s
[PROOFSTEP]
rcases hy with ⟨S, rfl, hS⟩
[GOAL]
case intro.intro
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ {x}
⊢ evalFrom M s (List.join S) = s
[PROOFSTEP]
induction' S with a S ih
[GOAL]
case intro.intro.nil
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS✝ : ∀ (y : List α), y ∈ S → y ∈ {x}
hS : ∀ (y : List α), y ∈ [] → y ∈ {x}
⊢ evalFrom M s (List.join []) = s
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
[PROOFSTEP]
have ha := hS a (List.mem_cons_self _ _)
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
[PROOFSTEP]
rw [Set.mem_singleton_iff] at ha 
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join (a :: S)) = s
[PROOFSTEP]
rw [List.join, evalFrom_of_append, ha, hx]
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join S) = s
[PROOFSTEP]
apply ih
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ ∀ (y : List α), y ∈ S → y ∈ {x}
[PROOFSTEP]
intro z hz
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
z : List α
hz : z ∈ S
⊢ z ∈ {x}
[PROOFSTEP]
exact hS z (List.mem_cons_of_mem a hz)
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ accepts M
hlen : Fintype.card σ ≤ List.length x
⊢ ∃ a b c, x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split hlen rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
⊢ ∃ a b c, x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
use a, b, c, hx, hlen, hnil
[GOAL]
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
⊢ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
intro y hy
[GOAL]
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
y : List α
hy : y ∈ {a} * {b}∗ * {c}
⊢ y ∈ accepts M
[PROOFSTEP]
rw [Language.mem_mul] at hy 
[GOAL]
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
y : List α
hy : ∃ a_1 b_1, a_1 ∈ {a} * {b}∗ ∧ b_1 ∈ {c} ∧ a_1 ++ b_1 = y
⊢ y ∈ accepts M
[PROOFSTEP]
rcases hy with ⟨ab, c', hab, hc', rfl⟩
[GOAL]
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
ab c' : List α
hab : ab ∈ {a} * {b}∗
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ accepts M
[PROOFSTEP]
rw [Language.mem_mul] at hab 
[GOAL]
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
ab c' : List α
hab : ∃ a_1 b_1, a_1 ∈ {a} ∧ b_1 ∈ {b}∗ ∧ a_1 ++ b_1 = ab
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ accepts M
[PROOFSTEP]
rcases hab with ⟨a', b', ha', hb', rfl⟩
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
c' : List α
hc' : c' ∈ {c}
a' b' : List α
ha' : a' ∈ {a}
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
rw [Set.mem_singleton_iff] at ha' hc' 
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
c' : List α
hc' : c' = c
a' b' : List α
ha' : a' = a
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
substs ha' hc'
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : List.length a' + List.length b ≤ Fintype.card σ
hb : evalFrom M (evalFrom M ?m.8103 a') b = evalFrom M ?m.8103 a'
hx : x = a' ++ b ++ c'
hc : evalFrom M (evalFrom M ?m.8103 a') c' = evalFrom M ?m.8103 x
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
have h := M.evalFrom_of_pow hb hb'
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : List.length a' + List.length b ≤ Fintype.card σ
hb : evalFrom M (evalFrom M ?m.8103 a') b = evalFrom M ?m.8103 a'
hx : x = a' ++ b ++ c'
hc : evalFrom M (evalFrom M ?m.8103 a') c' = evalFrom M ?m.8103 x
h : evalFrom M (evalFrom M ?m.8103 a') b' = evalFrom M ?m.8103 a'
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
rwa [mem_accepts, evalFrom_of_append, evalFrom_of_append, h, hc]
