awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
refl : Relation.ReflTransGen g.Produces (v ++ p) (v ++ p)
tail :
  ∀ {b c : List (Symbol T g.NT)},
    Relation.ReflTransGen g.Produces v b →
      ∀ (last : g.Produces b c) (ih : g.Derives (v ++ p) (b ++ p)), g.Derives (v ++ p) (c ++ p)
⊢ g.Derives (v ++ p) (w ++ p)

Tactic:
induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_right p

Premises used: ContextFreeGrammar.Derives.refl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hguv : g.Produces u v
obtain :
  ∀ (w : ContextFreeRule T g.NT) (l : w ∈ g.rules) (r : w.Rewrites u v), ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u
⊢ ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u

Tactic:
obtain ⟨w, l, r⟩ := hguv
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
w : ContextFreeRule T g.NT
l : w ∈ g.rules
r : w.Rewrites u v
⊢ ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u

Tactic:
⟨w, l, r.nonterminal_input_mem⟩

Premises used: And.intro, Exists.intro, ContextFreeRule.Rewrites.nonterminal_input_mem
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
w : ContextFreeRule T g.NT
l : w ∈ g.rules
r : w.Rewrites u v
⊢ ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u

Tactic:
exact ⟨w, l, r.nonterminal_input_mem⟩
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
rw : ¬([Symbol.nonterminal t] = s ∨ ∃ (v : List (Symbol T g.NT)), g.Produces [Symbol.nonterminal t] v ∧ g.Derives v s)
⊢ ¬g.Derives [Symbol.nonterminal t] s

Tactic:
rw [derives_iff_eq_or_head]

Premises used: ContextFreeGrammar.derives_iff_eq_or_head
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
push :
  [Symbol.nonterminal t] ≠ s ∧ ∀ (v : List (Symbol T g.NT)) (_ : g.Produces [Symbol.nonterminal t] v), ¬g.Derives v s
⊢ ¬([Symbol.nonterminal t] = s ∨ ∃ (v : List (Symbol T g.NT)), g.Produces [Symbol.nonterminal t] v ∧ g.Derives v s)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ [Symbol.nonterminal t] ≠ s ∧ ∀ (v : List (Symbol T g.NT)) (_ : g.Produces [Symbol.nonterminal t] v), ¬g.Derives v s

Tactic:
⟨hs.symm, fun _ hx ↦ ?_⟩

Premises used: Ne.symm, And.intro
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
refine : ∀ (x : List (Symbol T g.NT)) (hx : g.Produces [Symbol.nonterminal t] x), ¬g.Derives x s
⊢ [Symbol.nonterminal t] ≠ s ∧ ∀ (v : List (Symbol T g.NT)) (_ : g.Produces [Symbol.nonterminal t] v), ¬g.Derives v s

Tactic:
refine ⟨hs.symm, fun _ hx ↦ ?_⟩
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x
⊢ ∃ r ∈ g.rules, Membership.mem (γ := List (Symbol T g.NT)) [Symbol.nonterminal t] (Symbol.nonterminal r.input)

Tactic:
have hxr := hx.exists_nonterminal_input_mem
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x
hxr : ∃ r ∈ g.rules, Membership.mem (γ := List (Symbol T g.NT)) [Symbol.nonterminal t] (Symbol.nonterminal r.input)
⊢ ∃ r ∈ g.rules, r.input = t

Tactic:
simp_rw [List.mem_singleton, Symbol.nonterminal.injEq] at hxr

Premises used: List.mem_singleton, Symbol.nonterminal.injEq
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x
hxr : ∃ r ∈ g.rules, r.input = t
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : g.Derives x s → ∀ w ∈ g.rules, w.input = t → False
⊢ ¬g.Derives x s

Tactic:
tauto
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
hg : ∀ r ∈ g.rules, r.input ≠ g.initial
h : ∀ (x : List T), x ∈ g.language ↔ Membership.mem (γ := Language T) 0 x
⊢ g.language = 0

Tactic:
ext
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
hg : ∀ r ∈ g.rules, r.input ≠ g.initial
x : List T
⊢ x ∈ g.language ↔ Membership.mem (γ := Language T) 0 x

Tactic:
simp +contextual [derives_nonterminal, hg]

