awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
P : RegularExpression α
⊢ P.star.matches' = P.matches'∗

Tactic:
rfl

Premises used: RegularExpression.matches', rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ deriv 0 a = 0

Tactic:
rfl

Premises used: RegularExpression.deriv, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ deriv 1 a = 0

Tactic:
rfl

Premises used: RegularExpression.deriv, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (char a).deriv a = 1

Tactic:
if_pos rfl

Premises used: if_pos, RegularExpression.deriv, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
a b : α
inst : DecidableEq α
h : a ≠ b
⊢ (char a).deriv b = 0

Tactic:
if_neg h

Premises used: RegularExpression.deriv, if_neg
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
a : α
⊢ (P + Q).deriv a = P.deriv a + Q.deriv a

Tactic:
rfl

Premises used: RegularExpression.deriv, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P : RegularExpression α
a : α
⊢ P.star.deriv a = P.deriv a * P.star

Tactic:
rfl

Premises used: RegularExpression.deriv, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
nil : rmatch.{u_1} (α := α) 0 [] = false
cons : ∀ (head : α) (tail : List α), rmatch 0 tail = false → rmatch 0 (head :: tail) = false
⊢ rmatch 0 x = false

Tactic:
induction x
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
⊢ rmatch.{u_1} (α := α) 0 [] = false

Tactic:
simp [rmatch, matchEpsilon, *]

Premises used: RegularExpression.rmatch, RegularExpression.matchEpsilon
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
tail_ih : rmatch 0 tail = false
⊢ rmatch 0 (head :: tail) = false

Tactic:
simp [rmatch, matchEpsilon, *]

Premises used: RegularExpression.rmatch, RegularExpression.matchEpsilon
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
nil : rmatch.{u_1} (α := α) 1 [] = true ↔ Eq.{u_1 + 1} (α := List α) [] []
cons :
  ∀ (head : α) (tail : List α),
    (rmatch 1 tail = true ↔ tail = []) → (rmatch 1 (head :: tail) = true ↔ head :: tail = [])
⊢ rmatch 1 x = true ↔ x = []

Tactic:
induction x
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
⊢ rmatch.{u_1} (α := α) 1 [] = true ↔ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
simp [rmatch, matchEpsilon, *]

Premises used: RegularExpression.rmatch, RegularExpression.matchEpsilon
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
tail_ih : rmatch 1 tail = true ↔ tail = []
⊢ rmatch 1 (head :: tail) = true ↔ head :: tail = []

Tactic:
simp [rmatch, matchEpsilon, *]

Premises used: RegularExpression.rmatch, RegularExpression.matchEpsilon
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
nil : (char a).rmatch [] = true ↔ [] = [a]
cons : ∀ (head : α) (x : List α), (char a).rmatch (head :: x) = true ↔ head :: x = [a]
⊢ (char a).rmatch x = true ↔ x = [a]

Tactic:
rcases x with - | ⟨_, x⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (char a).rmatch [] = true ↔ [] = [a]

Tactic:
of_decide_eq_true rfl

Premises used: of_decide_eq_true, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (char a).rmatch [] = true ↔ [] = [a]

Tactic:
exact of_decide_eq_true rfl

Premises used: of_decide_eq_true
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
x : List α
cons : (char a).rmatch [head] = true ↔ [head] = [a]
cons₁ : ∀ (head_1 : α) (tail : List α), (char a).rmatch (head :: head_1 :: tail) = true ↔ head :: head_1 :: tail = [a]
⊢ (char a).rmatch (head :: x) = true ↔ head :: x = [a]

Tactic:
rcases x with - | ⟨head, tail⟩

Premises used: List.head, List.tail
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
cons : rmatch.{u_1} (α := α) (if a = head then 1 else 0) [] = true ↔ head = a
⊢ (char a).rmatch [head] = true ↔ [head] = [a]

Tactic:
rw [rmatch, deriv, List.singleton_inj]

Premises used: List.singleton_inj, RegularExpression.rmatch, RegularExpression.deriv
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
cons : a = head → (rmatch.{u_1} (α := α) 1 [] = true ↔ head = a)
cons₁ : ¬a = head → (rmatch.{u_1} (α := α) 0 [] = true ↔ head = a)
⊢ rmatch.{u_1} (α := α) (if a = head then 1 else 0) [] = true ↔ head = a

Tactic:
split
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
h : a = head
cons : rmatch.{u_1} (α := α) 1 [] = true → head = a
cons₁ : head = a → rmatch.{u_1} (α := α) 1 [] = true
cons₂ cons₃ cons₄ : rmatch.{u_1} (α := α) 1 [] = true → head = a
cons₅ cons₆ cons₇ : head = a → rmatch.{u_1} (α := α) 1 [] = true
cons₈ cons₉ cons₁₀ : rmatch.{u_1} (α := α) 1 [] = true → head = a
cons₁₁ cons₁₂ cons₁₃ : head = a → rmatch.{u_1} (α := α) 1 [] = true
cons₁₄ cons₁₅ : rmatch.{u_1} (α := α) 1 [] = true → head = a
cons₁₆ : head = a → rmatch.{u_1} (α := α) 1 [] = true
⊢ rmatch.{u_1} (α := α) 1 [] = true ↔ head = a

