no goals
ι : Type ?u.39493
α : Type u_1
β : Type ?u.39499
π : ι → Type ?u.39504
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]