Theorem: Primrec.list_all (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 γ
α : Type u_5
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
⊢ ∀ (n : α), List.foldr (fun b s => p n b && s) true (l n) = (l n).all (p n)
Tactic:
intro a
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 γ
α : Type u_5
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
⊢ List.foldr (fun b s => p a b && s) true (l a) = (l a).all (p a)

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 γ
α : Type u_5
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
⊢ List.foldr (fun b s => p a b && s) true (l a) = (l a).all (p a)
Tactic:
generalize l a = bs
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 γ
α : Type u_5
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
bs : List β
⊢ List.foldr (fun b s => p a b && s) true bs = bs.all (p a)

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 γ
α : Type u_5
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
bs : List β
⊢ List.foldr (fun b s => p a b && s) true bs = bs.all (p a)
Tactic:
induction bs <;> simp[*]
State after:
no goals