case nil
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a : α
⊢ rmatch (char a) [] = true ↔ [] = [a]

case cons
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
x : List α
⊢ rmatch (char a) (head✝ :: x) = true ↔ head✝ :: x = [a]
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a : α
x : List α
⊢ rmatch (char a) x = true ↔ x = [a]
cases' x with _ x
case cons.nil
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
⊢ rmatch (char a) [head✝] = true ↔ [head✝] = [a]

case cons.cons
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
⊢ rmatch (char a) (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]
case cons
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
x : List α
⊢ rmatch (char a) (head✝ :: x) = true ↔ head✝ :: x = [a]
cases' x with head tail
no goals
case nil
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a : α
⊢ rmatch (char a) [] = true ↔ [] = [a]
exact of_decide_eq_true rfl
case cons.nil
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
⊢ rmatch (if a = head✝ then 1 else 0) [] = true ↔ [head✝] = [a]
case cons.nil
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
⊢ rmatch (char a) [head✝] = true ↔ [head✝] = [a]
rw [rmatch, deriv]
case cons.nil.inl
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : a = head✝
⊢ rmatch 1 [] = true ↔ [head✝] = [a]

case cons.nil.inr
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : ¬a = head✝
⊢ rmatch 0 [] = true ↔ [head✝] = [a]
case cons.nil
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
⊢ rmatch (if a = head✝ then 1 else 0) [] = true ↔ [head✝] = [a]
split_ifs
no goals
case cons.nil.inl
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : a = head✝
⊢ rmatch 1 [] = true ↔ [head✝] = [a]
tauto
case cons.nil.inr
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : ¬a = head✝
⊢ ¬head✝ = a
case cons.nil.inr
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : ¬a = head✝
⊢ rmatch 0 [] = true ↔ [head✝] = [a]
simp [List.singleton_inj]
no goals
case cons.nil.inr
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ : α
h✝ : ¬a = head✝
⊢ ¬head✝ = a
tauto
case cons.cons
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
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]
case cons.cons
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
⊢ rmatch (char a) (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]
rw [rmatch, rmatch, deriv]
case cons.cons.inl
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
h : a = head✝
⊢ rmatch (deriv 1 head) tail = true ↔ head✝ :: head :: tail = [a]

case cons.cons.inr
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
h : ¬a = head✝
⊢ rmatch (deriv 0 head) tail = true ↔ head✝ :: head :: tail = [a]
case cons.cons
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
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]
split_ifs with h
no goals
case cons.cons.inl
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
h : a = head✝
⊢ rmatch (deriv 1 head) tail = true ↔ head✝ :: head :: tail = [a]
simp only [deriv_one, zero_rmatch, cons.injEq, and_false]
no goals
case cons.cons.inr
α : Type u_1
β : Type ?u.34271
γ : Type ?u.34274
dec : DecidableEq α
a✝ b a head✝ head : α
tail : List α
h : ¬a = head✝
⊢ rmatch (deriv 0 head) tail = true ↔ head✝ :: head :: tail = [a]
simp only [deriv_zero, zero_rmatch, cons.injEq, and_false]