ι : Type ?u.164668
α : Type u_1
β : Type ?u.164674
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
ι : Type ?u.164668
α : Type u_1
β : Type ?u.164674
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
refine' ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm _
ι : Type ?u.164668
α : Type u_1
β : Type ?u.164674
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ Disjoint (a ⊓ b) ((a ⊓ b)ᶜ)
ι : Type ?u.164668
α : Type u_1
β : Type ?u.164674
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
  disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]
no goals
ι : Type ?u.164668
α : Type u_1
β : Type ?u.164674
inst✝ : HeytingAlgebra α
a✝ b✝ c a b : α
⊢ Disjoint (a ⊓ b) ((a ⊓ b)ᶜ)
exact disjoint_compl_right