α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ DFA.accepts (toDFA M)
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ DFA.accepts (toDFA M)
α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ accepts M
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
rw [← toDFA_correct] at hx ⊢
no goals
α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ DFA.accepts (toDFA M)
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ DFA.accepts (toDFA M)
exact M.toDFA.pumping_lemma hx hlen