awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_1 :
  x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
refine_2 :
  (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)).length + (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length ≤
    Fintype.card σ
refine_3 : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ≠ []
refine_4 :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
      M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)) ∧
    M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    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

Tactic:
refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_1 : x = List.take (↑m : ℕ) x ++ List.drop (↑m : ℕ) x
refine_1₁ refine_1₂ : x = x
⊢ x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x

Tactic:
rw [List.take_append_drop, List.take_append_drop]

Premises used: List.take_append_drop
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_2 : min (↑n : ℕ) (min (↑m : ℕ) x.length) + (min (↑m : ℕ) x.length - (↑n : ℕ)) ≤ Fintype.card σ
⊢ (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)).length + (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length ≤
    Fintype.card σ

Tactic:
simp only [List.length_drop, List.length_take]

Premises used: List.length_drop, List.length_take
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ min (↑n : ℕ) (min (↑m : ℕ) x.length) + (min (↑m : ℕ) x.length - (↑n : ℕ)) ≤ Fintype.card σ

Tactic:
omega
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
h : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) = []
⊢ (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length = List.length.{u} (α := α) []

Tactic:
have hlen' := congr_arg List.length h
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
h : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) = []
hlen' : (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length = List.length.{u} (α := α) []
⊢ min (↑m : ℕ) x.length - (↑n : ℕ) = 0

Tactic:
simp only [List.length_drop, List.length, List.length_take] at hlen'

Premises used: List.length_drop, List.length_take, List.length
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
h : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) = []
hlen' : min (↑m : ℕ) x.length - (↑n : ℕ) = 0
⊢ False

Tactic:
omega
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
rw :
  M.evalFrom (M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x)
rw₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) x)) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) x)
rw₂ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) x)
rw₃ :
  M.evalFrom s (List.take (↑n : ℕ) x ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑m : ℕ) x)
rw₄ :
  M.evalFrom s (List.take (min (↑n : ℕ) (↑m : ℕ)) x ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
rw₅ :
  M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (min (↑n : ℕ) (↑m : ℕ)) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
rw₆ :
  M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑m : ℕ) x)
rw₇ rw₈ : M.evalFrom s (List.take (↑m : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))

Tactic:
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]

Premises used: DFA.evalFrom_of_append, List.take_append_drop, min_eq_left, List.take_take
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))

Tactic:
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]
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
right : M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
      M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)) ∧
    M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t

Tactic:
use hq
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))
right :
  M.evalFrom
      (M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑m : ℕ) x) =
    t
right₁ :
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)))
      (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
    t
right₂ :
  M.evalFrom s
      (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++
        (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x)) =
    t
right₃ :
  M.evalFrom s
      (List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x) =
    t
right₄ : M.evalFrom s (List.take (↑m : ℕ) x ++ List.drop (↑m : ℕ) x) = t
right₅ right₆ right₇ right₈ : M.evalFrom s x = t
⊢ M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t

Tactic:
rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]

Premises used: DFA.evalFrom_of_append, List.append_assoc, List.take_append_drop
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : M.evalFrom s x = s
hy : Membership.mem (γ := Language α) {x}∗ y
⊢ ∃ (L : List (List α)), y = L.flatten ∧ ∀ y ∈ L, Membership.mem (γ := Language α) {x} y

Tactic:
rw [Language.mem_kstar] at hy

