Theorem: BoolExpr.eval_attach (LeanSAT/Reflect/BoolExpr/Decidable.lean)

State before:
x : BoolExpr Nat
f : Fin x.vars → Bool
⊢ eval f x.attach = eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x
Tactic:
generalize h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
State after:
x : BoolExpr Nat
f : Fin x.vars → Bool
f' : Nat → Bool
h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
⊢ eval f x.attach = eval f' x

State before:
x : BoolExpr Nat
f : Fin x.vars → Bool
f' : Nat → Bool
h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
⊢ eval f x.attach = eval f' x
Tactic:
obtain rfl := show f = fun i : Fin _ => f' i by subst h; simp
State after:
x : BoolExpr Nat
f' : Nat → Bool
h : (fun i => if h : i < x.vars then (fun i => f' ↑i) ⟨i, h⟩ else false) = f'
⊢ eval (fun i => f' ↑i) x.attach = eval f' x

State before:
x : BoolExpr Nat
f' : Nat → Bool
h : (fun i => if h : i < x.vars then (fun i => f' ↑i) ⟨i, h⟩ else false) = f'
⊢ eval (fun i => f' ↑i) x.attach = eval f' x
Tactic:
rw [← eval_forget, forget_attach]
State after:
no goals

State before:
x : BoolExpr Nat
f : Fin x.vars → Bool
f' : Nat → Bool
h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
⊢ f = fun i => f' ↑i
Tactic:
subst h
State after:
x : BoolExpr Nat
f : Fin x.vars → Bool
⊢ f = fun i => (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) ↑i

State before:
x : BoolExpr Nat
f : Fin x.vars → Bool
⊢ f = fun i => (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) ↑i
Tactic:
simp
State after:
no goals