ι : Type ?u.27143
α : Type u_1
β : Type ?u.27149
π : ι → Type ?u.27154
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
ι : Type ?u.27143
α : Type u_1
β : Type ?u.27149
π : ι → Type ?u.27154
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b \ (a ⊓ b) = a ∆ b
rw [symmDiff_sdiff]
no goals
ι : Type ?u.27143
α : Type u_1
β : Type ?u.27149
π : ι → Type ?u.27154
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
simp [symmDiff]