ι : Type ?u.94740
α : Type u_1
β : Type ?u.94746
π : ι → Type ?u.94751
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a
ι : Type ?u.94740
α : Type u_1
β : Type ?u.94746
π : ι → Type ?u.94751
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c
simp_rw [symmDiff_comm a]
no goals
ι : Type ?u.94740
α : Type u_1
β : Type ?u.94746
π : ι → Type ?u.94751
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a
exact h.le_symmDiff_sup_symmDiff_left