Tactic:
tauto
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
h : ¬a = head
cons : rmatch.{u_1} (α := α) 0 [] = true → head = a
cons₁ : head = a → rmatch.{u_1} (α := α) 0 [] = true
cons₂ : rmatch.{u_1} (α := α) 0 [] = true → head = a
cons₃ cons₄ cons₅ cons₆ cons₇ cons₈ cons₉ cons₁₀ : head = a → rmatch.{u_1} (α := α) 0 [] = true
⊢ rmatch.{u_1} (α := α) 0 [] = true ↔ head = a

Tactic:
tauto
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
cons : (deriv (if a = head_1 then 1 else 0) head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
⊢ (char a).rmatch (head_1 :: head :: tail) = true ↔ head_1 :: head :: tail = [a]

Tactic:
rw [rmatch, rmatch, deriv, cons.injEq]

Premises used: RegularExpression.rmatch, List.cons.injEq, RegularExpression.deriv
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
cons : a = head_1 → ((deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = [])
cons₁ : ¬a = head_1 → ((deriv 0 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = [])
⊢ (deriv (if a = head_1 then 1 else 0) head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []

Tactic:
split
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : a = head_1
cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
cons₁ : false = true ↔ head_1 = a ∧ head :: tail = []
cons₂ : False ↔ head_1 = a ∧ False
⊢ (deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []

Tactic:
simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]

Premises used: reduceCtorEq, RegularExpression.deriv_one, and_false, RegularExpression.zero_rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : ¬a = head_1
cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
cons₁ : false = true ↔ head_1 = a ∧ head :: tail = []
cons₂ : False ↔ head_1 = a ∧ False
⊢ (deriv 0 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []

Tactic:
simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]

Premises used: reduceCtorEq, and_false, RegularExpression.zero_rmatch, RegularExpression.deriv_zero
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
⊢ (P + Q).rmatch [] = true ↔ P.rmatch [] = true ∨ Q.rmatch [] = true

Tactic:
simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]

Premises used: RegularExpression.rmatch, Bool.or_eq_true_iff, RegularExpression.matchEpsilon
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail = true ↔ P.rmatch tail = true ∨ Q.rmatch tail = true
P Q : RegularExpression α
cons :
  (P.deriv head + Q.deriv head).rmatch tail = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true
⊢ (P + Q).rmatch (head :: tail) = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true

Tactic:
rw [rmatch, deriv_add]

Premises used: RegularExpression.deriv_add, RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail = true ↔ P.rmatch tail = true ∨ Q.rmatch tail = true
P Q : RegularExpression α
⊢ (P.deriv head + Q.deriv head).rmatch tail = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true

Tactic:
ih _ _

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail = true ↔ P.rmatch tail = true ∨ Q.rmatch tail = true
P Q : RegularExpression α
⊢ (P.deriv head + Q.deriv head).rmatch tail = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true

Tactic:
exact ih _ _
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
x : List α
nil : ∀ (P Q : RegularExpression α), (P + Q).rmatch [] = true ↔ P.rmatch [] = true ∨ Q.rmatch [] = true
cons :
  ∀ (head : α) (tail : List α)
    (ih : ∀ (P Q : RegularExpression α), (P + Q).rmatch tail = true ↔ P.rmatch tail = true ∨ Q.rmatch tail = true)
    (P Q : RegularExpression α),
    (P + Q).rmatch (head :: tail) = true ↔ P.rmatch (head :: tail) = true ∨ Q.rmatch (head :: tail) = true
⊢ (P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true

Tactic:
induction x generalizing P Q with
  | nil => simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]
  | cons _ _ ih =>
    rw [rmatch, deriv_add]
    exact ih _ _

Premises used: RegularExpression.deriv_add, RegularExpression.rmatch, Bool.or_eq_true_iff, RegularExpression.matchEpsilon, List.cons, List.nil
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
nil :
  (P.matchEpsilon && Q.matchEpsilon) = true →
    ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
nil₁ :
  (∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    (P.matchEpsilon && Q.matchEpsilon) = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true ↔
    ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
constructor
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
⊢ ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
⟨[], [], rfl, ?_⟩

Premises used: And.intro, Exists.intro, rfl, List.nil
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
nil : P.rmatch [] = true ∧ Q.rmatch [] = true
⊢ ∃ (t : List α) (u : List α), [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
refine ⟨[], [], rfl, ?_⟩
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h : (P.matchEpsilon && Q.matchEpsilon) = true
nil nil₁ nil₂ nil₃ :
  ∀ (h : P.matchEpsilon = true ∧ Q.matchEpsilon = true), P.matchEpsilon = true ∧ Q.matchEpsilon = true
⊢ P.matchEpsilon = true ∧ Q.matchEpsilon = true

Tactic:
rwa [Bool.and_eq_true_iff] at h

Premises used: Bool.and_eq_true_iff
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : P.rmatch t = true ∧ Q.rmatch u = true
⊢ [] = HAppend.hAppend (α := List α) [] []

Tactic:
obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm

Premises used: List.append_eq_nil_iff, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : P.rmatch t = true ∧ Q.rmatch u = true
h₃ : [] = HAppend.hAppend (α := List α) [] []
⊢ P.rmatch [] = true ∧ Q.rmatch [] = true

Tactic:
obtain ⟨rfl, rfl⟩ := List.append_eq_nil_iff.1 h₁.symm

Premises used: List.append_eq_nil_iff, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.rmatch [] = true ∧ Q.rmatch [] = true
⊢ P.matchEpsilon = true ∧ Q.rmatch [] = true

Tactic:
rw [rmatch] at h₂

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.matchEpsilon = true ∧ Q.rmatch [] = true
⊢ P.matchEpsilon = true ∧ Q.matchEpsilon = true

Tactic:
rw [rmatch] at h₂

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.rmatch [] = true ∧ Q.rmatch [] = true
⊢ P.matchEpsilon = true ∧ Q.matchEpsilon = true

Tactic:
repeat rw [rmatch] at h₂

Premises used: RegularExpression.rmatch
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
inst : DecidableEq α
P Q : RegularExpression α
h₁ : [] = HAppend.hAppend (α := List α) [] []
h₂ : P.matchEpsilon = true ∧ Q.matchEpsilon = true
⊢ (P.matchEpsilon && Q.matchEpsilon) = true

Tactic:
simp [h₂]
-- 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 α
cons :
  ((P * Q).deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P * Q).rmatch (a :: x) = true ↔ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [rmatch]

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 α
pos :
  ∀ (hepsilon : P.matchEpsilon = true),
    (P.deriv a * Q + Q.deriv a).rmatch x = true ↔
      ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
neg :
  ∀ (hepsilon : ¬P.matchEpsilon = true),
    (P.deriv a * Q).rmatch x = true ↔
      ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (if P.matchEpsilon = true then P.deriv a * Q + Q.deriv a else P.deriv a * Q).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
split_ifs with hepsilon
-- 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
pos :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
      (Q.deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
⊢ (P.deriv a * Q + Q.deriv a).rmatch x = true ↔
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [add_rmatch_iff, ih]

Premises used: RegularExpression.add_rmatch_iff
-- 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
pos :
  (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
      (Q.deriv a).rmatch x = true →
    ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
pos₁ :
  (∃ (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) ∨
      (Q.deriv a).rmatch x = true
⊢ (∃ (t : List α) (u : List α), x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨
      (Q.deriv a).rmatch x = 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 ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
tauto tauto₁ :
  x = t ++ u →
    (P.deriv a).rmatch t = true →
      Q.rmatch u = true → a :: x = a :: t ++ u ∧ P.rmatch (a :: t) = true ∧ Q.rmatch u = true
left : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → a :: x = a :: t ++ u
right : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → P.rmatch (a :: t) = true
right₁ : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → Q.rmatch u = true
left₁ left₂ left₃ left₄ left₅ : x = t ++ u → (P.deriv a).rmatch t = true → Q.rmatch u = true → 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 ∧ (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:
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
h : (Q.deriv a).rmatch x = true
⊢ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
⟨[], a :: x, rfl, hepsilon, h⟩

Premises used: List.cons, And.intro, Exists.intro, rfl, List.nil
-- 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
h : (Q.deriv a).rmatch x = true
⊢ ∃ (t : List α) (u : List α), a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
exact ⟨[], a :: x, rfl, hepsilon, h⟩
-- 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
pos :
  ∀ (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) ∨
      (Q.deriv a).rmatch x = true
pos₁ :
  ∀ (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) ∨
      (Q.deriv a).rmatch x = 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:
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
pos : (Q.deriv a).rmatch x = 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:
right
-- 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
⊢ a :: x = u

Tactic:
rw [List.nil_append] at h

Premises used: List.nil_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
h : a :: x = [] ++ u
hP : P.rmatch [] = true
h₁ : a :: x = u
⊢ P.rmatch [] = true

Tactic:
rw [List.nil_append] at h

Premises used: List.nil_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
h : a :: x = u
hP : P.rmatch [] = true
⊢ Q.rmatch (a :: x) = true

Tactic:
rw [← h] at 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
h : a :: x = u
hP : P.rmatch [] = true
hQ₁ : Q.rmatch (a :: x) = true
⊢ a :: x = u

Tactic:
rw [← h] at 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
h : a :: x = u
hP : P.rmatch [] = true
hQ₁ : Q.rmatch (a :: x) = true
h₁ : a :: x = u
⊢ P.rmatch [] = true

Tactic:
rw [← h] at 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 (a :: x) = true
h : a :: x = u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true

Tactic:
hQ

Premises used: RegularExpression.rmatch