Premises used: ContextFreeGrammar.derives_nonterminal
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
⊢ r.reverse.reverse = r

Tactic:
simp [reverse]

Premises used: ContextFreeRule.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
h : ∀ (x : ContextFreeRule T N), (reverse ∘ reverse) x = id x
⊢ Eq (α := ContextFreeRule T N → ContextFreeRule T N) (reverse ∘ reverse) id

Tactic:
ext : 1
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
x : ContextFreeRule T N
⊢ (reverse ∘ reverse) x = id x

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
⊢ Involutive (α := ContextFreeRule T N) reverse

Tactic:
reverse_reverse

Premises used: ContextFreeRule.reverse_reverse, Function.Involutive
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
⊢ Bijective (α := ContextFreeRule T N) reverse

Tactic:
reverse_involutive.bijective

Premises used: Function.Involutive.bijective, ContextFreeRule.reverse_involutive
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
⊢ Injective (α := ContextFreeRule T N) reverse

Tactic:
reverse_bijective.injective

Premises used: Function.Bijective.injective, ContextFreeRule.reverse_bijective
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
⊢ Surjective (α := ContextFreeRule T N) reverse

Tactic:
reverse_bijective.surjective

Premises used: Function.Bijective.surjective, ContextFreeRule.reverse_bijective
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
s : List (Symbol T N)
⊢ r.reverse.Rewrites (Symbol.nonterminal r.input :: s).reverse (r.output ++ s).reverse

Tactic:
simpa using .append_left .input_output _
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
x : Symbol T N
u v : List (Symbol T N)
h : r.Rewrites u v
⊢ r.reverse.Rewrites (x :: u).reverse (x :: v).reverse

Tactic:
simpa using h.reverse.append_right _

Premises used: ContextFreeRule.Rewrites.append_right
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
h : r.reverse.Rewrites u.reverse v.reverse
⊢ r.Rewrites u v

Tactic:
simpa using h.reverse

Premises used: ContextFreeRule.Rewrites.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
rw : r.reverse.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u.reverse v.reverse
rw₁ rw₂ : r.Rewrites u.reverse v.reverse ↔ r.Rewrites u.reverse v.reverse
⊢ r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse

Tactic:
rw [← rewrites_reverse, reverse_reverse]

Premises used: ContextFreeRule.reverse_reverse, ContextFreeRule.rewrites_reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
⊢ Eq.{max 2 (u_1 + 1)} g.reverse.reverse g

Tactic:
simp [reverse, Finset.map_map]

Premises used: ContextFreeGrammar.reverse, Finset.map_map
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
⊢ Involutive.{max 2 (u_1 + 1)} (α := ContextFreeGrammar T) reverse

Tactic:
reverse_reverse

Premises used: ContextFreeGrammar.reverse_reverse, Function.Involutive
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
⊢ Bijective.{max 2 (u_1 + 1), max 2 (u_1 + 1)} (α := ContextFreeGrammar T) reverse

Tactic:
reverse_involutive.bijective

Premises used: ContextFreeGrammar.reverse_involutive, Function.Involutive.bijective
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
⊢ Injective.{max 2 (u_1 + 1), max 2 (u_1 + 1)} (α := ContextFreeGrammar T) reverse

Tactic:
reverse_bijective.injective

Premises used: Function.Bijective.injective, ContextFreeGrammar.reverse_bijective
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
⊢ Surjective.{max 2 (u_1 + 1), max 2 (u_1 + 1)} (α := ContextFreeGrammar T) reverse

Tactic:
reverse_bijective.surjective

Premises used: Function.Bijective.surjective, ContextFreeGrammar.reverse_bijective
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ ∀ (a : ContextFreeRule T g.reverse.NT),
    a ∈ g.reverse.rules ∧ a.Rewrites u.reverse v.reverse ↔
      Membership.mem (α := ContextFreeRule T g.NT) g.rules
          ((Equiv.ofBijective ContextFreeRule.reverse ⋯ :
                (a : ContextFreeRule T g.reverse.NT) → ContextFreeRule T g.reverse.NT)
              a :
            ContextFreeRule T g.reverse.NT) ∧
        ContextFreeRule.Rewrites
          ((Equiv.ofBijective ContextFreeRule.reverse ⋯ :
              (a : ContextFreeRule T g.reverse.NT) → ContextFreeRule T g.reverse.NT)
            a)
          u v

