-- Mathlib/Computability/DFA.lean
theorem pumping_lemma [Fintype σ] {x : List α} (hx : x ∈ M.accepts)
    (hlen : Fintype.card σ ≤ List.length x) :
    ∃ a b c,
      x = a ++ b ++ c ∧
        a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Proof state:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
⊢ a' ++ b' ++ c' ∈ M.accepts

Tactic:
have h := M.evalFrom_of_pow hb hb'

Result:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
⊢ a' ++ b' ++ c' ∈ M.accepts

Proof state:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'
⊢ a' ++ b' ++ c' ∈ M.accepts

Tactic:
rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]

Result:
no goals

Proof state:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ M.accepts

Tactic:
substs ha' hc'

Result:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : a'.length + b.length ≤ Fintype.card σ
hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
hx : x = a' ++ b ++ c'
hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x
⊢ a' ++ b' ++ c' ∈ M.accepts

Proof state:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : y ∈ {a} * {b}∗ * {c}
⊢ y ∈ M.accepts

Tactic:
rw [Language.mem_mul] at hy

Result:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : ∃ a_1 ∈ {a} * {b}∗, ∃ b ∈ {c}, a_1 ++ b = y
⊢ y ∈ M.accepts

Proof state:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' ∈ {c}
a' : List α
ha' : a' ∈ {a}
b' : List α
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ M.accepts

Tactic:
rw [Set.mem_singleton_iff] at ha' hc'

Result:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' = c
a' : List α
ha' : a' = a
b' : List α
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ M.accepts

Proof state:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : ∃ a_1 ∈ {a} * {b}∗, ∃ b ∈ {c}, a_1 ++ b = y
⊢ y ∈ M.accepts

Tactic:
rcases hy with ⟨ab, hab, c', hc', rfl⟩

Result:
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
ab : List α
hab : ab ∈ {a} * {b}∗
c' : List α
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ M.accepts

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
use a, b, c, hx, hlen, hnil

Result:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ {a} * {b}∗ * {c} ≤ M.accepts

Proof state:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
intro y hy

Result:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
y : List α
hy : y ∈ {a} * {b}∗ * {c}
⊢ y ∈ M.accepts