case nil
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ rmatch (P + Q) [] = true ↔ rmatch P [] = true ∨ rmatch Q [] = true

case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
dec : DecidableEq α
a b : α
P Q : RegularExpression α
x : List α
⊢ rmatch (P + Q) x = true ↔ rmatch P x = true ∨ rmatch Q x = true
induction' x with _ _ ih generalizing P Q
no goals
case nil
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
dec : DecidableEq α
a b : α
P✝ Q✝ P Q : RegularExpression α
⊢ rmatch (P + Q) [] = true ↔ rmatch P [] = true ∨ rmatch Q [] = true
simp only [rmatch, matchEpsilon, Bool.or_coe_iff]
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
repeat' rw [rmatch]
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
rw [deriv_add]
no goals
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
exact ih _ _
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
case cons
α : Type u_1
β : Type ?u.41307
γ : Type ?u.41310
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
rw [rmatch]