awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : ∃ (S : List (List α)), u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hwf : u.length < (a :: x).length
mp :
  ∀ (S' : List (List α)) (hsum : u = S'.flatten) (helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true),
    ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
rcases hu with ⟨S', hsum, helem⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
h : a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
⊢ ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
use (a :: t) :: S'

Premises used: List.cons
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
h : a :: x = ((a :: t) :: S').flatten
h₁ : ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true
⊢ a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true

Tactic:
constructor
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: x = ((a :: t) :: S').flatten

Tactic:
simp [hs, hsum]
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
h : (P.deriv a).rmatch t = true
⊢ a :: t ≠ [] ∧ P.rmatch (a :: t) = true

Tactic:
simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]

Premises used: reduceCtorEq, RegularExpression.rmatch, ne_eq, not_false_iff, true_and
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
ht
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ (P.deriv a).rmatch t = true

Tactic:
exact ht
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
t' : List α
ht' : Mem t' S'
⊢ t' ≠ [] ∧ P.rmatch t' = true

Tactic:
helem t' ht'
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
t' : List α
ht' : Mem t' S'
⊢ t' ≠ [] ∧ P.rmatch t' = true

Tactic:
exact helem t' ht'
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
t' : List α
ht' : t' ∈ (a :: t) :: S'
h : a :: t ≠ [] ∧ P.rmatch (a :: t) = true
h₁ : ∀ (ht' : Mem t' S'), t' ≠ [] ∧ P.rmatch t' = true
⊢ t' ≠ [] ∧ P.rmatch t' = true

Tactic:
cases ht' with
          | head ht' =>
            simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
            exact ht
          | tail _ ht' => exact helem t' ht'

Premises used: List.head, reduceCtorEq, RegularExpression.rmatch, ne_eq, List.tail, not_false_iff, true_and
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < x.length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
S : List (List α)
hsum : x = S.flatten
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
mpr :
  ∀
    (IH :
      ∀ (t : List α) (_h : t.length < length.{u_1} (α := α) []),
        P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
    (hsum : [] = S.flatten), P.star.rmatch [] = true
mpr₁ :
  ∀ (a : α) (x : List α)
    (IH :
      ∀ (t : List α) (_h : t.length < (a :: x).length),
        P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
    (hsum : a :: x = S.flatten), P.star.rmatch (a :: x) = true
⊢ P.star.rmatch x = true

Tactic:
rcases x with - | ⟨a, x⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
IH :
  ∀ (t : List α) (_h : t.length < length.{u_1} (α := α) []),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hsum : [] = S.flatten
⊢ P.star.rmatch [] = true

Tactic:
rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = S.flatten
mpr : ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
⊢ P.star.rmatch (a :: x) = true

Tactic:
rw [rmatch, deriv, mul_rmatch_iff]

Premises used: RegularExpression.rmatch, RegularExpression.deriv, RegularExpression.mul_rmatch_iff
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
S : List (List α)
helem : ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = S.flatten
mpr :
  ∀ (helem : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true)
    (hsum : a :: x = flatten []),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
mpr₁ :
  ∀ (t' : List α) (U : List (List α)) (helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true)
    (hsum : a :: x = (t' :: U).flatten),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
rcases S with - | ⟨t', U⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
helem : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = flatten []
⊢ x = HAppend.hAppend (α := List α) [] [] ∧ (P.deriv a).rmatch [] = true ∧ P.star.rmatch [] = true

Tactic:
tauto
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
helem : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = flatten []
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
exact ⟨[], [], by tauto⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
t' : List α
U : List (List α)
helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = (t' :: U).flatten
mpr :
  ∀ (helem : ∀ t ∈ [] :: U, t ≠ [] ∧ P.rmatch t = true) (hsum : a :: x = ([] :: U).flatten),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
mpr₁ :
  ∀ (b : α) (t : List α) (helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true)
    (hsum : a :: x = ((b :: t) :: U).flatten),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
obtain - | ⟨b, t⟩ := t'
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
helem : ∀ t ∈ [] :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = ([] :: U).flatten
⊢ (Ne.{u_1 + 1} (α := List α) [] [] ∧ P.rmatch [] = true) ∧ ∀ a ∈ U, a ≠ [] ∧ P.rmatch a = true

Tactic:
simp only [forall_eq_or_imp, List.mem_cons] at helem

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
hsum : a :: x = ([] :: U).flatten
helem : (Ne.{u_1 + 1} (α := List α) [] [] ∧ P.rmatch [] = true) ∧ ∀ a ∈ U, a ≠ [] ∧ P.rmatch a = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
simp only [not_true, Ne, false_and] at helem

Premises used: false_and, Ne, not_true
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a :: x = ((b :: t) :: U).flatten
⊢ a = b ∧ x = t ++ U.flatten

Tactic:
simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum

Premises used: List.cons_eq_cons, List.flatten_cons, List.cons_append
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
⟨t, U.flatten, hsum.2, ?_, ?_⟩

Premises used: And.right, And.intro, Exists.intro, List.flatten
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
mpr : (P.deriv a).rmatch t = true
mpr₁ : P.star.rmatch U.flatten = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ b :: t ∈ (b :: t) :: U

Tactic:
simp
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ b :: t ≠ [] ∧ P.rmatch (b :: t) = true

Tactic:
specialize helem (b :: t) (by simp)

Premises used: List.cons
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ P.rmatch (b :: t) = true
⊢ b :: t ≠ [] ∧ (P.deriv b).rmatch t = true

Tactic:
rw [rmatch] at helem

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
⊢ (P.deriv b).rmatch t = true

Tactic:
helem.2

Premises used: And.right
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
h : a = b
⊢ (P.deriv a).rmatch t = true

Tactic:
convert! helem.2

Premises used: And.right
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
hsum.1

Premises used: And.left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ U.flatten
helem : b :: t ≠ [] ∧ (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact hsum.1

Premises used: And.left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α) (_h : t.length < (a :: x).length),
    P.star.rmatch t = true ↔ ∃ (S : List (List α)), t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ P.star.rmatch U.flatten = true

Tactic:
grind
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
zero : false = true ↔ Membership.mem (γ := Language α) (matches' 0) x
⊢ rmatch RegularExpression.zero x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.zero) x

Tactic:
rw [zero_def, zero_rmatch]

Premises used: RegularExpression.zero_rmatch, RegularExpression.zero_def
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
zero : false = true → Membership.mem (γ := Language α) (matches' 0) x
zero₁ : Membership.mem (γ := Language α) (matches' 0) x → false = true
zero₂ : false = true → Membership.mem (γ := Language α) (matches' 0) x
zero₃ : Membership.mem (γ := Language α) (matches' 0) x → false = true
⊢ false = true ↔ Membership.mem (γ := Language α) (matches' 0) x

Tactic:
tauto
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
epsilon : rmatch 1 x = true ↔ Membership.mem (γ := Language α) (matches' 1) x
epsilon₁ : x = [] ↔ Membership.mem (γ := Language α) (matches' 1) x
epsilon₂ : x = [] ↔ Membership.mem (γ := Language α) 1 x
epsilon₃ epsilon₄ : x = [] ↔ x = []
⊢ rmatch RegularExpression.epsilon x = true ↔ Membership.mem (γ := Language α) (matches' RegularExpression.epsilon) x

Tactic:
rw [one_def, one_rmatch_iff, matches'_epsilon, Language.mem_one]

Premises used: Language.mem_one, RegularExpression.one_def, RegularExpression.one_rmatch_iff, RegularExpression.matches'_epsilon
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
char : x = [a] ↔ x ∈ (RegularExpression.char a).matches'
⊢ (RegularExpression.char a).rmatch x = true ↔ x ∈ (RegularExpression.char a).matches'

Tactic:
rw [char_rmatch_iff]

Premises used: RegularExpression.char_rmatch_iff
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
⊢ x = [a] ↔ x ∈ (char a).matches'

Tactic:
rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : RegularExpression α
ih₁ : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches'
ih₂ : ∀ (x : List α), a_1.rmatch x = true ↔ x ∈ a_1.matches'
x : List α
plus : x ∈ a.matches' ∨ x ∈ a_1.matches' ↔ x ∈ (a + a_1).matches'
⊢ (a.plus a_1).rmatch x = true ↔ x ∈ (a.plus a_1).matches'

Tactic:
rw [plus_def, add_rmatch_iff, ih₁, ih₂]

Premises used: RegularExpression.plus_def, RegularExpression.add_rmatch_iff
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : RegularExpression α
ih₁ : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches'
ih₂ : ∀ (x : List α), a_1.rmatch x = true ↔ x ∈ a_1.matches'
x : List α
⊢ x ∈ a.matches' ∨ x ∈ a_1.matches' ↔ x ∈ (a + a_1).matches'

Tactic:
rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
comp :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔
    ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
⊢ (P.comp Q).rmatch x = true ↔ x ∈ (P.comp Q).matches'

Tactic:
simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]

Premises used: RegularExpression.matches'_mul, RegularExpression.comp_def, Language.mem_mul, RegularExpression.mul_rmatch_iff
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : RegularExpression α
ih : ∀ (x : List α), a.rmatch x = true ↔ x ∈ a.matches'
x : List α
⊢ a.star.rmatch x = true ↔ x ∈ a.star.matches'

Tactic:
simp only [star_rmatch_iff, matches'_star, ih, Language.mem_kstar_iff_exists_nonempty, and_comm]

Premises used: Language.mem_kstar_iff_exists_nonempty, and_comm, RegularExpression.matches'_star, RegularExpression.star_rmatch_iff