case nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ rmatch (P * Q) [] = true ↔ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true

case cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
⊢ rmatch (P * Q) (a :: x) = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P Q : RegularExpression α
x : List α
⊢ rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
induction' x with a x ih generalizing P Q
case nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ matchEpsilon (P * Q) = true ↔ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ rmatch (P * Q) [] = true ↔ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
rw [rmatch]
case nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ (matchEpsilon P && matchEpsilon Q) = true ↔ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ matchEpsilon (P * Q) = true ↔ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
simp only [matchEpsilon]
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ (matchEpsilon P && matchEpsilon Q) = true → ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true

case nil.mpr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ (∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true) → (matchEpsilon P && matchEpsilon Q) = true
case nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ (matchEpsilon P && matchEpsilon Q) = true ↔ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
constructor
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ (matchEpsilon P && matchEpsilon Q) = true → ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
intro h
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ rmatch P [] = true ∧ rmatch Q [] = true
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ ∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
refine' ⟨[], [], rfl, _⟩
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ matchEpsilon P = true ∧ matchEpsilon Q = true
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ rmatch P [] = true ∧ rmatch Q [] = true
rw [rmatch, rmatch]
no goals
case nil.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ matchEpsilon P = true ∧ matchEpsilon Q = true
rwa [Bool.and_coe_iff] at h
case nil.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : rmatch P t = true ∧ rmatch Q u = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
case nil.mpr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ (∃ t u, [] = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true) → (matchEpsilon P && matchEpsilon Q) = true
rintro ⟨t, u, h₁, h₂⟩
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : rmatch P t = true ∧ rmatch Q u = true
ht : t = []
hu : u = []
⊢ (matchEpsilon P && matchEpsilon Q) = true
case nil.mpr.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : rmatch P t = true ∧ rmatch Q u = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
cases' List.append_eq_nil.1 h₁.symm with ht hu
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
u : List α
hu : u = []
h₁ : [] = [] ++ u
h₂ : rmatch P [] = true ∧ rmatch Q u = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
t u : List α
h₁ : [] = t ++ u
h₂ : rmatch P t = true ∧ rmatch Q u = true
ht : t = []
hu : u = []
⊢ (matchEpsilon P && matchEpsilon Q) = true
subst ht
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : rmatch P [] = true ∧ rmatch Q [] = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
u : List α
hu : u = []
h₁ : [] = [] ++ u
h₂ : rmatch P [] = true ∧ rmatch Q u = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
subst hu
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ matchEpsilon Q = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : rmatch P [] = true ∧ rmatch Q [] = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
repeat' rw [rmatch] at h₂
no goals
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ matchEpsilon Q = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
simp [h₂]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ matchEpsilon Q = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ matchEpsilon Q = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
rw [rmatch] at h₂
case cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
⊢ rmatch (deriv (P * Q) a) x = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
⊢ rmatch (P * Q) (a :: x) = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
rw [rmatch]
case cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
⊢ rmatch (if matchEpsilon P = true then deriv P a * Q + deriv Q a else deriv P a * Q) x = true ↔
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
⊢ rmatch (deriv (P * Q) a) x = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
simp [deriv]
case cons.inl
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ rmatch (deriv P a * Q + deriv Q a) x = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true

case cons.inr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
⊢ rmatch (deriv P a * Q) x = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
⊢ rmatch (if matchEpsilon P = true then deriv P a * Q + deriv Q a else deriv P a * Q) x = true ↔
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
split_ifs with hepsilon
case cons.inl
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true ↔
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case cons.inl
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ rmatch (deriv P a * Q + deriv Q a) x = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
rw [add_rmatch_iff, ih]
case cons.inl.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true →
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true

