[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ ∀ (p q : Bool), p ∆ q = xor p q
[PROOFSTEP]
decide
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b = b ∆ a
[PROOFSTEP]
simp only [symmDiff, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ a = ⊥
[PROOFSTEP]
rw [symmDiff, sup_idem, sdiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ ⊥ = a
[PROOFSTEP]
rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ ⊥ ∆ a = a
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
⊢ a ∆ b = ⊥ ↔ a = b
[PROOFSTEP]
simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a ∆ b = b \ a
[PROOFSTEP]
rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a ∆ b = a \ b
[PROOFSTEP]
rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
[PROOFSTEP]
simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b = (a ⊔ b) \ (a ⊓ b)
[PROOFSTEP]
simp [sup_sdiff, symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : Disjoint a b
⊢ a ∆ b = a ⊔ b
[PROOFSTEP]
rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
[PROOFSTEP]
rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b \ (a ⊓ b) = a ∆ b
[PROOFSTEP]
rw [symmDiff_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
[PROOFSTEP]
simp [symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ (b \ a) = a ⊔ b
[PROOFSTEP]
rw [symmDiff, sdiff_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
[PROOFSTEP]
exact
  le_antisymm (sup_le_sup sdiff_le sdiff_le)
    (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) ∆ b = a ⊔ b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b
[PROOFSTEP]
refine' le_antisymm (sup_le symmDiff_le_sup inf_le_sup) _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
[PROOFSTEP]
rw [sup_inf_left, symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
[PROOFSTEP]
refine' sup_le (le_inf le_sup_right _) (le_inf _ le_sup_right)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b
[PROOFSTEP]
rw [sup_right_comm]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a
[PROOFSTEP]
exact le_sup_of_le_left le_sdiff_sup
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
[PROOFSTEP]
rw [sup_assoc]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)
[PROOFSTEP]
exact le_sup_of_le_right le_sdiff_sup
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊓ b ⊔ a ∆ b = a ⊔ b
[PROOFSTEP]
rw [sup_comm, symmDiff_sup_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
[PROOFSTEP]
rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_symmDiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c
[PROOFSTEP]
refine' (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
[PROOFSTEP]
rw [@sup_comm _ _ (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ b = b ⇔ a
[PROOFSTEP]
simp only [(· ⇔ ·), inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ a = ⊤
[PROOFSTEP]
rw [bihimp, inf_idem, himp_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ ⊤ = a
[PROOFSTEP]
rw [bihimp, himp_top, top_himp, inf_top_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ ⊤ ⇔ a = a
[PROOFSTEP]
rw [bihimp_comm, bihimp_top]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a ⇔ b = b ⇨ a
[PROOFSTEP]
rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a ⇔ b = a ⇨ b
[PROOFSTEP]
rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
[PROOFSTEP]
simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ b = a ⊔ b ⇨ a ⊓ b
[PROOFSTEP]
simp [himp_inf_distrib, bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : Codisjoint a b
⊢ a ⇔ b = a ⊓ b
[PROOFSTEP]
rw [bihimp, h.himp_eq_left, h.himp_eq_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
[PROOFSTEP]
rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⊔ b ⇨ a ⇔ b = a ⇔ b
[PROOFSTEP]
rw [himp_bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
[PROOFSTEP]
simp [bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ ⊤ = ￢a
[PROOFSTEP]
simp [symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ∆ a = ￢a
[PROOFSTEP]
simp [symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤
[PROOFSTEP]
rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
[PROOFSTEP]
exact Codisjoint.top_le codisjoint_hnot_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ (￢a) = ⊤
[PROOFSTEP]
rw [symmDiff_comm, hnot_symmDiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a✝ a b : α
h : IsCompl a b
⊢ a ∆ b = ⊤
[PROOFSTEP]
rw [h.eq_hnot, hnot_symmDiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇔ ⊥ = aᶜ
[PROOFSTEP]
simp [bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : HeytingAlgebra α
a : α
⊢ ⊥ ⇔ a = aᶜ
[PROOFSTEP]
simp [bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : HeytingAlgebra α
a✝ a b : α
h : IsCompl a b
⊢ a ⇔ b = ⊥
[PROOFSTEP]
rw [h.eq_compl, compl_bihimp_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ (a ⊔ b) \ (a ⊓ b) = a ∆ b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint (a ∆ b) (a ⊓ b)
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
[PROOFSTEP]
exact disjoint_sdiff_self_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left, symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
[PROOFSTEP]
simp_rw [@inf_comm _ _ _ c, inf_symmDiff_distrib_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
[PROOFSTEP]
simp only [(· ∆ ·), sdiff_sdiff_sup_sdiff']
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
[PROOFSTEP]
rw [sdiff_symmDiff, sdiff_sup, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ a = b \ a
[PROOFSTEP]
rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ b = a \ b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_sdiff_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ a ∆ b = a ⊓ b
[PROOFSTEP]
simp [sdiff_symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b \ a ∆ b = a ⊓ b
[PROOFSTEP]
rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b
[PROOFSTEP]
refine' ⟨fun h => _, Disjoint.symmDiff_eq_sup⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h 
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b
[PROOFSTEP]
exact h.of_disjoint_inf_of_le le_sup_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ≤ a ∆ b ↔ Disjoint a b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ a ∆ b
⊢ Disjoint a b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf] at h 
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b
[PROOFSTEP]
exact disjoint_iff_inf_le.mpr (le_sdiff_iff.1 <| inf_le_of_left_le h).le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b ≤ a ∆ b ↔ Disjoint a b
[PROOFSTEP]
rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
[PROOFSTEP]
{rw [sdiff_symmDiff', @sup_comm _ _ (c ⊓ a ⊓ b), symmDiff_sdiff]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
[PROOFSTEP]
rw [sdiff_symmDiff', @sup_comm _ _ (c ⊓ a ⊓ b), symmDiff_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
[PROOFSTEP]
ac_rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
[PROOFSTEP]
{rw [sdiff_symmDiff', @sup_comm _ _ (a ⊓ b ⊓ c), symmDiff_sdiff]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
[PROOFSTEP]
rw [sdiff_symmDiff', @sup_comm _ _ (a ⊓ b ⊓ c), symmDiff_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
[PROOFSTEP]
ac_rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)
[PROOFSTEP]
rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ c) = b ∆ (a ∆ c)
[PROOFSTEP]
simp_rw [← symmDiff_assoc, symmDiff_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ c = a ∆ c ∆ b
[PROOFSTEP]
simp_rw [symmDiff_assoc, symmDiff_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
[PROOFSTEP]
simp_rw [symmDiff_assoc, symmDiff_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ (a ∆ b) = b
[PROOFSTEP]
simp [← symmDiff_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b ∆ a ∆ a = b
[PROOFSTEP]
simp [symmDiff_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ a = b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ↔ a ∆ b = a ∆ ⊥
[PROOFSTEP]
rw [symmDiff_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ∆ ⊥ ↔ b = ⊥
[PROOFSTEP]
rw [symmDiff_right_inj]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = b ↔ a = ⊥
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_eq_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c
[PROOFSTEP]
exact (ha.sup_left hb).disjoint_sdiff_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b
[PROOFSTEP]
rw [← symmDiff_of_le ha]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
[PROOFSTEP]
exact ((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
[PROOFSTEP]
simp_rw [← bihimp_assoc, bihimp_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b
[PROOFSTEP]
simp_rw [bihimp_assoc, bihimp_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)
[PROOFSTEP]
simp_rw [bihimp_assoc, bihimp_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ (a ⇔ b) = b
[PROOFSTEP]
simp [← bihimp_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ b ⇔ a ⇔ a = b
[PROOFSTEP]
simp [bihimp_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ a = b
[PROOFSTEP]
rw [bihimp_comm, bihimp_bihimp_cancel_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ
[PROOFSTEP]
simp only [(· ∆ ·), sdiff_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)
[PROOFSTEP]
simp only [(· ⇔ ·), himp_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ (a ∆ b)ᶜ = a ⇔ b
[PROOFSTEP]
simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b
[PROOFSTEP]
simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = ⊤ ↔ IsCompl a b
[PROOFSTEP]
rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff, codisjoint_iff, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
[PROOFSTEP]
rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff, codisjoint_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
[PROOFSTEP]
{rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
[PROOFSTEP]
rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
[PROOFSTEP]
{rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
[PROOFSTEP]
rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
[PROOFSTEP]
congr 1
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ
[PROOFSTEP]
congr 1
[GOAL]
case e_a.e_a
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ
[PROOFSTEP]
rw [inf_comm, inf_assoc]
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c
[PROOFSTEP]
apply inf_left_right_swap
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c
[PROOFSTEP]
trans c \ (a ⊓ b)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)
[PROOFSTEP]
rw [h.eq_bot, sdiff_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
[PROOFSTEP]
rw [sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c
[PROOFSTEP]
exact sup_le_sup le_sup_right le_sup_right
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c
[PROOFSTEP]
simp_rw [symmDiff_comm a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a
[PROOFSTEP]
exact h.le_symmDiff_sup_symmDiff_left
