α : Type u
β : Type ?u.54113
w x y z : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x (xᶜ)
α : Type u
β : Type ?u.54113
w x y z : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y
rw [← h]
no goals
α : Type u
β : Type ?u.54113
w x y z : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x (xᶜ)
exact isCompl_compl