Premises used: Language.mem_kstar
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : M.evalFrom s x = s
hy : ∃ (L : List (List α)), y = L.flatten ∧ ∀ y ∈ L, Membership.mem (γ := Language α) {x} y
rcases : ∀ (S : List (List α)) (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
⊢ M.evalFrom s y = s

Tactic:
rcases hy with ⟨S, rfl, hS⟩

Premises used: rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
hS : ∀ (y : List α), Membership.mem (γ := List (List α)) [] y → Membership.mem (γ := Language α) {x} y
⊢ M.evalFrom s (List.flatten []) = s

Tactic:
rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
⊢ Membership.mem (γ := Language α) {x} a

Tactic:
have ha := hS a List.mem_cons_self
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : Membership.mem (γ := Language α) {x} a
⊢ a = x

Tactic:
rw [Set.mem_singleton_iff] at ha

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : a = x
cons : M.evalFrom s S.flatten = s
⊢ M.evalFrom s (a :: S).flatten = s

Tactic:
rw [List.flatten_cons, evalFrom_of_append, ha, hx]

Premises used: DFA.evalFrom_of_append, List.flatten_cons
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : a = x
cons : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y
⊢ M.evalFrom s S.flatten = s

Tactic:
apply ih
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : a = x
z : List α
hz : z ∈ S
⊢ Membership.mem (γ := Language α) {x} z

Tactic:
hS z (List.mem_cons_of_mem a hz)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y
ha : a = x
z : List α
hz : z ∈ S
⊢ Membership.mem (γ := Language α) {x} z

Tactic:
exact hS z (List.mem_cons_of_mem a hz)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
S : List (List α)
hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y
nil :
  ∀ (hS : ∀ (y : List α), Membership.mem (γ := List (List α)) [] y → Membership.mem (γ := Language α) {x} y),
    M.evalFrom s (List.flatten []) = s
cons :
  ∀ (a : List α) (S : List (List α))
    (ih : ∀ (hS : ∀ y ∈ S, Membership.mem (γ := Language α) {x} y), M.evalFrom s S.flatten = s)
    (hS : ∀ y ∈ a :: S, Membership.mem (γ := Language α) {x} y), M.evalFrom s (a :: S).flatten = s
⊢ M.evalFrom s S.flatten = s

Tactic:
induction S with
  | nil => rfl
  | cons a S ih =>
    have ha := hS a List.mem_cons_self
    rw [Set.mem_singleton_iff] at ha
    rw [List.flatten_cons, evalFrom_of_append, ha, hx]
    apply ih
    intro z hz
    exact hS z (List.mem_cons_of_mem a hz)

Premises used: DFA.evalFrom_of_append, Set.mem_singleton_iff, List.flatten_cons
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card σ ≤ x.length
obtain :
  ∀ (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 : List α) (b : List α) (c : List α),
      x = a ++ b ++ c ∧
        a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts

Tactic:
obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split (s := M.start) hlen rfl

Premises used: DFA.evalFrom_split, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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
right : HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts

Tactic:
use a, b, c, hx, hlen, hnil
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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 ∈ HMul.hMul (α := Language α) {a} {b}∗ * {c}
⊢ ∃ a_1 ∈ HMul.hMul (α := Language α) {a} {b}∗, ∃ (b : List α), Membership.mem (γ := Language α) {c} b ∧ a_1 ++ b = y

Tactic:
rw [Language.mem_mul] at hy

Premises used: Language.mem_mul
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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 ∈ HMul.hMul (α := Language α) {a} {b}∗, ∃ (b : List α), Membership.mem (γ := Language α) {c} b ∧ a_1 ++ b = y
right :
  ∀ (ab : List α) (hab : ab ∈ HMul.hMul (α := Language α) {a} {b}∗) (c' : List α)
    (hc' : Membership.mem (γ := Language α) {c} c'), ab ++ c' ∈ M.accepts
⊢ y ∈ M.accepts

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

Premises used: rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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 ∈ HMul.hMul (α := Language α) {a} {b}∗
c' : List α
hc' : Membership.mem (γ := Language α) {c} c'
right :
  ∀
    (hab :
      ∃ (a_1 : List α),
        Membership.mem (γ := Language α) {a} a_1 ∧
          ∃ (b_1 : List α), Membership.mem (γ := Language α) {b}∗ b_1 ∧ a_1 ++ b_1 = ab)
    (c' : List α) (hc' : Membership.mem (γ := Language α) {c} c'), ab ++ c' ∈ M.accepts
⊢ ab ++ c' ∈ M.accepts

Tactic:
rw [Language.mem_mul] at hab

Premises used: Language.mem_mul
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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 :
  ∃ (a_1 : List α),
    Membership.mem (γ := Language α) {a} a_1 ∧
      ∃ (b_1 : List α), Membership.mem (γ := Language α) {b}∗ b_1 ∧ a_1 ++ b_1 = ab
c' : List α
hc' : Membership.mem (γ := Language α) {c} c'
right :
  ∀ (a' : List α) (ha' : Membership.mem (γ := Language α) {a} a') (b' : List α)
    (hb' : Membership.mem (γ := Language α) {b}∗ b'), a' ++ b' ++ c' ∈ M.accepts
⊢ ab ++ c' ∈ M.accepts

Tactic:
rcases hab with ⟨a', ha', b', hb', rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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' : Membership.mem (γ := Language α) {c} c'
a' : List α
ha' : Membership.mem (γ := Language α) {a} a'
b' : List α
hb' : Membership.mem (γ := Language α) {b}∗ b'
right :
  ∀ (hc' : c' = c) (a' : List α) (ha' : a' = a) (b' : List α) (hb' : Membership.mem (γ := Language α) {b}∗ b'),
    a' ++ b' ++ c' ∈ M.accepts
⊢ a' ++ b' ++ c' ∈ M.accepts

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

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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' : Membership.mem (γ := Language α) {b}∗ b'
⊢ a'.length + b.length ≤ Fintype.card σ

Tactic:
substs ha' hc'
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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' : Membership.mem (γ := Language α) {b}∗ b'
hlen₁ : a'.length + b.length ≤ Fintype.card σ
⊢ M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'

Tactic:
substs ha' hc'
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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' : Membership.mem (γ := Language α) {b}∗ b'
hlen₁ : a'.length + b.length ≤ Fintype.card σ
hb₁ : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'
⊢ x = a' ++ b ++ c'

Tactic:
substs ha' hc'
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : 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' : Membership.mem (γ := Language α) {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'
⊢ M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x

Tactic:
substs ha' hc'
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {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
⊢ M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'

Tactic:
have h := M.evalFrom_of_pow hb hb'
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
hx_1 : x ∈ M.accepts
hlen_1 : Fintype.card σ ≤ x.length
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : Membership.mem (γ := Language α) {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'
right : M.eval (a' ++ b' ++ c') ∈ M.accept
right₁ : M.evalFrom M.start (a' ++ b' ++ c') ∈ M.accept
right₂ : M.evalFrom (M.evalFrom M.start (a' ++ b')) c' ∈ M.accept
right₃ : M.evalFrom (M.evalFrom (M.evalFrom M.start a') b') c' ∈ M.accept
right₄ : M.evalFrom (M.evalFrom M.start a') c' ∈ M.accept
right₅ right₆ right₇ right₈ : M.evalFrom M.start x ∈ M.accept
⊢ a' ++ b' ++ c' ∈ M.accepts

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

Premises used: DFA.evalFrom_of_append, DFA.eval, DFA.mem_accepts
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ comap id M = M

Tactic:
rfl

Premises used: DFA.comap, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
s : σ
⊢ (comap f M).evalFrom s [] = M.evalFrom s (List.map f [])

Tactic:
simp