ι : Type ?u.139347
α : Type u_1
β : Type ?u.139353
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ a \ b = a \ ⊥
ι : Type ?u.139347
α : Type u_1
β : Type ?u.139353
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ a \ b = a
conv_rhs => rw [← @sdiff_bot _ _ a]
no goals
ι : Type ?u.139347
α : Type u_1
β : Type ?u.139353
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
h : Disjoint a b
⊢ a \ b = a \ ⊥
rw [← h.eq_bot, sdiff_inf_self_left]