ι : Type ?u.78168
α : Type u_1
β : Type ?u.78174
π : ι → Type ?u.78179
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
ι : Type ?u.78168
α : Type u_1
β : Type ?u.78174
π : ι → Type ?u.78179
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b
rw [← symmDiff_of_le ha]
no goals
ι : Type ?u.78168
α : Type u_1
β : Type ?u.78174
π : ι → Type ?u.78179
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
exact ((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm