Theorem: BoolExpr.sat_and (LeanSAT/Reflect/BoolExpr/Basic.lean)

State before:
α : Type
x y : BoolExpr α
f : α → Bool
hx : x.sat f
hy : y.sat f
⊢ (gate Gate.and x y).sat f
Tactic:
simp only [sat] at *
State after:
α : Type
x y : BoolExpr α
f : α → Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true

State before:
α : Type
x y : BoolExpr α
f : α → Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true
Tactic:
simp [hx, hy, Gate.eval]
State after:
no goals