case cons.inl.mpr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ (∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true) →
    (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
case cons.inl
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true ↔
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
constructor
case cons.inl.mp.inl.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
t u : List α
h✝ : x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
⊢ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true

case cons.inl.mp.inr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
h : rmatch (deriv Q a) x = true
⊢ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case cons.inl.mp
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true →
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
rintro (⟨t, u, _⟩ | h)
no goals
case cons.inl.mp.inl.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
t u : List α
h✝ : x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
⊢ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
exact ⟨a :: t, u, by tauto⟩
no goals
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
t u : List α
h✝ : x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
⊢ a :: x = a :: t ++ u ∧ rmatch P (a :: t) = true ∧ rmatch Q u = true
tauto
no goals
case cons.inl.mp.inr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
h : rmatch (deriv Q a) x = true
⊢ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
exact ⟨[], a :: x, rfl, hepsilon, h⟩
case cons.inl.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
t u : List α
h : a :: x = t ++ u
hP : rmatch P t = true
hQ : rmatch Q u = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
case cons.inl.mpr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
⊢ (∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true) →
    (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
rintro ⟨t, u, h, hP, hQ⟩
case cons.inl.mpr.intro.intro.intro.intro.nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = [] ++ u
hP : rmatch P [] = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true

case cons.inl.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : rmatch P (b :: t) = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
case cons.inl.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
t u : List α
h : a :: x = t ++ u
hP : rmatch P t = true
hQ : rmatch Q u = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
cases' t with b t
case cons.inl.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = [] ++ u
hP : rmatch P [] = true
⊢ rmatch (deriv Q a) x = true
case cons.inl.mpr.intro.intro.intro.intro.nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = [] ++ u
hP : rmatch P [] = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
right
case cons.inl.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = u
hP : rmatch P [] = true
⊢ rmatch (deriv Q a) x = true
case cons.inl.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = [] ++ u
hP : rmatch P [] = true
⊢ rmatch (deriv Q a) x = true
rw [List.nil_append] at h
case cons.inl.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q (a :: x) = true
h : a :: x = u
hP : rmatch P [] = true
⊢ rmatch (deriv Q a) x = true
case cons.inl.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = u
hP : rmatch P [] = true
⊢ rmatch (deriv Q a) x = true
rw [← h] at hQ
no goals
case cons.inl.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q (a :: x) = true
h : a :: x = u
hP : rmatch P [] = true
⊢ rmatch (deriv Q a) x = true
exact hQ
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
case cons.inl.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : rmatch P (b :: t) = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ∨ rmatch (deriv Q a) x = true
left
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
rw [List.cons_append, List.cons_eq_cons] at h
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
refine' ⟨t, u, h.2, _, hQ⟩
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
rw [rmatch] at hP
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ a = b
case cons.inl.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
convert hP
no goals
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ a = b
exact h.1
case cons.inr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ↔
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
case cons.inr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
⊢ rmatch (deriv P a * Q) x = true ↔ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
rw [ih]
case cons.inr.mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
t u : List α
h : x = t ++ u
hP : rmatch (deriv P a) t = true
hQ : rmatch Q u = true
⊢ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true

case cons.inr.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
t u : List α
h : a :: x = t ++ u
hP : rmatch P t = true
hQ : rmatch Q u = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
case cons.inr
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true) ↔
    ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
constructor <;> rintro ⟨t, u, h, hP, hQ⟩
no goals
case cons.inr.mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
t u : List α
h : x = t ++ u
hP : rmatch (deriv P a) t = true
hQ : rmatch Q u = true
⊢ ∃ t u, a :: x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
exact ⟨a :: t, u, by tauto⟩
no goals
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
t u : List α
h : x = t ++ u
hP : rmatch (deriv P a) t = true
hQ : rmatch Q u = true
⊢ a :: x = a :: t ++ u ∧ rmatch P (a :: t) = true ∧ rmatch Q u = true
tauto
case cons.inr.mpr.intro.intro.intro.intro.nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = [] ++ u
hP : rmatch P [] = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true

case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
case cons.inr.mpr.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
t u : List α
h : a :: x = t ++ u
hP : rmatch P t = true
hQ : rmatch Q u = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
cases' t with b t
no goals
case cons.inr.mpr.intro.intro.intro.intro.nil
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
h : a :: x = [] ++ u
hP : rmatch P [] = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
contradiction
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
rw [List.cons_append, List.cons_eq_cons] at h
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch Q u = true
refine' ⟨t, u, h.2, _, hQ⟩
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
rw [rmatch] at hP
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ a = b
case cons.inr.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
convert hP
no goals
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type ?u.43048
γ : Type ?u.43051
dec : DecidableEq α
a✝ b✝ : α
P✝ Q✝ : RegularExpression α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P * Q) x = true ↔ ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
P Q : RegularExpression α
hepsilon : ¬matchEpsilon P = true
u : List α
hQ : rmatch Q u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : rmatch (deriv P b) t = true
⊢ a = b
exact h.1