@[simp]

theorem and_imp_iff_and {a b : Prop} : a ∧ (a → b) ↔ a ∧ b

@[simp]

theorem imp_and_iff_and {a b : Prop} : (a → b) ∧ a ↔ b ∧ a