awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch (a :: x) = true
h : a :: x = u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true

Tactic:
exact hQ
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
pos : ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
    (Q.deriv a).rmatch x = true

Tactic:
left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ a = b ∧ x = t ++ u

Tactic:
rw [List.cons_append, List.cons_eq_cons] at h

Premises used: List.cons_eq_cons, List.cons_append
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
h₁ : a = b ∧ x = t ++ u
⊢ P.rmatch (b :: t) = true

Tactic:
rw [List.cons_append, List.cons_eq_cons] at h

Premises used: List.cons_eq_cons, List.cons_append
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
⟨t, u, h.2, ?_, hQ⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
pos : (P.deriv a).rmatch t = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨t, u, h.2, ?_, hQ⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ (P.deriv b).rmatch t = true

Tactic:
rw [rmatch] at hP

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv b).rmatch t = true

Tactic:
hP
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
h₁ : a = b
⊢ (P.deriv a).rmatch t = true

Tactic:
convert! hP
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
neg :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [ih]
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
neg :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) →
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
neg₁ :
  (∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
constructor
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
left : a :: x = a :: t ++ u
right : P.rmatch (a :: t) = true
right₁ : Q.rmatch u = true
left₁ left₂ left₃ left₄ left₅ : a :: x = a :: t ++ u
⊢ a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true

Tactic:
tauto
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : x = t ++ u
hP : (P.deriv a).rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
exact ⟨a :: t, u, by tauto⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
neg :
  ∀ (h : a :: x = [] ++ u) (hP : P.rmatch [] = true),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
neg₁ :
  ∀ (b : α) (t : List α) (h : a :: x = b :: t ++ u) (hP : P.rmatch (b :: t) = true),
    ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
rcases t with - | ⟨b, t⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
contradiction
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ a = b ∧ x = t ++ u

Tactic:
rw [List.cons_append, List.cons_eq_cons] at h

Premises used: List.cons_eq_cons, List.cons_append
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
h₁ : a = b ∧ x = t ++ u
⊢ P.rmatch (b :: t) = true

Tactic:
rw [List.cons_append, List.cons_eq_cons] at h

Premises used: List.cons_eq_cons, List.cons_append
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
⟨t, u, h.2, ?_, hQ⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
neg : (P.deriv a).rmatch t = true
⊢ ∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨t, u, h.2, ?_, hQ⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ (P.deriv b).rmatch t = true

Tactic:
rw [rmatch] at hP

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ (P.deriv b).rmatch t = true

Tactic:
hP
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
h₁ : a = b
⊢ (P.deriv a).rmatch t = true

Tactic:
convert! hP
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
ih :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
x : List α
nil :
  ∀ (P Q : RegularExpression α),
    (P * Q).rmatch [] = true ↔ ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
cons :
  ∀ (a : α) (x : List α)
    (ih :
      ∀ (P Q : RegularExpression α),
        (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true)
    (P Q : RegularExpression α),
    (P * Q).rmatch (a :: x) = true ↔
      ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P * Q).rmatch x = true ↔ ∃ (t : List α) (u : List α), x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
induction x generalizing P Q with
  | nil =>
    rw [rmatch]; simp only [matchEpsilon]
    constructor
    · intro h
      refine ⟨[], [], rfl, ?_⟩
      rw [rmatch, rmatch]
      rwa [Bool.and_eq_true_iff] at h
    · rintro ⟨t, u, h₁, h₂⟩
      obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm
      repeat rw [rmatch] at h₂
      simp [h₂]
  | cons a x ih =>
    rw [rmatch]; simp only [deriv]
    split_ifs with hepsilon
    · rw [add_rmatch_iff, ih]
      constructor
      · rintro (⟨t, u, _⟩ | h)
        · exact ⟨a :: t, u, by tauto⟩
        · exact ⟨[], a :: x, rfl, hepsilon, h⟩
      · rintro ⟨t, u, h, hP, hQ⟩
        rcases t with - | ⟨b, t⟩
        · right
          rw [List.nil_append] at h
          rw [← h] at hQ
          exact hQ
        · left
          rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1
    · rw [ih]
      constructor <;> rintro ⟨t, u, h, hP, hQ⟩
      · exact ⟨a :: t, u, by tauto⟩
      · rcases t with - | ⟨b, t⟩
        · contradiction
        · rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1

Premises used: RegularExpression.rmatch, RegularExpression.matchEpsilon, List.cons, Bool.and_eq_true_iff, RegularExpression.deriv, List.cons_eq_cons, List.nil_append, RegularExpression.add_rmatch_iff, List.cons_append, rfl, List.nil
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
x : List α
⊢ ∀ (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

Tactic:
have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
-- 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
mp : P.star.rmatch x = true → ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
mpr : (∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true) → P.star.rmatch x = true
⊢ P.star.rmatch x = true ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
constructor
-- 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
mp :
  ∀
    (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),
    P.star.rmatch [] = true → ∃ (S : List (List α)), [] = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
mp₁ :
  ∀ (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),
    P.star.rmatch (a :: x) = true → ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ P.star.rmatch x = true → ∃ (S : List (List α)), x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
rcases x with - | ⟨a, x⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
h :
  Eq.{u_1 + 1} (α := List α) [] (flatten []) ∧
    ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t ≠ [] ∧ P.rmatch t = true
⊢ ∃ (S : List (List α)), [] = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
use []
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
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
_h : P.star.rmatch [] = true
h : Eq.{u_1 + 1} (α := List α) [] []
h₁ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
h₂ h₃ h₄ : Eq.{u_1 + 1} (α := List α) [] []
h₅ h₆ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = true
h₇ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = []
h₈ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → P.rmatch t = true
h₉ h₁₀ h₁₁ : Eq.{u_1 + 1} (α := List α) [] []
h₁₂ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → t = [] → False
h₁₃ : ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → P.rmatch t = true
h₁₄ h₁₅ h₁₆ h₁₇ : Eq.{u_1 + 1} (α := List α) [] []
⊢ Eq.{u_1 + 1} (α := List α) [] [] ∧
    ∀ (t : List α), Membership.mem (γ := List (List α)) [] t → ¬t = [] ∧ P.rmatch t = 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
mp :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true) →
    ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ P.star.rmatch (a :: x) = true → ∃ (S : List (List α)), a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = 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 α
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 : P.star.rmatch u = true
rw : u.length < t.length + u.length + 1
⊢ u.length < (a :: x).length

Tactic:
rw [hs, List.length_cons, List.length_append]

Premises used: List.length_cons, List.length_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
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hu : P.star.rmatch u = true
⊢ u.length < t.length + u.length + 1

Tactic:
lia
-- 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 : P.star.rmatch u = true
⊢ u.length < (a :: x).length

Tactic:
have hwf : u.length < (List.cons a x).length := by
          rw [hs, List.length_cons, List.length_append]
          lia
-- 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 : P.star.rmatch u = true
hwf : u.length < (a :: x).length
⊢ ∃ (S : List (List α)), u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
rw [IH _ hwf] at hu
-- 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 : P.star.rmatch u = true
hwf : u.length < (a :: x).length
hu₁ : ∃ (S : List (List α)), u = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
⊢ u.length < (a :: x).length

Tactic:
rw [IH _ hwf] at hu