Theorem: LO.FirstOrder.Semiformula.Operator.operator_and (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
k : ℕ
ξ : Type u_1
n : ℕ
o₁ o₂ : Operator L k
v : Fin k → Semiterm L ξ n
⊢ (o₁.and o₂).operator v = o₁.operator v ⋏ o₂.operator v
Tactic:
simp [operator, and]
State after:
no goals