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
α : 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
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)
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 : σ}
    (hlen : Fintype.card σ ≤ List.length x) (hx : 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

α✝ : 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
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
wlog hle : (n : ℕ) ≤ m
α✝ : 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
α✝ : 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
have hm : (m : ℕ) ≤ Fintype.card σ := Fin.is_le m
α✝ : 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
α✝ : 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
dsimp at heq
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

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 σ

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) ≠ []

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
α✝ : 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
refine'
  ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, _, _, _, by
    rfl, _⟩
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
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
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]
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 (↑m) x) = t
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
use hq
no goals
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 (↑m) x) = t
rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
  List.take_append_drop, List.take_append_drop]
no goals
α : 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))
norm_num
no goals
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 : σ}
    (hlen : Fintype.card σ ≤ List.length x) (hx : 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
exact this _ hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle)
no goals
α✝ : 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))
rfl
no goals
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
rw [List.take_append_drop, List.take_append_drop]
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 σ
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 σ
simp only [List.length_drop, List.length_take]
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 σ
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 σ
rw [min_eq_left (hm.trans hlen), min_eq_left hle, add_tsub_cancel_of_le hle]
no goals
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 σ
exact hm
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
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) ≠ []
intro h
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
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
have hlen' := congr_arg List.length h
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
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
simp only [List.length_drop, List.length, List.length_take] at hlen'
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

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
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
rw [min_eq_left, tsub_eq_zero_iff_le] at hlen'
no goals
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
exact hm.trans hlen
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
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
apply hneq
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
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
apply le_antisymm
no goals
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
assumption'
no goals
α✝ : 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))
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]