Tactic:
simp [ContextFreeRule.reverse_involutive.eq_iff]

Premises used: Function.Involutive.eq_iff, ContextFreeRule.reverse_involutive
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ ∀ (a : ContextFreeRule T g.reverse.NT),
    a ∈ g.reverse.rules ∧ a.Rewrites u v ↔
      Membership.mem (α := ContextFreeRule T g.NT) g.rules
          ((Equiv.ofBijective ContextFreeRule.reverse ⋯ :
                (a : ContextFreeRule T g.reverse.NT) → ContextFreeRule T g.reverse.NT)
              a :
            ContextFreeRule T g.reverse.NT) ∧
        ContextFreeRule.Rewrites
          ((Equiv.ofBijective ContextFreeRule.reverse ⋯ :
              (a : ContextFreeRule T g.reverse.NT) → ContextFreeRule T g.reverse.NT)
            a)
          u.reverse v.reverse

Tactic:
simp [ContextFreeRule.reverse_involutive.eq_iff]

Premises used: Function.Involutive.eq_iff, ContextFreeRule.reverse_involutive
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ Relation.ReflTransGen g.reverse.Produces u.reverse u.reverse

Tactic:
rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v b c : List (Symbol T g.NT)
h : Relation.ReflTransGen g.Produces u b
orig : g.Produces b c
ih : g.reverse.Derives u.reverse b.reverse
⊢ g.reverse.Derives u.reverse c.reverse

Tactic:
ih.trans_produces orig.reverse

Premises used: ContextFreeGrammar.Derives.trans_produces, ContextFreeGrammar.Produces.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v b c : List (Symbol T g.NT)
h : Relation.ReflTransGen g.Produces u b
orig : g.Produces b c
ih : g.reverse.Derives u.reverse b.reverse
⊢ g.reverse.Derives u.reverse c.reverse

Tactic:
exact ih.trans_produces orig.reverse

Premises used: ContextFreeGrammar.Derives.trans_produces, ContextFreeGrammar.Produces.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hg : g.Derives u v
refl : Relation.ReflTransGen g.reverse.Produces u.reverse u.reverse
tail :
  ∀ {b c : List (Symbol T g.NT)},
    Relation.ReflTransGen g.Produces u b →
      ∀ (orig : g.Produces b c) (ih : g.reverse.Derives u.reverse b.reverse), g.reverse.Derives u.reverse c.reverse
⊢ g.reverse.Derives u.reverse v.reverse

Tactic:
induction hg with
  | refl => rfl
  | tail _ orig ih => exact ih.trans_produces orig.reverse

Premises used: ContextFreeGrammar.Derives.refl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ g.reverse.reverse.Derives u.reverse.reverse v.reverse.reverse

Tactic:
h.reverse

Premises used: ContextFreeGrammar.Derives.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
h₁ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse
h₂ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse → u = u.reverse.reverse
h₃ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse → v = v.reverse.reverse
⊢ g.Derives u v

Tactic:
convert! h.reverse

Premises used: ContextFreeGrammar.Derives.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ Eq.{max 2 (u_1 + 1)} g g.reverse.reverse

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2 : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse
⊢ u = u.reverse.reverse

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2 : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse
⊢ v = v.reverse.reverse

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
rw : g.Derives u.reverse v.reverse ↔ g.reverse.Derives u v
rw₁ : g.reverse.Derives u.reverse.reverse v.reverse.reverse ↔ g.reverse.Derives u v
rw₂ : g.reverse.Derives u v.reverse.reverse ↔ g.reverse.Derives u v
rw₃ rw₄ : g.reverse.Derives u v ↔ g.reverse.Derives u v
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse

Tactic:
rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]

Premises used: iff_comm, List.reverse_reverse, ContextFreeGrammar.derives_reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u : List (Symbol T g.NT)
⊢ g.reverse.Generates u.reverse ↔ g.Generates u

Tactic:
simp [Generates]

Premises used: ContextFreeGrammar.Generates
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u : List (Symbol T g.NT)
⊢ g.reverse.Generates u ↔ g.Generates u.reverse

