no goals
ι : Type ?u.76166
α : Type u_1
β : Type ?u.76172
π : ι → Type ?u.76177
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ↔ a ∆ b = a ∆ ⊥
rw [symmDiff_bot]
no goals
ι : Type ?u.76166
α : Type u_1
β : Type ?u.76172
π : ι → Type ?u.76177
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ∆ ⊥ ↔ b = ⊥
rw [symmDiff_right_inj]