diff --git a/Mathlib.lean b/Mathlib.lean
index 788e885ffb27b..2ed934b727fee 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -282,6 +282,7 @@ import Mathlib.Combinatorics.SetFamily.Shadow
 import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
 import Mathlib.Combinatorics.Young.SemistandardTableau
 import Mathlib.Combinatorics.Young.YoungDiagram
+import Mathlib.Computability.DFA
 import Mathlib.Computability.Language
 import Mathlib.Computability.TuringMachine
 import Mathlib.Control.Applicative
diff --git a/Mathlib/Computability/DFA.lean b/Mathlib/Computability/DFA.lean
new file mode 100644
index 0000000000000..be1b063224eac
--- /dev/null
+++ b/Mathlib/Computability/DFA.lean
@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2020 Fox Thomson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fox Thomson
+
+! This file was ported from Lean 3 source module computability.DFA
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Fintype.Card
+import Mathlib.Computability.Language
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.WLOG
+
+/-!
+# Deterministic Finite Automata
+
+This file contains the definition of a Deterministic Finite Automaton (DFA), a state machine which
+determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set
+in linear time.
+Note that this definition allows for Automaton with infinite states, a `Fintype` instance must be
+supplied for true DFA's.
+-/
+
+
+open Computability
+
+universe u v
+
+-- Porting note: Required as `DFA` is used in mathlib3
+set_option linter.uppercaseLean3 false
+
+/-- A DFA is a set of states (`σ`), a transition function from state to state labelled by the
+  alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`). -/
+structure DFA (α : Type u) (σ : Type v) where
+  /-- A transition function from state to state labelled by the alphabet. -/
+  step : σ → α → σ
+  /-- Starting state. -/
+  start : σ
+  /-- Set of acceptance states. -/
+  accept : Set σ
+#align DFA DFA
+
+namespace DFA
+
+variable {α : Type u} {σ : Type v} (M : DFA α σ)
+
+instance [Inhabited σ] : Inhabited (DFA α σ) :=
+  ⟨DFA.mk (fun _ _ => default) default ∅⟩
+
+/-- `M.evalFrom s x` evaluates `M` with input `x` starting from the state `s`. -/
+def evalFrom (start : σ) : List α → σ :=
+  List.foldl M.step start
+#align DFA.eval_from DFA.evalFrom
+
+@[simp]
+theorem evalFrom_nil (s : σ) : M.evalFrom s [] = s :=
+  rfl
+#align DFA.eval_from_nil DFA.evalFrom_nil
+
+@[simp]
+theorem evalFrom_singleton (s : σ) (a : α) : M.evalFrom s [a] = M.step s a :=
+  rfl
+#align DFA.eval_from_singleton DFA.evalFrom_singleton
+
+@[simp]
+theorem evalFrom_append_singleton (s : σ) (x : List α) (a : α) :
+    M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a := by
+  simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
+#align DFA.eval_from_append_singleton DFA.evalFrom_append_singleton
+
+/-- `M.eval x` evaluates `M` with input `x` starting from the state `M.start`. -/
+def eval : List α → σ :=
+  M.evalFrom M.start
+#align DFA.eval DFA.eval
+
+@[simp]
+theorem eval_nil : M.eval [] = M.start :=
+  rfl
+#align DFA.eval_nil DFA.eval_nil
+
+@[simp]
+theorem eval_singleton (a : α) : M.eval [a] = M.step M.start a :=
+  rfl
+#align DFA.eval_singleton DFA.eval_singleton
+
+@[simp]
+theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.step (M.eval x) a :=
+  evalFrom_append_singleton _ _ _ _
+#align DFA.eval_append_singleton DFA.eval_append_singleton
+
+theorem evalFrom_of_append (start : σ) (x y : List α) :
+    M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y :=
+  x.foldl_append _ _ y
+#align DFA.eval_from_of_append DFA.evalFrom_of_append
+
+/-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state. -/
+def accepts : Language α := fun x => M.eval x ∈ M.accept
+#align DFA.accepts DFA.accepts
+
+theorem mem_accepts (x : List α) : x ∈ M.accepts ↔ M.evalFrom M.start x ∈ M.accept := by rfl
+#align DFA.mem_accepts DFA.mem_accepts
+
+theorem evalFrom_split [Fintype σ] {x : List α} {s t : σ} (hlen : Fintype.card σ ≤ x.length)
+    (hx : M.evalFrom s x = t) :
+    ∃ q a b c,
+      x = a ++ b ++ c ∧
+        a.length + b.length ≤ Fintype.card σ ∧
+          b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t := by
+  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)
+  wlog hle : (n : ℕ) ≤ m
+  · exact this _ hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle)
+  have hm : (m : ℕ) ≤ Fintype.card σ := Fin.is_le m
+  dsimp at heq
+  refine'
+    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, _, _, _, by
+      rfl, _⟩
+  · rw [List.take_append_drop, List.take_append_drop]
+  · simp only [List.length_drop, List.length_take]
+    rw [min_eq_left (hm.trans hlen), min_eq_left hle, add_tsub_cancel_of_le hle]
+    exact hm
+  · intro h
+    have hlen' := congr_arg List.length h
+    simp only [List.length_drop, List.length, List.length_take] at hlen'
+    rw [min_eq_left, tsub_eq_zero_iff_le] at hlen'
+    · apply hneq
+      apply le_antisymm
+      assumption'
+    exact hm.trans hlen
+  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]
+  use hq
+  rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
+    List.take_append_drop, List.take_append_drop]
+#align DFA.eval_from_split DFA.evalFrom_split
+
+theorem evalFrom_of_pow {x y : List α} {s : σ} (hx : M.evalFrom s x = s)
+    (hy : y ∈ ({x} : Language α)∗) : M.evalFrom s y = s := by
+  rw [Language.mem_kstar] at hy
+  rcases hy with ⟨S, rfl, hS⟩
+  induction' S with a S ih
+  · rfl
+  · have ha := hS a (List.mem_cons_self _ _)
+    rw [Set.mem_singleton_iff] at ha
+    rw [List.join, evalFrom_of_append, ha, hx]
+    apply ih
+    intro z hz
+    exact hS z (List.mem_cons_of_mem a hz)
+#align DFA.eval_from_of_pow DFA.evalFrom_of_pow
+
+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 := by
+  obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split hlen rfl
+  use a, b, c, hx, hlen, hnil
+  intro y hy
+  rw [Language.mem_mul] at hy
+  rcases hy with ⟨ab, c', hab, hc', rfl⟩
+  rw [Language.mem_mul] at hab
+  rcases hab with ⟨a', b', ha', hb', rfl⟩
+  rw [Set.mem_singleton_iff] at ha' hc'
+  substs ha' hc'
+  have h := M.evalFrom_of_pow hb hb'
+  rwa [mem_accepts, evalFrom_of_append, evalFrom_of_append, h, hc]
+#align DFA.pumping_lemma DFA.pumping_lemma
+
+end DFA