Tactic:
simp [Generates]

Premises used: ContextFreeGrammar.Generates
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
h : ∀ (x : List T), x ∈ g.reverse.language ↔ x ∈ g.language.reverse
⊢ g.reverse.language = g.language.reverse

Tactic:
ext
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
x : List T
⊢ x ∈ g.reverse.language ↔ x ∈ g.language.reverse

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
L : Language T
h : L.IsContextFree
rcases : ∀ (g : ContextFreeGrammar T), g.language.reverse.IsContextFree
⊢ L.reverse.IsContextFree

Tactic:
rcases h with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.language = g.language.reverse

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
⊢ g.language.reverse.IsContextFree

Tactic:
exact ⟨g.reverse, by simp⟩
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
L : Language T
h : L.reverse.IsContextFree
⊢ L.IsContextFree

Tactic:
simpa using h.reverse

Premises used: Language.IsContextFree.reverse
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
L : Language T
⊢ L.reverse.IsContextFree ↔ L.IsContextFree

Tactic:
⟨.of_reverse, .reverse⟩

Premises used: Language.IsContextFree.of_reverse, Iff.intro, Language.IsContextFree.reverse
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
s : σ
⊢ M.evalFrom s [] = s

Tactic:
rfl

Premises used: DFA.evalFrom, List.foldl, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
s : σ
a : α
x : List α
⊢ M.evalFrom s (a :: x) = M.evalFrom (M.step s a) x

Tactic:
rfl

Premises used: DFA.evalFrom, List.foldl, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
s : σ
a : α
⊢ M.evalFrom s [a] = M.step s a

Tactic:
rfl

Premises used: DFA.evalFrom, List.foldl, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
a : α
⊢ M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a

Tactic:
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

Premises used: DFA.evalFrom, List.foldl_nil, List.foldl_append, List.foldl_cons
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ M.eval [] = M.start

Tactic:
rfl

Premises used: DFA.evalFrom, List.foldl, DFA.eval, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
a : α
⊢ M.eval [a] = M.step M.start a

Tactic:
rfl

Premises used: DFA.evalFrom, List.foldl, DFA.eval, rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
a : α
⊢ M.eval (x ++ [a]) = M.step (M.eval x) a

Tactic:
evalFrom_append_singleton _ _ _ _

Premises used: DFA.evalFrom_append_singleton, DFA.eval
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
start : σ
x y : List α
⊢ M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y

Tactic:
List.foldl_append

Premises used: DFA.evalFrom, List.foldl_append
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
⊢ x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept

Tactic:
rfl
-- Module: Mathlib.Computability.DFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts ↔ M.eval x ∈ M.accept

Tactic:
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
⊢ Fintype.card σ < Fintype.card (Fin (Fintype.card σ + 1))

Tactic:
simp
-- 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
obtain :
  ∀ (n m : Fin (Fintype.card σ + 1)) (hneq : n ≠ m)
    (heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)),
    ∃ (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
⊢ ∃ (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:
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 simp)

Premises used: Fintype.exists_ne_map_eq_of_card_lt, DFA.evalFrom, Fin.val, List.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)
inr :
  ∀
    (this :
      ∀ (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 : ℕ)),
        ∃ (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)
    (hle : ¬(↑n : ℕ) ≤ (↑m : ℕ)),
    ∃ (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
wlog :
  ∀ (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 : ℕ)),
    ∃ (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
⊢ ∃ (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:
wlog hle : (n : ℕ) ≤ m generalizing n m

Premises used: Fin.val
-- 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)
this :
  ∀ (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 : ℕ)),
    ∃ (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
hle : ¬(↑n : ℕ) ≤ (↑m : ℕ)
⊢ ∃ (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:
this m n hneq.symm heq.symm (le_of_not_ge hle)

Premises used: le_of_not_ge, Ne.symm, Eq.symm
-- 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)
this :
  ∀ (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 : ℕ)),
    ∃ (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
hle : ¬(↑n : ℕ) ≤ (↑m : ℕ)
⊢ ∃ (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:
exact this m n hneq.symm heq.symm (le_of_not_ge hle)

Premises used: le_of_not_ge, Ne.symm, Eq.symm
-- 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 s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)) = M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))

Tactic:
rfl