Theorem: PropagateStruc.eval_compose (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
inst✝ : Fintype arity
new_arity : Type
q_arity : arity → Type
vars : (a : arity) → q_arity a → new_arity
q : (a : arity) → PropagateStruc (q_arity a)
x : new_arity → ℕ → Bool
⊢ eval (compose p new_arity q_arity vars q) x = eval p fun a => eval (q a) fun i => x (vars a i)
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
inst✝ : Fintype arity
new_arity : Type
q_arity : arity → Type
vars : (a : arity) → q_arity a → new_arity
q : (a : arity) → PropagateStruc (q_arity a)
x : new_arity → ℕ → Bool
n : ℕ
⊢ eval (compose p new_arity q_arity vars q) x n = eval p (fun a => eval (q a) fun i => x (vars a i)) n

State before:
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
inst✝ : Fintype arity
new_arity : Type
q_arity : arity → Type
vars : (a : arity) → q_arity a → new_arity
q : (a : arity) → PropagateStruc (q_arity a)
x : new_arity → ℕ → Bool
n : ℕ
⊢ eval (compose p new_arity q_arity vars q) x n = eval p (fun a => eval (q a) fun i => x (vars a i)) n
Tactic:
simp only [eval, compose, propagate_propagate]
State after:
no goals