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