[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = false
[PROOFSTEP]
induction x
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
⊢ rmatch 0 [] = false
[PROOFSTEP]
simp [rmatch, matchEpsilon, *]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b head✝ : α
tail✝ : List α
tail_ih✝ : rmatch 0 tail✝ = false
⊢ rmatch 0 (head✝ :: tail✝) = false
[PROOFSTEP]
simp [rmatch, matchEpsilon, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x = []
[PROOFSTEP]
induction x
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
⊢ rmatch 1 [] = true ↔ [] = []
[PROOFSTEP]
simp [rmatch, matchEpsilon, *]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b head✝ : α
tail✝ : List α
tail_ih✝ : rmatch 1 tail✝ = true ↔ tail✝ = []
⊢ rmatch 1 (head✝ :: tail✝) = true ↔ head✝ :: tail✝ = []
[PROOFSTEP]
simp [rmatch, matchEpsilon, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a : α
x : List α
⊢ rmatch (char a) x = true ↔ x = [a]
[PROOFSTEP]
cases' x with _ x
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a : α
⊢ rmatch (char a) [] = true ↔ [] = [a]
[PROOFSTEP]
exact of_decide_eq_true rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ : α
x : List α
⊢ rmatch (char a) (head✝ :: x) = true ↔ head✝ :: x = [a]
[PROOFSTEP]
cases' x with head tail
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ : α
⊢ rmatch (char a) [head✝] = true ↔ [head✝] = [a]
[PROOFSTEP]
rw [rmatch, deriv]
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ : α
⊢ rmatch (if a = head✝ then 1 else 0) [] = true ↔ [head✝] = [a]
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : a = head✝
⊢ rmatch 1 [] = true ↔ [head✝] = [a]
[PROOFSTEP]
tauto
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : ¬a = head✝
⊢ rmatch 0 [] = true ↔ [head✝] = [a]
[PROOFSTEP]
simp [List.singleton_inj]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : ¬a = head✝
⊢ ¬head✝ = a
[PROOFSTEP]
tauto
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
⊢ rmatch (char a) (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]
[PROOFSTEP]
rw [rmatch, rmatch, deriv]
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
⊢ rmatch (deriv (if a = head✝ then 1 else 0) head) tail = true ↔ head✝ :: head :: tail = [a]
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
h : a = head✝
⊢ rmatch (deriv 1 head) tail = true ↔ head✝ :: head :: tail = [a]
[PROOFSTEP]
simp only [deriv_one, zero_rmatch, cons.injEq, and_false]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
h : ¬a = head✝
⊢ rmatch (deriv 0 head) tail = true ↔ head✝ :: head :: tail = [a]
[PROOFSTEP]
simp only [deriv_zero, zero_rmatch, cons.injEq, and_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
x : List α
⊢ rmatch (P + Q) x = true ↔ rmatch P x = true ∨ rmatch Q x = true
[PROOFSTEP]
induction' x with _ _ ih generalizing P Q
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ rmatch (P + Q) [] = true ↔ rmatch P [] = true ∨ rmatch Q [] = true
[PROOFSTEP]
simp only [rmatch, matchEpsilon, Bool.or_coe_iff]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (P + Q) (head✝ :: tail✝) = true ↔ rmatch P (head✝ :: tail✝) = true ∨ rmatch Q (head✝ :: tail✝) = true
[PROOFSTEP]
repeat' rw [rmatch]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (P + Q) (head✝ :: tail✝) = true ↔ rmatch P (head✝ :: tail✝) = true ∨ rmatch Q (head✝ :: tail✝) = true
[PROOFSTEP]
rw [rmatch]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (deriv (P + Q) head✝) tail✝ = true ↔ rmatch P (head✝ :: tail✝) = true ∨ rmatch Q (head✝ :: tail✝) = true
[PROOFSTEP]
rw [rmatch]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (deriv (P + Q) head✝) tail✝ = true ↔ rmatch (deriv P head✝) tail✝ = true ∨ rmatch Q (head✝ :: tail✝) = true
[PROOFSTEP]
rw [rmatch]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (deriv (P + Q) head✝) tail✝ = true ↔ rmatch (deriv P head✝) tail✝ = true ∨ rmatch (deriv Q head✝) tail✝ = true
[PROOFSTEP]
rw [rmatch]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (deriv (P + Q) head✝) tail✝ = true ↔ rmatch (deriv P head✝) tail✝ = true ∨ rmatch (deriv Q head✝) tail✝ = true
[PROOFSTEP]
rw [deriv_add]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ : RegularExpression α
head✝ : α
tail✝ : List α
ih : ∀ (P Q : RegularExpression α), rmatch (P + Q) tail✝ = true ↔ rmatch P tail✝ = true ∨ rmatch Q tail✝ = true
P Q : RegularExpression α
⊢ rmatch (deriv P head✝ + deriv Q head✝) tail✝ = true ↔
    rmatch (deriv P head✝) tail✝ = true ∨ rmatch (deriv Q head✝) tail✝ = true
[PROOFSTEP]
exact ih _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
induction' x with a x ih generalizing P Q
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [rmatch]
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [matchEpsilon]
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
constructor
[GOAL]
case nil.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
intro h
[GOAL]
case nil.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
refine' ⟨[], [], rfl, _⟩
[GOAL]
case nil.mp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ rmatch P [] = true ∧ rmatch Q [] = true
[PROOFSTEP]
rw [rmatch, rmatch]
[GOAL]
case nil.mp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h : (matchEpsilon P && matchEpsilon Q) = true
⊢ matchEpsilon P = true ∧ matchEpsilon Q = true
[PROOFSTEP]
rwa [Bool.and_coe_iff] at h 
[GOAL]
case nil.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro ⟨t, u, h₁, h₂⟩
[GOAL]
case nil.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
cases' List.append_eq_nil.1 h₁.symm with ht hu
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
subst ht
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
subst hu
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : rmatch P [] = true ∧ rmatch Q [] = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
[PROOFSTEP]
repeat' rw [rmatch] at h₂ 
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : rmatch P [] = true ∧ rmatch Q [] = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
[PROOFSTEP]
rw [rmatch] at h₂ 
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ rmatch Q [] = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
[PROOFSTEP]
rw [rmatch] at h₂ 
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ matchEpsilon Q = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
[PROOFSTEP]
rw [rmatch] at h₂ 
[GOAL]
case nil.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
h₁ : [] = [] ++ []
h₂ : matchEpsilon P = true ∧ matchEpsilon Q = true
⊢ (matchEpsilon P && matchEpsilon Q) = true
[PROOFSTEP]
simp [h₂]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [rmatch]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp [deriv]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
split_ifs with hepsilon
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [add_rmatch_iff, ih]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro (⟨t, u, _⟩ | h)
[GOAL]
case pos.mp.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨a :: t, u, by tauto⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
tauto
[GOAL]
case pos.mp.inr
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨[], a :: x, rfl, hepsilon, h⟩
[GOAL]
case pos.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro ⟨t, u, h, hP, hQ⟩
[GOAL]
case pos.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
cases' t with b t
[GOAL]
case pos.mpr.intro.intro.intro.intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
right
[GOAL]
case pos.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [List.nil_append] at h 
[GOAL]
case pos.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [← h] at hQ 
[GOAL]
case pos.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact hQ
[GOAL]
case pos.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
left
[GOAL]
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [List.cons_append, List.cons_eq_cons] at h 
[GOAL]
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
refine' ⟨t, u, h.2, _, hQ⟩
[GOAL]
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [rmatch] at hP 
[GOAL]
case pos.mpr.intro.intro.intro.intro.cons.h
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
convert hP
[GOAL]
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact h.1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [ih]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro ⟨t, u, h, hP, hQ⟩
[GOAL]
case neg.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rintro ⟨t, u, h, hP, hQ⟩
[GOAL]
case neg.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact ⟨a :: t, u, by tauto⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
tauto
[GOAL]
case neg.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
cases' t with b t
[GOAL]
case neg.mpr.intro.intro.intro.intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
contradiction
[GOAL]
case neg.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [List.cons_append, List.cons_eq_cons] at h 
[GOAL]
case neg.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
refine' ⟨t, u, h.2, _, hQ⟩
[GOAL]
case neg.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
rw [rmatch] at hP 
[GOAL]
case neg.mpr.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
convert hP
[GOAL]
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
exact h.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
have A : ∀ m n : ℕ, n < m + n + 1 := by
  intro m n
  convert add_lt_add_of_le_of_lt (add_le_add (zero_le m) (le_refl n)) zero_lt_one
  simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
⊢ ∀ (m n : ℕ), n < m + n + 1
[PROOFSTEP]
intro m n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
m n : ℕ
⊢ n < m + n + 1
[PROOFSTEP]
convert add_lt_add_of_le_of_lt (add_le_add (zero_le m) (le_refl n)) zero_lt_one
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
m n : ℕ
⊢ n = 0 + n + 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
clear star_rmatch_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true ↔ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) x = true → ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
cases' x with a x
[GOAL]
case mp.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) [] = true → ∃ S, [] = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
intro _h
[GOAL]
case mp.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ ∃ S, [] = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
use[]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ [] = join [] ∧ ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
dsimp
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
_h : rmatch (star P) [] = true
⊢ [] = [] ∧ ∀ (t : List α), t ∈ [] → ¬t = [] ∧ rmatch P t = true
[PROOFSTEP]
tauto
[GOAL]
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ rmatch (star P) (a :: x) = true → ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
rw [rmatch, deriv, mul_rmatch_iff]
[GOAL]
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ (∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true) →
    ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
rintro ⟨t, u, hs, ht, hu⟩
[GOAL]
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
have hwf : u.length < (List.cons a x).length :=
  by
  rw [hs, List.length_cons, List.length_append]
  apply A
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ length u < length (a :: x)
[PROOFSTEP]
rw [hs, List.length_cons, List.length_append]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
⊢ length u < Nat.succ (length t + length u)
[PROOFSTEP]
apply A
[GOAL]
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : rmatch (star P) u = true
hwf : length u < length (a :: x)
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
rw [IH _ hwf] at hu 
[GOAL]
case mp.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hu : ∃ S, u = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
hwf : length u < length (a :: x)
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
rcases hu with ⟨S', hsum, helem⟩
[GOAL]
case mp.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ ∃ S, a :: x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
use(a :: t) :: S'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: x = join ((a :: t) :: S') ∧ ∀ (t_1 : List α), t_1 ∈ (a :: t) :: S' → t_1 ≠ [] ∧ rmatch P t_1 = true
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: x = join ((a :: t) :: S')
[PROOFSTEP]
simp [hs, hsum]
[GOAL]
case h.right
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ ∀ (t_1 : List α), t_1 ∈ (a :: t) :: S' → t_1 ≠ [] ∧ rmatch P t_1 = true
[PROOFSTEP]
intro t' ht'
[GOAL]
case h.right
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
ht' : t' ∈ (a :: t) :: S'
⊢ t' ≠ [] ∧ rmatch P t' = true
[PROOFSTEP]
cases ht'
[GOAL]
case h.right.head
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: t ≠ [] ∧ rmatch P (a :: t) = true
case h.right.tail
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝¹ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
a✝ : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
[PROOFSTEP]
case head ht' =>
  simp only [ne_eq, not_false_iff, true_and, rmatch]
  exact ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
ht' b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: t ≠ [] ∧ rmatch P (a :: t) = true
[PROOFSTEP]
case head ht' =>
  simp only [ne_eq, not_false_iff, true_and, rmatch]
  exact ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
ht' b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ a :: t ≠ [] ∧ rmatch P (a :: t) = true
[PROOFSTEP]
simp only [ne_eq, not_false_iff, true_and, rmatch]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
ht' b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (deriv P a) t = true
[PROOFSTEP]
exact ht
[GOAL]
case h.right.tail
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝¹ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
a✝ : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
[PROOFSTEP]
case tail ht' => exact helem t' ht'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
ht' : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
[PROOFSTEP]
case tail ht' => exact helem t' ht'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t u : List α
hs : x = t ++ u
ht : rmatch (deriv P a) t = true
hwf : length u < length (a :: x)
S' : List (List α)
hsum : u = join S'
helem : ∀ (t : List α), t ∈ S' → t ≠ [] ∧ rmatch P t = true
t' : List α
ht' : Mem t' S'
⊢ t' ≠ [] ∧ rmatch P t' = true
[PROOFSTEP]
exact helem t' ht'
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true) → rmatch (star P) x = true
[PROOFSTEP]
rintro ⟨S, hsum, helem⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
A : ∀ (m n : ℕ), n < m + n + 1
IH :
  ∀ (t : List α),
    length t < length x →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
S : List (List α)
hsum : x = join S
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
⊢ rmatch (star P) x = true
[PROOFSTEP]
cases' x with a x
[GOAL]
case mpr.intro.intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
IH :
  ∀ (t : List α),
    length t < length [] →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : [] = join S
⊢ rmatch (star P) [] = true
[PROOFSTEP]
rfl
[GOAL]
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : a :: x = join S
⊢ rmatch (star P) (a :: x) = true
[PROOFSTEP]
rw [rmatch, deriv, mul_rmatch_iff]
[GOAL]
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
S : List (List α)
helem : ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
hsum : a :: x = join S
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
cases' S with t' U
[GOAL]
case mpr.intro.intro.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
helem : ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join []
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
exact ⟨[], [], by tauto⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
helem : ∀ (t : List α), t ∈ [] → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join []
⊢ x = [] ++ [] ∧ rmatch (deriv P a) [] = true ∧ rmatch (star P) [] = true
[PROOFSTEP]
tauto
[GOAL]
case mpr.intro.intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
t' : List α
U : List (List α)
helem : ∀ (t : List α), t ∈ t' :: U → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join (t' :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
cases' t' with b t
[GOAL]
case mpr.intro.intro.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
helem : ∀ (t : List α), t ∈ [] :: U → t ≠ [] ∧ rmatch P t = true
hsum : a :: x = join ([] :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
simp only [forall_eq_or_imp, List.mem_cons] at helem 
[GOAL]
case mpr.intro.intro.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
hsum : a :: x = join ([] :: U)
helem : ([] ≠ [] ∧ rmatch P [] = true) ∧ ∀ (a : List α), a ∈ U → a ≠ [] ∧ rmatch P a = true
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
simp only [eq_self_iff_true, not_true, Ne.def, false_and_iff] at helem 
[GOAL]
case mpr.intro.intro.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a :: x = join ((b :: t) :: U)
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
simp only [List.join, List.cons_append, List.cons_eq_cons] at hsum 
[GOAL]
case mpr.intro.intro.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ ∃ t u, x = t ++ u ∧ rmatch (deriv P a) t = true ∧ rmatch (star P) u = true
[PROOFSTEP]
refine' ⟨t, U.join, hsum.2, _, _⟩
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ rmatch (deriv P a) t = true
[PROOFSTEP]
specialize helem (b :: t) (by simp)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ b :: t ∈ (b :: t) :: U
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch P (b :: t) = true
⊢ rmatch (deriv P a) t = true
[PROOFSTEP]
rw [rmatch] at helem 
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch (deriv P b) t = true
⊢ rmatch (deriv P a) t = true
[PROOFSTEP]
convert helem.2
[GOAL]
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
hsum : a = b ∧ x = t ++ join U
helem : b :: t ≠ [] ∧ rmatch (deriv P b) t = true
⊢ a = b
[PROOFSTEP]
exact hsum.1
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ rmatch (star P) (join U) = true
[PROOFSTEP]
have hwf : U.join.length < (List.cons a x).length :=
  by
  rw [hsum.1, hsum.2]
  simp only [List.length_append, List.length_join, List.length]
  apply A
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ length (join U) < length (a :: x)
[PROOFSTEP]
rw [hsum.1, hsum.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ length (join U) < length (b :: (t ++ join U))
[PROOFSTEP]
simp only [List.length_append, List.length_join, List.length]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
⊢ sum (map length U) < length t + sum (map length U) + 1
[PROOFSTEP]
apply A
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
hwf : length (join U) < length (a :: x)
⊢ rmatch (star P) (join U) = true
[PROOFSTEP]
rw [IH _ hwf]
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t : List α
helem : ∀ (t_1 : List α), t_1 ∈ (b :: t) :: U → t_1 ≠ [] ∧ rmatch P t_1 = true
hsum : a = b ∧ x = t ++ join U
hwf : length (join U) < length (a :: x)
⊢ ∃ S, join U = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true
[PROOFSTEP]
refine' ⟨U, rfl, fun t h => helem t _⟩
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ (t : List α), t ∈ (b :: t✝) :: U → t ≠ [] ∧ rmatch P t = true
hsum : a = b ∧ x = t✝ ++ join U
hwf : length (join U) < length (a :: x)
t : List α
h : t ∈ U
⊢ t ∈ (b :: t✝) :: U
[PROOFSTEP]
right
[GOAL]
case mpr.intro.intro.cons.cons.cons.refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b✝ : α
P : RegularExpression α
A : ∀ (m n : ℕ), n < m + n + 1
a : α
x : List α
IH :
  ∀ (t : List α),
    length t < length (a :: x) →
      (rmatch (star P) t = true ↔ ∃ S, t = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch P t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ (t : List α), t ∈ (b :: t✝) :: U → t ≠ [] ∧ rmatch P t = true
hsum : a = b ∧ x = t✝ ++ join U
hwf : length (join U) < length (a :: x)
t : List α
h : t ∈ U
⊢ Mem t U
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
⊢ ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P : RegularExpression α
x : List α
⊢ rmatch P x = true ↔ x ∈ matches' P
[PROOFSTEP]
induction P generalizing x
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch zero x = true ↔ x ∈ matches' zero
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch epsilon x = true ↔ x ∈ matches' epsilon
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
all_goals
  try rw [zero_def]
  try rw [one_def]
  try rw [plus_def]
  try rw [comp_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch zero x = true ↔ x ∈ matches' zero
[PROOFSTEP]
try rw [zero_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch zero x = true ↔ x ∈ matches' zero
[PROOFSTEP]
rw [zero_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
try rw [one_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
rw [one_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
try rw [plus_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
rw [plus_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
try rw [comp_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
rw [comp_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch epsilon x = true ↔ x ∈ matches' epsilon
[PROOFSTEP]
try rw [zero_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch epsilon x = true ↔ x ∈ matches' epsilon
[PROOFSTEP]
rw [zero_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch epsilon x = true ↔ x ∈ matches' epsilon
[PROOFSTEP]
try rw [one_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch epsilon x = true ↔ x ∈ matches' epsilon
[PROOFSTEP]
rw [one_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
[PROOFSTEP]
try rw [plus_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
[PROOFSTEP]
rw [plus_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
[PROOFSTEP]
try rw [comp_def]
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
[PROOFSTEP]
rw [comp_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
try rw [zero_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
rw [zero_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
try rw [one_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
rw [one_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
try rw [plus_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
rw [plus_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
try rw [comp_def]
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
rw [comp_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
[PROOFSTEP]
try rw [zero_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
[PROOFSTEP]
rw [zero_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
[PROOFSTEP]
try rw [one_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
[PROOFSTEP]
rw [one_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
[PROOFSTEP]
try rw [plus_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (plus a✝¹ a✝) x = true ↔ x ∈ matches' (plus a✝¹ a✝)
[PROOFSTEP]
rw [plus_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
[PROOFSTEP]
try rw [comp_def]
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
[PROOFSTEP]
rw [comp_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
try rw [zero_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
rw [zero_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
try rw [one_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
rw [one_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
try rw [plus_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
rw [plus_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
try rw [comp_def]
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (comp a✝¹ a✝) x = true ↔ x ∈ matches' (comp a✝¹ a✝)
[PROOFSTEP]
rw [comp_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
try rw [zero_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
rw [zero_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
try rw [one_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
rw [one_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
try rw [plus_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
rw [plus_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
try rw [comp_def]
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
rw [comp_def]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ * a✝) x = true ↔ x ∈ matches' (a✝¹ * a✝)
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case zero =>
  rw [zero_rmatch]
  tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
case zero =>
  rw [zero_rmatch]
  tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 0 x = true ↔ x ∈ matches' 0
[PROOFSTEP]
rw [zero_rmatch]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ false = true ↔ x ∈ matches' 0
[PROOFSTEP]
tauto
[GOAL]
case epsilon
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ * a✝) x = true ↔ x ∈ matches' (a✝¹ * a✝)
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case epsilon =>
  rw [one_rmatch_iff]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
[PROOFSTEP]
case epsilon =>
  rw [one_rmatch_iff]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1
[PROOFSTEP]
rw [one_rmatch_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
x : List α
⊢ x = [] ↔ x ∈ matches' 1
[PROOFSTEP]
rfl
[GOAL]
case char
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ * a✝) x = true ↔ x ∈ matches' (a✝¹ * a✝)
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case char =>
  rw [char_rmatch_iff]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
case char =>
  rw [char_rmatch_iff]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ rmatch (char a✝) x = true ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
rw [char_rmatch_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b a✝ : α
x : List α
⊢ x = [a✝] ↔ x ∈ matches' (char a✝)
[PROOFSTEP]
rfl
[GOAL]
case plus
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ * a✝) x = true ↔ x ∈ matches' (a✝¹ * a✝)
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case plus _ _ ih₁ ih₂ =>
  rw [add_rmatch_iff, ih₁, ih₂]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
ih₂ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
[PROOFSTEP]
case plus _ _ ih₁ ih₂ =>
  rw [add_rmatch_iff, ih₁, ih₂]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
ih₂ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ + a✝) x = true ↔ x ∈ matches' (a✝¹ + a✝)
[PROOFSTEP]
rw [add_rmatch_iff, ih₁, ih₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
ih₁ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
ih₂ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ x ∈ matches' a✝¹ ∨ x ∈ matches' a✝ ↔ x ∈ matches' (a✝¹ + a✝)
[PROOFSTEP]
rfl
[GOAL]
case comp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝¹ a✝ : RegularExpression α
a_ih✝¹ : ∀ (x : List α), rmatch a✝¹ x = true ↔ x ∈ matches' a✝¹
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (a✝¹ * a✝) x = true ↔ x ∈ matches' (a✝¹ * a✝)
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case comp P Q ih₁
  ih₂ =>
  simp only [mul_rmatch_iff, comp_def, Language.mul_def, exists_and_left, Set.mem_image2, Set.image_prod]
  constructor
  · rintro ⟨x, y, hsum, hmatch₁, hmatch₂⟩
    rw [ih₁] at hmatch₁ 
    rw [ih₂] at hmatch₂ 
    exact ⟨x, y, hmatch₁, hmatch₂, hsum.symm⟩
  · rintro ⟨x, y, hmatch₁, hmatch₂, hsum⟩
    rw [← ih₁] at hmatch₁ 
    rw [← ih₂] at hmatch₂ 
    exact ⟨x, y, hsum.symm, hmatch₁, hmatch₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x : List α
⊢ rmatch (P * Q) x = true ↔ x ∈ matches' (P * Q)
[PROOFSTEP]
case comp P Q ih₁
  ih₂ =>
  simp only [mul_rmatch_iff, comp_def, Language.mul_def, exists_and_left, Set.mem_image2, Set.image_prod]
  constructor
  · rintro ⟨x, y, hsum, hmatch₁, hmatch₂⟩
    rw [ih₁] at hmatch₁ 
    rw [ih₂] at hmatch₂ 
    exact ⟨x, y, hmatch₁, hmatch₂, hsum.symm⟩
  · rintro ⟨x, y, hmatch₁, hmatch₂, hsum⟩
    rw [← ih₁] at hmatch₁ 
    rw [← ih₂] at hmatch₂ 
    exact ⟨x, y, hsum.symm, hmatch₁, hmatch₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x : List α
⊢ rmatch (P * Q) x = true ↔ x ∈ matches' (P * Q)
[PROOFSTEP]
simp only [mul_rmatch_iff, comp_def, Language.mul_def, exists_and_left, Set.mem_image2, Set.image_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x : List α
⊢ (∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true) ↔ x ∈ matches' (P * Q)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x : List α
⊢ (∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true) → x ∈ matches' (P * Q)
[PROOFSTEP]
rintro ⟨x, y, hsum, hmatch₁, hmatch₂⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x✝ x y : List α
hsum : x✝ = x ++ y
hmatch₁ : rmatch P x = true
hmatch₂ : rmatch Q y = true
⊢ x✝ ∈ matches' (P * Q)
[PROOFSTEP]
rw [ih₁] at hmatch₁ 
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x✝ x y : List α
hsum : x✝ = x ++ y
hmatch₁ : x ∈ matches' P
hmatch₂ : rmatch Q y = true
⊢ x✝ ∈ matches' (P * Q)
[PROOFSTEP]
rw [ih₂] at hmatch₂ 
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x✝ x y : List α
hsum : x✝ = x ++ y
hmatch₁ : x ∈ matches' P
hmatch₂ : y ∈ matches' Q
⊢ x✝ ∈ matches' (P * Q)
[PROOFSTEP]
exact ⟨x, y, hmatch₁, hmatch₂, hsum.symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x : List α
⊢ x ∈ matches' (P * Q) → ∃ t u, x = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
[PROOFSTEP]
rintro ⟨x, y, hmatch₁, hmatch₂, hsum⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x✝ x y : List α
hmatch₁ : x ∈ matches' P
hmatch₂ : y ∈ matches' Q
hsum : (fun x x_1 => x ++ x_1) x y = x✝
⊢ ∃ t u, x✝ = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
[PROOFSTEP]
rw [← ih₁] at hmatch₁ 
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x✝ x y : List α
hmatch₁ : rmatch P x = true
hmatch₂ : y ∈ matches' Q
hsum : (fun x x_1 => x ++ x_1) x y = x✝
⊢ ∃ t u, x✝ = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
[PROOFSTEP]
rw [← ih₂] at hmatch₂ 
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), rmatch P x = true ↔ x ∈ matches' P
ih₂ : ∀ (x : List α), rmatch Q x = true ↔ x ∈ matches' Q
x✝ x y : List α
hmatch₁ : rmatch P x = true
hmatch₂ : rmatch Q y = true
hsum : (fun x x_1 => x ++ x_1) x y = x✝
⊢ ∃ t u, x✝ = t ++ u ∧ rmatch P t = true ∧ rmatch Q u = true
[PROOFSTEP]
exact ⟨x, y, hsum.symm, hmatch₁, hmatch₂⟩
[GOAL]
case star
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
a_ih✝ : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case star _ ih =>
  rw [star_rmatch_iff]
  simp only [ne_eq, matches', Language.kstar_def_nonempty, mem_setOf_eq]
  constructor
  all_goals
    rintro ⟨S, hx, hS⟩
    refine' ⟨S, hx, _⟩
    intro y
    specialize hS y
  · rw [← ih y]
    tauto
  · rw [ih y]
    tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
case star _ ih =>
  rw [star_rmatch_iff]
  simp only [ne_eq, matches', Language.kstar_def_nonempty, mem_setOf_eq]
  constructor
  all_goals
    rintro ⟨S, hx, hS⟩
    refine' ⟨S, hx, _⟩
    intro y
    specialize hS y
  · rw [← ih y]
    tauto
  · rw [ih y]
    tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ rmatch (star a✝) x = true ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
rw [star_rmatch_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → t ≠ [] ∧ rmatch a✝ t = true) ↔ x ∈ matches' (star a✝)
[PROOFSTEP]
simp only [ne_eq, matches', Language.kstar_def_nonempty, mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true) ↔
    x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []}
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true) →
    x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []}
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []} →
    ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
[PROOFSTEP]
all_goals
  rintro ⟨S, hx, hS⟩
  refine' ⟨S, hx, _⟩
  intro y
  specialize hS y
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ (∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true) →
    x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []}
[PROOFSTEP]
rintro ⟨S, hx, hS⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
hS : ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
⊢ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []}
[PROOFSTEP]
refine' ⟨S, hx, _⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
hS : ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
⊢ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
[PROOFSTEP]
intro y
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
hS : ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
y : List α
⊢ y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
[PROOFSTEP]
specialize hS y
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
⊢ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []} →
    ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
[PROOFSTEP]
rintro ⟨S, hx, hS⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
hS : ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
⊢ ∃ S, x = join S ∧ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
[PROOFSTEP]
refine' ⟨S, hx, _⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
hS : ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
⊢ ∀ (t : List α), t ∈ S → ¬t = [] ∧ rmatch a✝ t = true
[PROOFSTEP]
intro y
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
hS : ∀ (y : List α), y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
y : List α
⊢ y ∈ S → ¬y = [] ∧ rmatch a✝ y = true
[PROOFSTEP]
specialize hS y
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
y : List α
hS : y ∈ S → ¬y = [] ∧ rmatch a✝ y = true
⊢ y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
[PROOFSTEP]
rw [← ih y]
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
y : List α
hS : y ∈ S → ¬y = [] ∧ rmatch a✝ y = true
⊢ y ∈ S → rmatch a✝ y = true ∧ ¬y = []
[PROOFSTEP]
tauto
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
y : List α
hS : y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
⊢ y ∈ S → ¬y = [] ∧ rmatch a✝ y = true
[PROOFSTEP]
rw [ih y]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
a✝ : RegularExpression α
ih : ∀ (x : List α), rmatch a✝ x = true ↔ x ∈ matches' a✝
x : List α
S : List (List α)
hx : x = join S
y : List α
hS : y ∈ S → y ∈ matches' a✝ ∧ ¬y = []
⊢ y ∈ S → ¬y = [] ∧ y ∈ matches' a✝
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
P : RegularExpression α
⊢ map f (P ^ 0) = map f P ^ 0
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
P : RegularExpression α
⊢ 1 = map f P ^ 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
R S : RegularExpression α
⊢ map id (R + S) = R + S
[PROOFSTEP]
simp_rw [map, map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
R S : RegularExpression α
⊢ map id (R * S) = R * S
[PROOFSTEP]
simp_rw [map, map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
R : RegularExpression α
⊢ map id (star R) = star R
[PROOFSTEP]
simp_rw [map, map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R + S)) = map (g ∘ f) (R + S)
[PROOFSTEP]
simp only [map, Function.comp_apply, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R * S)) = map (g ∘ f) (R * S)
[PROOFSTEP]
simp only [map, Function.comp_apply, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
g : β → γ
f : α → β
R : RegularExpression α
⊢ map g (map f (star R)) = map (g ∘ f) (star R)
[PROOFSTEP]
simp only [map, Function.comp_apply, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
f : α → β
a : α
⊢ matches' (map f (char a)) = ↑(Language.map f) (matches' (char a))
[PROOFSTEP]
rw [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a✝ b : α
f : α → β
a : α
⊢ ↑(Language.map f) (matches' (char a)) = matches' (map f (char a))
[PROOFSTEP]
exact image_singleton
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ matches' (map f (R + S)) = ↑(Language.map f) (matches' (R + S))
[PROOFSTEP]
simp only [matches'_map, map, matches'_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ ↑(Language.map f) (matches' R) + ↑(Language.map f) (matches' S) = ↑(Language.map f) (matches' R + matches' S)
[PROOFSTEP]
rw [map_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ matches' (map f (R * S)) = ↑(Language.map f) (matches' (R * S))
[PROOFSTEP]
simp only [matches'_map, map, matches'_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ ↑(Language.map f) (matches' R) * ↑(Language.map f) (matches' S) = ↑(Language.map f) (matches' R * matches' S)
[PROOFSTEP]
rw [map_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ matches' (map f (star R)) = ↑(Language.map f) (matches' (star R))
[PROOFSTEP]
simp_rw [map, matches', matches'_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (↑(Language.map f) (matches' R))∗ = ↑(Language.map f) (matches' R)∗
[PROOFSTEP]
rw [Language.kstar_eq_iSup_pow, Language.kstar_eq_iSup_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ ⨆ (i : ℕ), ↑(Language.map f) (matches' R) ^ i = ↑(Language.map f) (⨆ (i : ℕ), matches' R ^ i)
[PROOFSTEP]
simp_rw [← map_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ ⨆ (i : ℕ), ↑(Language.map f) (matches' R ^ i) = ↑(Language.map f) (⨆ (i : ℕ), matches' R ^ i)
[PROOFSTEP]
exact image_iUnion.symm
