Theorem: Primrec.list_subset (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✝ : DecidableEq α
⊢ PrimrecRel fun x x_1 => x ⊆ x_1
Tactic:
have : Primrec₂ (fun l₁ l₂ => l₁.foldr (fun a' ih => a' ∈ l₂ && ih) true : List α → List α → Bool) :=
  to₂' <| list_foldr fst (const true)
    <| (dom_bool₂ _).comp₂
      (list_mem.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.left))
      (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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true 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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
⊢ PrimrecRel fun x x_1 => x ⊆ x_1
Tactic:
exact this.of_eq <| by intro l₁ l₂; induction l₁ <;> simp[*]
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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
⊢ ∀ (a b : List α), List.foldr (fun a' ih => decide (a' ∈ b) && ih) true a = decide ((fun x x_1 => x ⊆ x_1) a b)
Tactic:
intro l₁ l₂
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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
l₁ l₂ : List α
⊢ List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁ = decide ((fun x x_1 => x ⊆ x_1) l₁ l₂)

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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
l₁ l₂ : List α
⊢ List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁ = decide ((fun x x_1 => x ⊆ x_1) l₁ l₂)
Tactic:
induction l₁ <;> simp[*]
State after:
no goals