Theorem: Primrec.list_mem (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
⊢ PrimrecRel fun x x_1 => x ∈ x_1
Tactic:
have : Primrec₂ (fun a l => l.foldr (fun a' ih => (a == a') || ih) false : α → List α → Bool) :=
  to₂' <| list_foldr snd (const false)
    <| (dom_bool₂ Bool.or).comp₂
      (Primrec.lawfulbeq.comp₂ (fst.comp₂ Primrec₂.left) (fst.comp₂ Primrec₂.right))
      (snd.comp₂ Primrec₂.right)
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ PrimrecRel fun x x_1 => x ∈ x_1

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ PrimrecRel fun x x_1 => x ∈ x_1
Tactic:
exact this.of_eq <| by intro a as; induction as <;> simp[*]; symm; simp[decide_eq_iff]
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ ∀ (a : α) (b : List α), List.foldr (fun a' ih => a == a' || ih) false b = decide ((fun x x_1 => x ∈ x_1) a b)
Tactic:
intro a as
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a : α
as : List α
⊢ List.foldr (fun a' ih => a == a' || ih) false as = decide ((fun x x_1 => x ∈ x_1) a as)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a : α
as : List α
⊢ List.foldr (fun a' ih => a == a' || ih) false as = decide ((fun x x_1 => x ∈ x_1) a as)
Tactic:
induction as <;> simp[*]
State after:
case cons
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ (a == head✝ || decide (a ∈ tail✝)) = decide (a ∈ head✝ :: tail✝)

State before:
case cons
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ (a == head✝ || decide (a ∈ tail✝)) = decide (a ∈ head✝ :: tail✝)
Tactic:
symm
State after:
case cons
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ decide (a ∈ head✝ :: tail✝) = (a == head✝ || decide (a ∈ tail✝))

State before:
case cons
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ decide (a ∈ head✝ :: tail✝) = (a == head✝ || decide (a ∈ tail✝))
Tactic:
simp[decide_eq_iff]
State after:
no goals