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

State before:
x : BoolExpr Nat
h : x.attach.unsat
f : Nat → Bool
⊢ eval f x = false
Tactic:
specialize h fun i => f i
State after:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => f ↑i) x.attach = false
⊢ eval f x = false

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

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

State before:
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ eval f x = eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x
Tactic:
apply eval_congr
State after:
case w
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ ∀ (i : Nat), i < x.vars → f i = if h : i < x.vars then f ↑⟨i, h⟩ else false

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

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

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

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