a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → b) ∧ (b → a) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
rw [iff_iff_implies_and_implies a b]
no goals
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → b) ∧ (b → a) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
simp only [imp_iff_not_or, Or.comm]