Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Adam Topaz, Bryan Gin-ge Chen, Yaël Dillies
Ported by: Frédéric Dupuis

! This file was ported from Lean 3 source module order.symm_diff
! leanprover-community/mathlib commit 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.BooleanAlgebra
import Mathlib.Logic.Equiv.Basic

/-!
# Symmetric difference and bi-implication

This file defines the symmetric difference and bi-implication operators in (co-)Heyting algebras.

## Examples

Some examples are
* The symmetric difference of two sets is the set of elements that are in either but not both.
* The symmetric difference on propositions is `Xor'`.
* The symmetric difference on `Bool` is `Bool.xor`.
* The equivalence of propositions. Two propositions are equivalent if they imply each other.
* The symmetric difference translates to addition when considering a Boolean algebra as a Boolean
ring.

## Main declarations

* `symmDiff`: The symmetric difference operator, defined as `(a \ b) ⊔ (b \ a)`
* `bihimp`: The bi-implication operator, defined as `(b ⇨ a) ⊓ (a ⇨ b)`

In generalized Boolean algebras, the symmetric difference operator is:

* `symmDiff_comm`: commutative, and
* `symmDiff_assoc`: associative.

## Notations

* `a ∆ b`: `symmDiff a b`
* `a ⇔ b`: `bihimp a b`

## References

The proof of associativity follows the note "Associativity of the Symmetric Difference of Sets: A
Proof from the Book" by John McCuan:

*

## Tags

boolean ring, generalized boolean algebra, boolean algebra, symmetric difference, bi-implication,
Heyting
-/

open Function OrderDual

variable {ι: Type ?u.62901ι α: Type ?u.5α β: Type ?u.62907β : Type _: Type (?u.78448+1)Type _} {π: ι → Type ?u.13π : ι: Type ?u.16ι → Type _: Type (?u.32974+1)Type _}

/-- The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`. -/
def symmDiff: {α : Type u_1} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff [Sup: Type ?u.30 → Type ?u.30Sup α: Type ?u.19α] [SDiff: Type ?u.33 → Type ?u.33SDiff α: Type ?u.19α] (a: αa b: αb : α: Type ?u.19α) : α: Type ?u.19α :=
a: αa \ b: αb ⊔ b: αb \ a: αa
#align symm_diff symmDiff: {α : Type u_1} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff

/-- The Heyting bi-implication is `(b ⇨ a) ⊓ (a ⇨ b)`. This generalizes equivalence of
propositions. -/
def bihimp: [inst : Inf α] → [inst : HImp α] → α → α → αbihimp [Inf: Type ?u.189 → Type ?u.189Inf α: Type ?u.178α] [HImp: Type ?u.192 → Type ?u.192HImp α: Type ?u.178α] (a: αa b: αb : α: Type ?u.178α) : α: Type ?u.178α :=
(b: αb ⇨ a: αa) ⊓ (a: αa ⇨ b: αb)
#align bihimp bihimp: {α : Type u_1} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp

/- This notation might conflict with the Laplacian once we have it. Feel free to put it in locale
`order` or `symmDiff` if that happens. -/
/-- Notation for symmDiff -/
infixl:100 " ∆ " =>  symmDiff: {α : Type u_1} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff

/-- Notation for bihimp -/
infixl:100 " ⇔ " => bihimp: {α : Type u_1} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp

theorem symmDiff_def: ∀ {α : Type u_1} [inst : Sup α] [inst_1 : SDiff α] (a b : α), a ∆ b = a \ b ⊔ b \ asymmDiff_def [Sup: Type ?u.15945 → Type ?u.15945Sup α: Type ?u.15934α] [SDiff: Type ?u.15948 → Type ?u.15948SDiff α: Type ?u.15934α] (a: αa b: αb : α: Type ?u.15934α) : a: αa ∆ b: αb = a: αa \ b: αb ⊔ b: αb \ a: αa :=
rfl: ∀ {α : Sort ?u.16008} {a : α}, a = arfl
#align symm_diff_def symmDiff_def: ∀ {α : Type u_1} [inst : Sup α] [inst_1 : SDiff α] (a b : α), a ∆ b = a \ b ⊔ b \ asymmDiff_def

theorem bihimp_def: ∀ [inst : Inf α] [inst_1 : HImp α] (a b : α), a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)bihimp_def [Inf: Type ?u.16034 → Type ?u.16034Inf α: Type ?u.16023α] [HImp: Type ?u.16037 → Type ?u.16037HImp α: Type ?u.16023α] (a: αa b: αb : α: Type ?u.16023α) : a: αa ⇔ b: αb = (b: αb ⇨ a: αa) ⊓ (a: αa ⇨ b: αb) :=
rfl: ∀ {α : Sort ?u.16090} {a : α}, a = arfl
#align bihimp_def bihimp_def: ∀ {α : Type u_1} [inst : Inf α] [inst_1 : HImp α] (a b : α), a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)bihimp_def

theorem symmDiff_eq_Xor': ∀ (p q : Prop), p ∆ q = Xor' p qsymmDiff_eq_Xor' (p: Propp q: Propq : Prop: TypeProp) : p: Propp ∆ q: Propq = Xor': Prop → Prop → PropXor' p: Propp q: Propq :=
rfl: ∀ {α : Sort ?u.16215} {a : α}, a = arfl
#align symm_diff_eq_xor symmDiff_eq_Xor': ∀ (p q : Prop), p ∆ q = Xor' p qsymmDiff_eq_Xor'

@[simp]
theorem bihimp_iff_iff: ∀ {p q : Prop}, p ⇔ q ↔ (p ↔ q)bihimp_iff_iff {p: Propp q: Propq : Prop: TypeProp} : p: Propp ⇔ q: Propq ↔ (p: Propp ↔ q: Propq) :=
(iff_iff_implies_and_implies: ∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)iff_iff_implies_and_implies _: Prop_ _: Prop_).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans Iff.comm: ∀ {a b : Prop}, (a ↔ b) ↔ (b ↔ a)Iff.comm
#align bihimp_iff_iff bihimp_iff_iff: ∀ {p q : Prop}, p ⇔ q ↔ (p ↔ q)bihimp_iff_iff

@[simp]
theorem Bool.symmDiff_eq_xor: ∀ (p q : Bool), p ∆ q = xor p qBool.symmDiff_eq_xor : ∀ p: Boolp q: Boolq : Bool: TypeBool, p: Boolp ∆ q: Boolq = xor: Bool → Bool → Boolxor p: Boolp q: Boolq := byGoals accomplished! 🐙 ι: Type ?u.16365α: Type ?u.16368β: Type ?u.16371π: ι → Type ?u.16376∀ (p q : Bool), p ∆ q = xor p qdecideGoals accomplished! 🐙
#align bool.symm_diff_eq_bxor Bool.symmDiff_eq_xor: ∀ (p q : Bool), p ∆ q = xor p qBool.symmDiff_eq_xor

section GeneralizedCoheytingAlgebra

variable [GeneralizedCoheytingAlgebra: Type ?u.18827 → Type ?u.18827GeneralizedCoheytingAlgebra α: Type ?u.16635α] (a: αa b: αb c: αc d: αd : α: Type ?u.26727α)

@[simp]
theorem toDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), ↑toDual (a ∆ b) = ↑toDual a ⇔ ↑toDual btoDual_symmDiff : toDual: {α : Type ?u.16658} → α ≃ αᵒᵈtoDual (a: αa ∆ b: αb) = toDual: {α : Type ?u.16804} → α ≃ αᵒᵈtoDual a: αa ⇔ toDual: {α : Type ?u.16869} → α ≃ αᵒᵈtoDual b: αb :=
rfl: ∀ {α : Sort ?u.16986} {a : α}, a = arfl
#align to_dual_symm_diff toDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), ↑toDual (a ∆ b) = ↑toDual a ⇔ ↑toDual btoDual_symmDiff

@[simp]
theorem ofDual_bihimp: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ⇔ b) = ↑ofDual a ∆ ↑ofDual bofDual_bihimp (a: αᵒᵈa b: αᵒᵈb : α: Type ?u.17036αᵒᵈ) : ofDual: {α : Type ?u.17065} → αᵒᵈ ≃ αofDual (a: αᵒᵈa ⇔ b: αᵒᵈb) = ofDual: {α : Type ?u.17217} → αᵒᵈ ≃ αofDual a: αᵒᵈa ∆ ofDual: {α : Type ?u.17282} → αᵒᵈ ≃ αofDual b: αᵒᵈb :=
rfl: ∀ {α : Sort ?u.17411} {a : α}, a = arfl
#align of_dual_bihimp ofDual_bihimp: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ⇔ b) = ↑ofDual a ∆ ↑ofDual bofDual_bihimp

theorem symmDiff_comm: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ asymmDiff_comm : a: αa ∆ b: αb = b: αb ∆ a: αa := byGoals accomplished! 🐙 ι: Type ?u.17458α: Type u_1β: Type ?u.17464π: ι → Type ?u.17469inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b = b ∆ asimp only [symmDiff: {α : Type ?u.17557} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff, sup_comm: ∀ {α : Type ?u.17564} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ asup_comm]Goals accomplished! 🐙
#align symm_diff_comm symmDiff_comm: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ asymmDiff_comm

instance symmDiff_isCommutative: IsCommutative α fun x x_1 => x ∆ x_1symmDiff_isCommutative : IsCommutative: (α : Type ?u.17728) → (α → α → α) → PropIsCommutative α: Type ?u.17706α (· ∆ ·): α → α → α(· ∆ ·) :=
⟨symmDiff_comm: ∀ {α : Type ?u.17833} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ asymmDiff_comm⟩
#align symm_diff_is_comm symmDiff_isCommutative: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α], IsCommutative α fun x x_1 => x ∆ x_1symmDiff_isCommutative

@[simp]
theorem symmDiff_self: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ a = ⊥symmDiff_self : a: αa ∆ a: αa = ⊥: ?m.17971⊥ := byGoals accomplished! 🐙 ι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ a = ⊥rw [ι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ a = ⊥symmDiff: {α : Type ?u.18160} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ a ⊔ a \ a = ⊥ ι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ a = ⊥sup_idem: ∀ {α : Type ?u.18161} [inst : SemilatticeSup α] {a : α}, a ⊔ a = asup_idem,ι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ a = ⊥ ι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ a = ⊥sdiff_self: ∀ {α : Type ?u.18207} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ a = ⊥sdiff_selfι: Type ?u.17889α: Type u_1β: Type ?u.17895π: ι → Type ?u.17900inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α⊥ = ⊥]Goals accomplished! 🐙
#align symm_diff_self symmDiff_self: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ a = ⊥symmDiff_self

@[simp]
theorem symmDiff_bot: a ∆ ⊥ = asymmDiff_bot : a: αa ∆ ⊥: ?m.18291⊥ = a: αa := byGoals accomplished! 🐙 ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ ⊥ = arw [ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ ⊥ = asymmDiff: {α : Type ?u.18505} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ ⊥ ⊔ ⊥ \ a = a ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ ⊥ = asdiff_bot: ∀ {α : Type ?u.18506} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ ⊥ = asdiff_bot,ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ ⊥ \ a = a ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ ⊥ = abot_sdiff: ∀ {α : Type ?u.18541} [inst : GeneralizedCoheytingAlgebra α] {a : α}, ⊥ \ a = ⊥bot_sdiff,ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ ⊥ = a ι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ ⊥ = asup_bot_eq: ∀ {α : Type ?u.18567} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, a ⊔ ⊥ = asup_bot_eqι: Type ?u.18260α: Type u_1β: Type ?u.18266π: ι → Type ?u.18271inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa = a]Goals accomplished! 🐙
#align symm_diff_bot symmDiff_bot: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ ⊥ = asymmDiff_bot

@[simp]
theorem bot_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), ⊥ ∆ a = abot_symmDiff : ⊥: ?m.18844⊥ ∆ a: αa = a: αa := byGoals accomplished! 🐙 ι: Type ?u.18813α: Type u_1β: Type ?u.18819π: ι → Type ?u.18824inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α⊥ ∆ a = arw [ι: Type ?u.18813α: Type u_1β: Type ?u.18819π: ι → Type ?u.18824inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α⊥ ∆ a = asymmDiff_comm: ∀ {α : Type ?u.18962} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ asymmDiff_comm,ι: Type ?u.18813α: Type u_1β: Type ?u.18819π: ι → Type ?u.18824inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ ⊥ = a ι: Type ?u.18813α: Type u_1β: Type ?u.18819π: ι → Type ?u.18824inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α⊥ ∆ a = asymmDiff_bot: ∀ {α : Type ?u.18999} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ ⊥ = asymmDiff_botι: Type ?u.18813α: Type u_1β: Type ?u.18819π: ι → Type ?u.18824inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa = a]Goals accomplished! 🐙
#align bot_symm_diff bot_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), ⊥ ∆ a = abot_symmDiff

@[simp]
theorem symmDiff_eq_bot: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b = ⊥ ↔ a = bsymmDiff_eq_bot {a: αa b: αb : α: Type ?u.19060α} : a: αa ∆ b: αb = ⊥: ?m.19143⊥ ↔ a: αa = b: αb := byGoals accomplished! 🐙
ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa ∆ b = ⊥ ↔ a = bsimp_rw [ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa ∆ b = ⊥ ↔ a = bsymmDiff: {α : Type ?u.19309} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa \ b ⊔ b \ a = ⊥ ↔ a = b ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa ∆ b = ⊥ ↔ a = bsup_eq_bot_iff: ∀ {α : Type ?u.19439} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a b : α}, a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥sup_eq_bot_iff,ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa \ b = ⊥ ∧ b \ a = ⊥ ↔ a = b ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa ∆ b = ⊥ ↔ a = bsdiff_eq_bot_iff: ∀ {α : Type ?u.19723} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ bsdiff_eq_bot_iff,ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa ≤ b ∧ b ≤ a ↔ a = b ι: Type ?u.19057α: Type u_1β: Type ?u.19063π: ι → Type ?u.19068inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αa ∆ b = ⊥ ↔ a = ble_antisymm_iff: ∀ {α : Type ?u.19890} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ b ≤ ale_antisymm_iffGoals accomplished! 🐙]Goals accomplished! 🐙
#align symm_diff_eq_bot symmDiff_eq_bot: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b = ⊥ ↔ a = bsymmDiff_eq_bot

theorem symmDiff_of_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → a ∆ b = b \ asymmDiff_of_le {a: αa b: αb : α: Type ?u.20050α} (h: a ≤ bh : a: αa ≤ b: αb) : a: αa ∆ b: αb = b: αb \ a: αa := byGoals accomplished! 🐙
ι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ∆ b = b \ arw [ι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ∆ b = b \ asymmDiff: {α : Type ?u.20290} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba \ b ⊔ b \ a = b \ a ι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ∆ b = b \ asdiff_eq_bot_iff: ∀ {α : Type ?u.20291} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ bsdiff_eq_bot_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: a ≤ bh,ι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ b⊥ ⊔ b \ a = b \ a ι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ∆ b = b \ abot_sup_eq: ∀ {α : Type ?u.20341} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, ⊥ ⊔ a = abot_sup_eqι: Type ?u.20047α: Type u_1β: Type ?u.20053π: ι → Type ?u.20058inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ bb \ a = b \ a]Goals accomplished! 🐙
#align symm_diff_of_le symmDiff_of_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → a ∆ b = b \ asymmDiff_of_le

theorem symmDiff_of_ge: ∀ {a b : α}, b ≤ a → a ∆ b = a \ bsymmDiff_of_ge {a: αa b: αb : α: Type ?u.20572α} (h: b ≤ ah : b: αb ≤ a: αa) : a: αa ∆ b: αb = a: αa \ b: αb := byGoals accomplished! 🐙
ι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ∆ b = a \ brw [ι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ∆ b = a \ bsymmDiff: {α : Type ?u.20812} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa \ b ⊔ b \ a = a \ b ι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ∆ b = a \ bsdiff_eq_bot_iff: ∀ {α : Type ?u.20813} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ bsdiff_eq_bot_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: b ≤ ah,ι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa \ b ⊔ ⊥ = a \ b ι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ∆ b = a \ bsup_bot_eq: ∀ {α : Type ?u.20863} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, a ⊔ ⊥ = asup_bot_eqι: Type ?u.20569α: Type u_1β: Type ?u.20575π: ι → Type ?u.20580inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa \ b = a \ b]Goals accomplished! 🐙
#align symm_diff_of_ge symmDiff_of_ge: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ a → a ∆ b = a \ bsymmDiff_of_ge

theorem symmDiff_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → a ∆ b ≤ csymmDiff_le {a: αa b: αb c: αc : α: Type ?u.21094α} (ha: a ≤ b ⊔ cha : a: αa ≤ b: αb ⊔ c: αc) (hb: b ≤ a ⊔ chb : b: αb ≤ a: αa ⊔ c: αc) : a: αa ∆ b: αb ≤ c: αc :=
sup_le: ∀ {α : Type ?u.21238} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le (sdiff_le_iff: ∀ {α : Type ?u.21288} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ csdiff_le_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ha: a ≤ b ⊔ cha) <| sdiff_le_iff: ∀ {α : Type ?u.21324} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ csdiff_le_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hb: b ≤ a ⊔ chb
#align symm_diff_le symmDiff_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → a ∆ b ≤ csymmDiff_le

theorem symmDiff_le_iff: ∀ {a b c : α}, a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csymmDiff_le_iff {a: αa b: αb c: αc : α: Type ?u.21358α} : a: αa ∆ b: αb ≤ c: αc ↔ a: αa ≤ b: αb ⊔ c: αc ∧ b: αb ≤ a: αa ⊔ c: αc := byGoals accomplished! 🐙
ι: Type ?u.21355α: Type u_1β: Type ?u.21361π: ι → Type ?u.21366inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csimp_rw [ι: Type ?u.21355α: Type u_1β: Type ?u.21361π: ι → Type ?u.21366inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csymmDiff: {α : Type ?u.21606} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.21355α: Type u_1β: Type ?u.21361π: ι → Type ?u.21366inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa \ b ⊔ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c ι: Type ?u.21355α: Type u_1β: Type ?u.21361π: ι → Type ?u.21366inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csup_le_iff: ∀ {α : Type ?u.21700} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ csup_le_iff,ι: Type ?u.21355α: Type u_1β: Type ?u.21361π: ι → Type ?u.21366inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa \ b ≤ c ∧ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c ι: Type ?u.21355α: Type u_1β: Type ?u.21361π: ι → Type ?u.21366inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csdiff_le_iff: ∀ {α : Type ?u.21874} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ csdiff_le_iffGoals accomplished! 🐙]Goals accomplished! 🐙
#align symm_diff_le_iff symmDiff_le_iff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csymmDiff_le_iff

@[simp]
theorem symmDiff_le_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b ≤ a ⊔ bsymmDiff_le_sup {a: αa b: αb : α: Type ?u.22046α} : a: αa ∆ b: αb ≤ a: αa ⊔ b: αb :=
sup_le_sup: ∀ {α : Type ?u.22169} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ dsup_le_sup sdiff_le: ∀ {α : Type ?u.22220} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ asdiff_le sdiff_le: ∀ {α : Type ?u.22249} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ asdiff_le
#align symm_diff_le_sup symmDiff_le_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b ≤ a ⊔ bsymmDiff_le_sup

theorem symmDiff_eq_sup_sdiff_inf: a ∆ b = (a ⊔ b) \ (a ⊓ b)symmDiff_eq_sup_sdiff_inf : a: αa ∆ b: αb = (a: αa ⊔ b: αb) \ (a: αa ⊓ b: αb) := byGoals accomplished! 🐙 ι: Type ?u.22302α: Type u_1β: Type ?u.22308π: ι → Type ?u.22313inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b = (a ⊔ b) \ (a ⊓ b)simp [sup_sdiff: ∀ {α : Type ?u.22435} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a ⊔ b) \ c = a \ c ⊔ b \ csup_sdiff, symmDiff: {α : Type ?u.22455} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff]Goals accomplished! 🐙
#align symm_diff_eq_sup_sdiff_inf symmDiff_eq_sup_sdiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = (a ⊔ b) \ (a ⊓ b)symmDiff_eq_sup_sdiff_inf

theorem Disjoint.symmDiff_eq_sup: ∀ {a b : α}, Disjoint a b → a ∆ b = a ⊔ bDisjoint.symmDiff_eq_sup {a: αa b: αb : α: Type ?u.26275α} (h: Disjoint a bh : Disjoint: {α : Type ?u.26301} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint a: αa b: αb) : a: αa ∆ b: αb = a: αa ⊔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba ∆ b = a ⊔ brw [ι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba ∆ b = a ⊔ bsymmDiff: {α : Type ?u.26662} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba \ b ⊔ b \ a = a ⊔ b ι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba ∆ b = a ⊔ bh: Disjoint a bh.sdiff_eq_left: ∀ {α : Type ?u.26663} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → a \ b = asdiff_eq_left,ι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba ⊔ b \ a = a ⊔ b ι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba ∆ b = a ⊔ bh: Disjoint a bh.sdiff_eq_right: ∀ {α : Type ?u.26696} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → b \ a = bsdiff_eq_rightι: Type ?u.26272α: Type u_1β: Type ?u.26278π: ι → Type ?u.26283inst✝: GeneralizedCoheytingAlgebra αa✝, b✝, c, d, a, b: αh: Disjoint a ba ⊔ b = a ⊔ b]Goals accomplished! 🐙
#align disjoint.symm_diff_eq_sup Disjoint.symmDiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → a ∆ b = a ⊔ bDisjoint.symmDiff_eq_sup

theorem symmDiff_sdiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)symmDiff_sdiff : a: αa ∆ b: αb \ c: αc = a: αa \ (b: αb ⊔ c: αc) ⊔ b: αb \ (a: αa ⊔ c: αc) := byGoals accomplished! 🐙
ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)rw [ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)symmDiff: {α : Type ?u.27010} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)sup_sdiff_distrib: ∀ {α : Type ?u.27011} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), (a ⊔ b) \ c = a \ c ⊔ b \ csup_sdiff_distrib,ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a \ b) \ c ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)sdiff_sdiff_left: ∀ {α : Type ?u.27053} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = a \ (b ⊔ c)sdiff_sdiff_left,ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ (b ⊔ c) ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)sdiff_sdiff_left: ∀ {α : Type ?u.27081} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = a \ (b ⊔ c)sdiff_sdiff_leftι: Type ?u.26724α: Type u_1β: Type ?u.26730π: ι → Type ?u.26735inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ (b ⊔ c) ⊔ b \ (a ⊔ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)]Goals accomplished! 🐙
#align symm_diff_sdiff symmDiff_sdiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)symmDiff_sdiff

@[simp]
theorem symmDiff_sdiff_inf: a ∆ b \ (a ⊓ b) = a ∆ bsymmDiff_sdiff_inf : a: αa ∆ b: αb \ (a: αa ⊓ b: αb) = a: αa ∆ b: αb := byGoals accomplished! 🐙
ι: Type ?u.27143α: Type u_1β: Type ?u.27149π: ι → Type ?u.27154inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ (a ⊓ b) = a ∆ brw [ι: Type ?u.27143α: Type u_1β: Type ?u.27149π: ι → Type ?u.27154inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ (a ⊓ b) = a ∆ bsymmDiff_sdiff: ∀ {α : Type ?u.27289} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)symmDiff_sdiffι: Type ?u.27143α: Type u_1β: Type ?u.27149π: ι → Type ?u.27154inst✝: 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.27154inst✝: 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.27154inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b \ (a ⊓ b) = a ∆ bsimp [symmDiff: {α : Type ?u.27352} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff]Goals accomplished! 🐙
#align symm_diff_sdiff_inf symmDiff_sdiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b \ (a ⊓ b) = a ∆ bsymmDiff_sdiff_inf

@[simp]
theorem symmDiff_sdiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ bsymmDiff_sdiff_eq_sup : a: αa ∆ (b: αb \ a: αa) = a: αa ⊔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ (b \ a) = a ⊔ brw [ι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ (b \ a) = a ⊔ bsymmDiff: {α : Type ?u.32236} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ (b \ a) ⊔ (b \ a) \ a = a ⊔ b ι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ (b \ a) = a ⊔ bsdiff_idem: ∀ {α : Type ?u.32237} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a \ b) \ b = a \ bsdiff_idemι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ (b \ a) ⊔ b \ a = a ⊔ b]ι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ (b \ a) ⊔ b \ a = a ⊔ b
ι: Type ?u.32022α: Type u_1β: Type ?u.32028π: ι → Type ?u.32033inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ (b \ a) = a ⊔ bexact
le_antisymm: ∀ {α : Type ?u.32325} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm (sup_le_sup: ∀ {α : Type ?u.32348} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ dsup_le_sup sdiff_le: ∀ {α : Type ?u.32413} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ asdiff_le sdiff_le: ∀ {α : Type ?u.32439} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ asdiff_le)
(sup_le: ∀ {α : Type ?u.32461} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le le_sdiff_sup: ∀ {α : Type ?u.32485} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ ble_sdiff_sup <| le_sdiff_sup: ∀ {α : Type ?u.32511} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ ble_sdiff_sup.trans: ∀ {α : Type ?u.32525} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ ctrans <| sup_le: ∀ {α : Type ?u.32591} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le le_sup_right: ∀ {α : Type ?u.32615} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ ble_sup_right le_sdiff_sup: ∀ {α : Type ?u.32638} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ ble_sdiff_sup)Goals accomplished! 🐙
#align symm_diff_sdiff_eq_sup symmDiff_sdiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ bsymmDiff_sdiff_eq_sup

@[simp]
theorem sdiff_symmDiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ bsdiff_symmDiff_eq_sup : (a: αa \ b: αb) ∆ b: αb = a: αa ⊔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a \ b) ∆ b = a ⊔ brw [ι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a \ b) ∆ b = a ⊔ bsymmDiff_comm: ∀ {α : Type ?u.32806} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ asymmDiff_comm,ι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αb ∆ (a \ b) = a ⊔ b ι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a \ b) ∆ b = a ⊔ bsymmDiff_sdiff_eq_sup: ∀ {α : Type ?u.32843} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ bsymmDiff_sdiff_eq_sup,ι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αb ⊔ a = a ⊔ b ι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a \ b) ∆ b = a ⊔ bsup_comm: ∀ {α : Type ?u.32882} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ asup_commι: Type ?u.32704α: Type u_1β: Type ?u.32710π: ι → Type ?u.32715inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b = a ⊔ b]Goals accomplished! 🐙
#align sdiff_symm_diff_eq_sup sdiff_symmDiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ bsdiff_symmDiff_eq_sup

@[simp]
theorem symmDiff_sup_inf: a ∆ b ⊔ a ⊓ b = a ⊔ bsymmDiff_sup_inf : a: αa ∆ b: αb ⊔ a: αa ⊓ b: αb = a: αa ⊔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ brefine' le_antisymm: ∀ {α : Type ?u.33108} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm (sup_le: ∀ {α : Type ?u.33131} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le symmDiff_le_sup: ∀ {α : Type ?u.33200} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b ≤ a ⊔ bsymmDiff_le_sup inf_le_sup: ∀ {α : Type ?u.33232} [inst : Lattice α] {a b : α}, a ⊓ b ≤ a ⊔ binf_le_sup) _: ?m.33112 ≤ ?m.33111_ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b ≤ a ∆ b ⊔ a ⊓ b
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ brw [ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b ≤ a ∆ b ⊔ a ⊓ bsup_inf_left: ∀ {α : Type ?u.33274} [inst : DistribLattice α] {x y z : α}, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)sup_inf_left,ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b ≤ (a ∆ b ⊔ a) ⊓ (a ∆ b ⊔ b) ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b ≤ a ∆ b ⊔ a ⊓ bsymmDiff: {α : Type ?u.33502} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiffι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)]ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ brefine' sup_le: ∀ {α : Type ?u.33550} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le (le_inf: ∀ {α : Type ?u.33574} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ cle_inf le_sup_right: ∀ {α : Type ?u.33610} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ ble_sup_right _: ?m.33577 ≤ ?m.33579_) (le_inf: ∀ {α : Type ?u.33640} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ cle_inf _: ?m.33643 ≤ ?m.33644_ le_sup_right: ∀ {α : Type ?u.33665} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ ble_sup_right)ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b \ a ⊔ bι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ b \ a ⊔ a
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ b·ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b \ a ⊔ b ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b \ a ⊔ bι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ b \ a ⊔ arw [ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b \ a ⊔ bsup_right_comm: ∀ {α : Type ?u.33688} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ bsup_right_commι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b ⊔ b \ a]ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b ⊔ b \ a
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_1a ≤ a \ b ⊔ b \ a ⊔ bexact le_sup_of_le_left: ∀ {α : Type ?u.33768} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ ble_sup_of_le_left le_sdiff_sup: ∀ {α : Type ?u.33792} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ ble_sdiff_supGoals accomplished! 🐙
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ b·ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ b \ a ⊔ a ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ b \ a ⊔ arw [ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ b \ a ⊔ asup_assoc: ∀ {α : Type ?u.33822} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ⊔ c = a ⊔ (b ⊔ c)sup_assocι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ (b \ a ⊔ a)]ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ (b \ a ⊔ a)
ι: Type ?u.32963α: Type u_1β: Type ?u.32969π: ι → Type ?u.32974inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αrefine'_2b ≤ a \ b ⊔ b \ a ⊔ aexact le_sup_of_le_right: ∀ {α : Type ?u.33899} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ ble_sup_of_le_right le_sdiff_sup: ∀ {α : Type ?u.33923} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ ble_sdiff_supGoals accomplished! 🐙
#align symm_diff_sup_inf symmDiff_sup_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ bsymmDiff_sup_inf

@[simp]
theorem inf_sup_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ a ∆ b = a ⊔ binf_sup_symmDiff : a: αa ⊓ b: αb ⊔ a: αa ∆ b: αb = a: αa ⊔ b: αb := byGoals accomplished! 🐙 ι: Type ?u.33973α: Type u_1β: Type ?u.33979π: ι → Type ?u.33984inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊓ b ⊔ a ∆ b = a ⊔ brw [ι: Type ?u.33973α: Type u_1β: Type ?u.33979π: ι → Type ?u.33984inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊓ b ⊔ a ∆ b = a ⊔ bsup_comm: ∀ {α : Type ?u.34118} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ asup_comm,ι: Type ?u.33973α: Type u_1β: Type ?u.33979π: ι → Type ?u.33984inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ b ι: Type ?u.33973α: Type u_1β: Type ?u.33979π: ι → Type ?u.33984inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊓ b ⊔ a ∆ b = a ⊔ bsymmDiff_sup_inf: ∀ {α : Type ?u.34170} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ bsymmDiff_sup_infι: Type ?u.33973α: Type u_1β: Type ?u.33979π: ι → Type ?u.33984inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b = a ⊔ b]Goals accomplished! 🐙
#align inf_sup_symm_diff inf_sup_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ a ∆ b = a ⊔ binf_sup_symmDiff

@[simp]
theorem symmDiff_symmDiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ bsymmDiff_symmDiff_inf : a: αa ∆ b: αb ∆ (a: αa ⊓ b: αb) = a: αa ⊔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ∆ (a ⊓ b) = a ⊔ brw [ι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ∆ (a ⊓ b) = a ⊔ b← symmDiff_sdiff_inf: ∀ {α : Type ?u.34395} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b \ (a ⊓ b) = a ∆ bsymmDiff_sdiff_inf a: αa,ι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b ι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ∆ (a ⊓ b) = a ⊔ bsdiff_symmDiff_eq_sup: ∀ {α : Type ?u.34412} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ bsdiff_symmDiff_eq_sup,ι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ⊔ a ⊓ b = a ⊔ b ι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ∆ (a ⊓ b) = a ⊔ bsymmDiff_sup_inf: ∀ {α : Type ?u.34451} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ bsymmDiff_sup_infι: Type ?u.34249α: Type u_1β: Type ?u.34255π: ι → Type ?u.34260inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b = a ⊔ b]Goals accomplished! 🐙
#align symm_diff_symm_diff_inf symmDiff_symmDiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ bsymmDiff_symmDiff_inf

@[simp]
theorem inf_symmDiff_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a ⊓ b) ∆ (a ∆ b) = a ⊔ binf_symmDiff_symmDiff : (a: αa ⊓ b: αb) ∆ (a: αa ∆ b: αb) = a: αa ⊔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.34523α: Type u_1β: Type ?u.34529π: ι → Type ?u.34534inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a ⊓ b) ∆ (a ∆ b) = a ⊔ brw [ι: Type ?u.34523α: Type u_1β: Type ?u.34529π: ι → Type ?u.34534inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a ⊓ b) ∆ (a ∆ b) = a ⊔ bsymmDiff_comm: ∀ {α : Type ?u.34669} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ asymmDiff_comm,ι: Type ?u.34523α: Type u_1β: Type ?u.34529π: ι → Type ?u.34534inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ b ∆ (a ⊓ b) = a ⊔ b ι: Type ?u.34523α: Type u_1β: Type ?u.34529π: ι → Type ?u.34534inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: α(a ⊓ b) ∆ (a ∆ b) = a ⊔ bsymmDiff_symmDiff_inf: ∀ {α : Type ?u.34706} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ bsymmDiff_symmDiff_infι: Type ?u.34523α: Type u_1β: Type ?u.34529π: ι → Type ?u.34534inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ⊔ b = a ⊔ b]Goals accomplished! 🐙
#align inf_symm_diff_symm_diff inf_symmDiff_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a ⊓ b) ∆ (a ∆ b) = a ⊔ binf_symmDiff_symmDiff

theorem symmDiff_triangle: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ c ≤ a ∆ b ⊔ b ∆ csymmDiff_triangle : a: αa ∆ c: αc ≤ a: αa ∆ b: αb ⊔ b: αb ∆ c: αc := byGoals accomplished! 🐙
ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ c ≤ a ∆ b ⊔ b ∆ crefine' (sup_le_sup: ∀ {α : Type ?u.34950} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ dsup_le_sup (sdiff_triangle: ∀ {α : Type ?u.34957} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a \ c ≤ a \ b ⊔ b \ csdiff_triangle a: αa b: αb c: αc) <| sdiff_triangle: ∀ {α : Type ?u.34986} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a \ c ≤ a \ b ⊔ b \ csdiff_triangle _: ?m.34987_ b: αb _: ?m.34987_).trans_eq: ∀ {α : Type ?u.34995} [inst : Preorder α] {a b c : α}, a ≤ b → b = c → a ≤ ctrans_eq _: ?m.35006 = ?m.35007_ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa ∆ c ≤ a ∆ b ⊔ b ∆ crw [ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c@sup_comm: ∀ {α : Type ?u.35042} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ asup_comm _: Type ?u.35042_ _ (c: αc \ b: αb),ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ csup_sup_sup_comm: ∀ {α : Type ?u.35113} [inst : SemilatticeSup α] (a b c d : α), a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)sup_sup_sup_comm,ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a ∆ b ⊔ b ∆ c ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ csymmDiff: {α : Type ?u.35231} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff,ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ b ∆ c ι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ csymmDiff: {α : Type ?u.35289} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiffι: Type ?u.34775α: Type u_1β: Type ?u.34781π: ι → Type ?u.34786inst✝: GeneralizedCoheytingAlgebra αa, b, c, d: αa \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b)]Goals accomplished! 🐙
#align symm_diff_triangle symmDiff_triangle: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ c ≤ a ∆ b ⊔ b ∆ csymmDiff_triangle

end GeneralizedCoheytingAlgebra

section GeneralizedHeytingAlgebra

variable [GeneralizedHeytingAlgebra: Type ?u.38081 → Type ?u.38081GeneralizedHeytingAlgebra α: Type ?u.35332α] (a: αa b: αb c: αc d: αd : α: Type ?u.35307α)

@[simp]
theorem toDual_bihimp: ↑toDual (a ⇔ b) = ↑toDual a ∆ ↑toDual btoDual_bihimp : toDual: {α : Type ?u.35355} → α ≃ αᵒᵈtoDual (a: αa ⇔ b: αb) = toDual: {α : Type ?u.35505} → α ≃ αᵒᵈtoDual a: αa ∆ toDual: {α : Type ?u.35570} → α ≃ αᵒᵈtoDual b: αb :=
rfl: ∀ {α : Sort ?u.35714} {a : α}, a = arfl
#align to_dual_bihimp toDual_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), ↑toDual (a ⇔ b) = ↑toDual a ∆ ↑toDual btoDual_bihimp

@[simp]
theorem ofDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ∆ b) = ↑ofDual a ⇔ ↑ofDual bofDual_symmDiff (a: αᵒᵈa b: αᵒᵈb : α: Type ?u.35764αᵒᵈ) : ofDual: {α : Type ?u.35793} → αᵒᵈ ≃ αofDual (a: αᵒᵈa ∆ b: αᵒᵈb) = ofDual: {α : Type ?u.35973} → αᵒᵈ ≃ αofDual a: αᵒᵈa ⇔ ofDual: {α : Type ?u.36038} → αᵒᵈ ≃ αofDual b: αᵒᵈb :=
rfl: ∀ {α : Sort ?u.36164} {a : α}, a = arfl
#align of_dual_symm_diff ofDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ∆ b) = ↑ofDual a ⇔ ↑ofDual bofDual_symmDiff

theorem bihimp_comm: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ abihimp_comm : a: αa ⇔ b: αb = b: αb ⇔ a: αa := byGoals accomplished! 🐙 ι: Type ?u.36211α: Type u_1β: Type ?u.36217π: ι → Type ?u.36222inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ b = b ⇔ asimp only [(· ⇔ ·), inf_comm: ∀ {α : Type ?u.36320} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ⊓ ainf_comm]Goals accomplished! 🐙
#align bihimp_comm bihimp_comm: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ abihimp_comm

instance bihimp_isCommutative: IsCommutative α fun x x_1 => x ⇔ x_1bihimp_isCommutative : IsCommutative: (α : Type ?u.36518) → (α → α → α) → PropIsCommutative α: Type ?u.36496α (· ⇔ ·): α → α → α(· ⇔ ·) :=
⟨bihimp_comm: ∀ {α : Type ?u.36627} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ abihimp_comm⟩
#align bihimp_is_comm bihimp_isCommutative: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α], IsCommutative α fun x x_1 => x ⇔ x_1bihimp_isCommutative

@[simp]
theorem bihimp_self: a ⇔ a = ⊤bihimp_self : a: αa ⇔ a: αa = ⊤: ?m.36766⊤ := byGoals accomplished! 🐙 ι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ a = ⊤rw [ι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ a = ⊤bihimp: {α : Type ?u.36943} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α(a ⇨ a) ⊓ (a ⇨ a) = ⊤ ι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ a = ⊤inf_idem: ∀ {α : Type ?u.36944} [inst : SemilatticeInf α] {a : α}, a ⊓ a = ainf_idem,ι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ a = ⊤ ι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ a = ⊤himp_self: ∀ {α : Type ?u.37007} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ a = ⊤himp_selfι: Type ?u.36681α: Type u_1β: Type ?u.36687π: ι → Type ?u.36692inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α⊤ = ⊤]Goals accomplished! 🐙
#align bihimp_self bihimp_self: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ a = ⊤bihimp_self

@[simp]
theorem bihimp_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ ⊤ = abihimp_top : a: αa ⇔ ⊤: ?m.37088⊤ = a: αa := byGoals accomplished! 🐙 ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ ⊤ = arw [ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ ⊤ = abihimp: {α : Type ?u.37297} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α(⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ ⊤ = ahimp_top: ∀ {α : Type ?u.37298} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ ⊤ = ⊤himp_top,ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α(⊤ ⇨ a) ⊓ ⊤ = a ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ ⊤ = atop_himp: ∀ {α : Type ?u.37344} [inst : GeneralizedHeytingAlgebra α] {a : α}, ⊤ ⇨ a = atop_himp,ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⊓ ⊤ = a ι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ ⊤ = ainf_top_eq: ∀ {α : Type ?u.37368} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = ainf_top_eqι: Type ?u.37057α: Type u_1β: Type ?u.37063π: ι → Type ?u.37068inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa = a]Goals accomplished! 🐙
#align bihimp_top bihimp_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ ⊤ = abihimp_top

@[simp]
theorem top_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), ⊤ ⇔ a = atop_bihimp : ⊤: ?m.37665⊤ ⇔ a: αa = a: αa := byGoals accomplished! 🐙 ι: Type ?u.37634α: Type u_1β: Type ?u.37640π: ι → Type ?u.37645inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α⊤ ⇔ a = arw [ι: Type ?u.37634α: Type u_1β: Type ?u.37640π: ι → Type ?u.37645inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α⊤ ⇔ a = abihimp_comm: ∀ {α : Type ?u.37769} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ abihimp_comm,ι: Type ?u.37634α: Type u_1β: Type ?u.37640π: ι → Type ?u.37645inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ ⊤ = a ι: Type ?u.37634α: Type u_1β: Type ?u.37640π: ι → Type ?u.37645inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α⊤ ⇔ a = abihimp_top: ∀ {α : Type ?u.37803} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ ⊤ = abihimp_topι: Type ?u.37634α: Type u_1β: Type ?u.37640π: ι → Type ?u.37645inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa = a]Goals accomplished! 🐙
#align top_bihimp top_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), ⊤ ⇔ a = atop_bihimp

@[simp]
theorem bihimp_eq_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇔ b = ⊤ ↔ a = bbihimp_eq_top {a: αa b: αb : α: Type ?u.37860α} : a: αa ⇔ b: αb = ⊤: ?m.37946⊤ ↔ a: αa = b: αb :=
@symmDiff_eq_bot: ∀ {α : Type ?u.37999} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b = ⊥ ↔ a = bsymmDiff_eq_bot α: Type ?u.37860αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align bihimp_eq_top bihimp_eq_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇔ b = ⊤ ↔ a = bbihimp_eq_top

theorem bihimp_of_le: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b → a ⇔ b = b ⇨ abihimp_of_le {a: αa b: αb : α: Type ?u.38070α} (h: a ≤ bh : a: αa ≤ b: αb) : a: αa ⇔ b: αb = b: αb ⇨ a: αa := byGoals accomplished! 🐙
ι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ⇔ b = b ⇨ arw [ι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ⇔ b = b ⇨ abihimp: {α : Type ?u.38334} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ b(b ⇨ a) ⊓ (a ⇨ b) = b ⇨ a ι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ⇔ b = b ⇨ ahimp_eq_top_iff: ∀ {α : Type ?u.38335} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇨ b = ⊤ ↔ a ≤ bhimp_eq_top_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: a ≤ bh,ι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ b(b ⇨ a) ⊓ ⊤ = b ⇨ a ι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ ba ⇔ b = b ⇨ ainf_top_eq: ∀ {α : Type ?u.38383} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = ainf_top_eqι: Type ?u.38067α: Type u_1β: Type ?u.38073π: ι → Type ?u.38078inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: a ≤ bb ⇨ a = b ⇨ a]Goals accomplished! 🐙
#align bihimp_of_le bihimp_of_le: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b → a ⇔ b = b ⇨ abihimp_of_le

theorem bihimp_of_ge: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ≤ a → a ⇔ b = a ⇨ bbihimp_of_ge {a: αa b: αb : α: Type ?u.38630α} (h: b ≤ ah : b: αb ≤ a: αa) : a: αa ⇔ b: αb = a: αa ⇨ b: αb := byGoals accomplished! 🐙
ι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ⇔ b = a ⇨ brw [ι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ⇔ b = a ⇨ bbihimp: {α : Type ?u.38894} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ a(b ⇨ a) ⊓ (a ⇨ b) = a ⇨ b ι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ⇔ b = a ⇨ bhimp_eq_top_iff: ∀ {α : Type ?u.38895} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇨ b = ⊤ ↔ a ≤ bhimp_eq_top_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: b ≤ ah,ι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ a⊤ ⊓ (a ⇨ b) = a ⇨ b ι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ⇔ b = a ⇨ btop_inf_eq: ∀ {α : Type ?u.38943} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, ⊤ ⊓ a = atop_inf_eqι: Type ?u.38627α: Type u_1β: Type ?u.38633π: ι → Type ?u.38638inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: b ≤ aa ⇨ b = a ⇨ b]Goals accomplished! 🐙
#align bihimp_of_ge bihimp_of_ge: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ≤ a → a ⇔ b = a ⇨ bbihimp_of_ge

theorem le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ⊓ b ≤ c → a ⊓ c ≤ b → a ≤ b ⇔ cle_bihimp {a: αa b: αb c: αc : α: Type ?u.39190α} (hb: a ⊓ b ≤ chb : a: αa ⊓ b: αb ≤ c: αc) (hc: a ⊓ c ≤ bhc : a: αa ⊓ c: αc ≤ b: αb) : a: αa ≤ b: αb ⇔ c: αc :=
le_inf: ∀ {α : Type ?u.39353} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ cle_inf (le_himp_iff: ∀ {α : Type ?u.39427} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ cle_himp_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hc: a ⊓ c ≤ bhc) <| le_himp_iff: ∀ {α : Type ?u.39457} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ cle_himp_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hb: a ⊓ b ≤ chb
#align le_bihimp le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ⊓ b ≤ c → a ⊓ c ≤ b → a ≤ b ⇔ cle_bihimp

theorem le_bihimp_iff: ∀ {a b c : α}, a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ ble_bihimp_iff {a: αa b: αb c: αc : α: Type ?u.39496α} : a: αa ≤ b: αb ⇔ c: αc ↔ a: αa ⊓ b: αb ≤ c: αc ∧ a: αa ⊓ c: αc ≤ b: αb := byGoals accomplished! 🐙
ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ bsimp_rw [ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ bbihimp: {α : Type ?u.39757} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ (c ⇨ b) ⊓ (b ⇨ c) ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ ble_inf_iff: ∀ {α : Type ?u.39854} [inst : SemilatticeInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ cle_inf_iff,ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ c ⇨ b ∧ a ≤ b ⇨ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ ble_himp_iff: ∀ {α : Type ?u.40040} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ cle_himp_iff,ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ⊓ c ≤ b ∧ a ⊓ b ≤ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b ι: Type ?u.39493α: Type u_1β: Type ?u.39499π: ι → Type ?u.39504inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c✝, d, a, b, c: αa ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ band_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ aand_commGoals accomplished! 🐙]Goals accomplished! 🐙
#align le_bihimp_iff le_bihimp_iff: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ ble_bihimp_iff

@[simp]
theorem inf_le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⊓ b ≤ a ⇔ binf_le_bihimp {a: αa b: αb : α: Type ?u.40298α} : a: αa ⊓ b: αb ≤ a: αa ⇔ b: αb :=
inf_le_inf: ∀ {α : Type ?u.40440} [inst : SemilatticeInf α] {a b c d : α}, a ≤ b → c ≤ d → a ⊓ c ≤ b ⊓ dinf_le_inf le_himp: ∀ {α : Type ?u.40515} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b ⇨ ale_himp le_himp: ∀ {α : Type ?u.40540} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b ⇨ ale_himp
#align inf_le_bihimp inf_le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⊓ b ≤ a ⇔ binf_le_bihimp

theorem bihimp_eq_inf_himp_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = a ⊔ b ⇨ a ⊓ bbihimp_eq_inf_himp_inf : a: αa ⇔ b: αb = a: αa ⊔ b: αb ⇨ a: αa ⊓ b: αb := byGoals accomplished! 🐙 ι: Type ?u.40596α: Type u_1β: Type ?u.40602π: ι → Type ?u.40607inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇔ b = a ⊔ b ⇨ a ⊓ bsimp [himp_inf_distrib: ∀ {α : Type ?u.40752} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)himp_inf_distrib, bihimp: {α : Type ?u.40772} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp]Goals accomplished! 🐙
#align bihimp_eq_inf_himp_inf bihimp_eq_inf_himp_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = a ⊔ b ⇨ a ⊓ bbihimp_eq_inf_himp_inf

theorem Codisjoint.bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇔ b = a ⊓ bCodisjoint.bihimp_eq_inf {a: αa b: αb : α: Type ?u.44595α} (h: Codisjoint a bh : Codisjoint: {α : Type ?u.44621} → [inst : PartialOrder α] → [inst : OrderTop α] → α → α → PropCodisjoint a: αa b: αb) : a: αa ⇔ b: αb = a: αa ⊓ b: αb := byGoals accomplished! 🐙
ι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a ba ⇔ b = a ⊓ brw [ι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a ba ⇔ b = a ⊓ bbihimp: {α : Type ?u.44989} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a b(b ⇨ a) ⊓ (a ⇨ b) = a ⊓ b ι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a ba ⇔ b = a ⊓ bh: Codisjoint a bh.himp_eq_left: ∀ {α : Type ?u.44990} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇨ b = bhimp_eq_left,ι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a b(b ⇨ a) ⊓ b = a ⊓ b ι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a ba ⇔ b = a ⊓ bh: Codisjoint a bh.himp_eq_right: ∀ {α : Type ?u.45022} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → b ⇨ a = ahimp_eq_rightι: Type ?u.44592α: Type u_1β: Type ?u.44598π: ι → Type ?u.44603inst✝: GeneralizedHeytingAlgebra αa✝, b✝, c, d, a, b: αh: Codisjoint a ba ⊓ b = a ⊓ b]Goals accomplished! 🐙
#align codisjoint.bihimp_eq_inf Codisjoint.bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇔ b = a ⊓ bCodisjoint.bihimp_eq_inf

theorem himp_bihimp: a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_bihimp : a: αa ⇨ b: αb ⇔ c: αc = (a: αa ⊓ c: αc ⇨ b: αb) ⊓ (a: αa ⊓ b: αb ⇨ c: αc) := byGoals accomplished! 🐙
ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)rw [ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)bihimp: {α : Type ?u.45347} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp,ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ (c ⇨ b) ⊓ (b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_inf_distrib: ∀ {α : Type ?u.45348} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)himp_inf_distrib,ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α(a ⇨ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_himp: ∀ {α : Type ?u.45387} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = a ⊓ b ⇨ chimp_himp,ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α(a ⊓ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) ι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_himp: ∀ {α : Type ?u.45416} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = a ⊓ b ⇨ chimp_himpι: Type ?u.45050α: Type u_1β: Type ?u.45056π: ι → Type ?u.45061inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α(a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)]Goals accomplished! 🐙
#align himp_bihimp himp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_bihimp

@[simp]
theorem sup_himp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ a ⇔ b = a ⇔ bsup_himp_bihimp : a: αa ⊔ b: αb ⇨ a: αa ⇔ b: αb = a: αa ⇔ b: αb := byGoals accomplished! 🐙
ι: Type ?u.45477α: Type u_1β: Type ?u.45483π: ι → Type ?u.45488inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⊔ b ⇨ a ⇔ b = a ⇔ brw [ι: Type ?u.45477α: Type u_1β: Type ?u.45483π: ι → Type ?u.45488inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⊔ b ⇨ a ⇔ b = a ⇔ bhimp_bihimp: ∀ {α : Type ?u.45646} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_bihimpι: Type ?u.45477α: Type u_1β: Type ?u.45483π: ι → Type ?u.45488inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b]ι: Type ?u.45477α: Type u_1β: Type ?u.45483π: ι → Type ?u.45488inst✝: GeneralizedHeytingAlgebra αa, b, c, d: α((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
ι: Type ?u.45477α: Type u_1β: Type ?u.45483π: ι → Type ?u.45488inst✝: GeneralizedHeytingAlgebra αa, b, c, d: αa ⊔ b ⇨ a ⇔ b = a ⇔ bsimp [bihimp: {α : Type ?u.45706} → [inst : Inf α] → [inst : HImp α] → α → α → αbihimp]Goals accomplished! 🐙
#align sup_himp_bihimp sup_himp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ a ⇔ b = a ⇔ bsup_himp_bihimp

@[simp]
theorem bihimp_himp_eq_inf: a ⇔ (a ⇨ b) = a ⊓ bbihimp_himp_eq_inf : a: αa ⇔ (a: αa ⇨ b: αb) = a: αa ⊓ b: αb :=
@symmDiff_sdiff_eq_sup: ∀ {α : Type ?u.51996} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ bsymmDiff_sdiff_eq_sup α: Type ?u.51895αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align bihimp_himp_eq_inf bihimp_himp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ (a ⇨ b) = a ⊓ bbihimp_himp_eq_inf

@[simp]
theorem himp_bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (b ⇨ a) ⇔ b = a ⊓ bhimp_bihimp_eq_inf : (b: αb ⇨ a: αa) ⇔ b: αb = a: αa ⊓ b: αb :=
@sdiff_symmDiff_eq_sup: ∀ {α : Type ?u.52159} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ bsdiff_symmDiff_eq_sup α: Type ?u.52058αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align himp_bihimp_eq_inf himp_bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (b ⇨ a) ⇔ b = a ⊓ bhimp_bihimp_eq_inf

@[simp]
theorem bihimp_inf_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⊓ (a ⊔ b) = a ⊓ bbihimp_inf_sup : a: αa ⇔ b: αb ⊓ (a: αa ⊔ b: αb) = a: αa ⊓ b: αb :=
@symmDiff_sup_inf: ∀ {α : Type ?u.52385} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ bsymmDiff_sup_inf α: Type ?u.52221αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align bihimp_inf_sup bihimp_inf_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⊓ (a ⊔ b) = a ⊓ bbihimp_inf_sup

@[simp]
theorem sup_inf_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⊓ a ⇔ b = a ⊓ bsup_inf_bihimp : (a: αa ⊔ b: αb) ⊓ a: αa ⇔ b: αb = a: αa ⊓ b: αb :=
@inf_sup_symmDiff: ∀ {α : Type ?u.52615} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ a ∆ b = a ⊔ binf_sup_symmDiff α: Type ?u.52451αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align sup_inf_bihimp sup_inf_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⊓ a ⇔ b = a ⊓ bsup_inf_bihimp

@[simp]
theorem bihimp_bihimp_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⇔ (a ⊔ b) = a ⊓ bbihimp_bihimp_sup : a: αa ⇔ b: αb ⇔ (a: αa ⊔ b: αb) = a: αa ⊓ b: αb :=
@symmDiff_symmDiff_inf: ∀ {α : Type ?u.52848} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ bsymmDiff_symmDiff_inf α: Type ?u.52683αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align bihimp_bihimp_sup bihimp_bihimp_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⇔ (a ⊔ b) = a ⊓ bbihimp_bihimp_sup

@[simp]
theorem sup_bihimp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ bsup_bihimp_bihimp : (a: αa ⊔ b: αb) ⇔ (a: αa ⇔ b: αb) = a: αa ⊓ b: αb :=
@inf_symmDiff_symmDiff: ∀ {α : Type ?u.53081} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a ⊓ b) ∆ (a ∆ b) = a ⊔ binf_symmDiff_symmDiff α: Type ?u.52916αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_
#align sup_bihimp_bihimp sup_bihimp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ bsup_bihimp_bihimp

theorem bihimp_triangle: a ⇔ b ⊓ b ⇔ c ≤ a ⇔ cbihimp_triangle : a: αa ⇔ b: αb ⊓ b: αb ⇔ c: αc ≤ a: αa ⇔ c: αc :=
@symmDiff_triangle: ∀ {α : Type ?u.53339} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ c ≤ a ∆ b ⊔ b ∆ csymmDiff_triangle α: Type ?u.53147αᵒᵈ _ _: αᵒᵈ_ _: αᵒᵈ_ _: αᵒᵈ_
#align bihimp_triangle bihimp_triangle: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇔ b ⊓ b ⇔ c ≤ a ⇔ cbihimp_triangle

end GeneralizedHeytingAlgebra

section CoheytingAlgebra

variable [CoheytingAlgebra: Type ?u.54510 → Type ?u.54510CoheytingAlgebra α: Type ?u.53410α] (a: αa : α: Type ?u.53391α)

@[simp]
theorem symmDiff_top': ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), a ∆ ⊤ = ￢asymmDiff_top' : a: αa ∆ ⊤: ?m.53432⊤ = ￢a: αa := byGoals accomplished! 🐙 ι: Type ?u.53407α: Type u_1β: Type ?u.53413π: ι → Type ?u.53418inst✝: CoheytingAlgebra αa: αa ∆ ⊤ = ￢asimp [symmDiff: {α : Type ?u.53537} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff]Goals accomplished! 🐙
#align symm_diff_top' symmDiff_top': ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), a ∆ ⊤ = ￢asymmDiff_top'

@[simp]
theorem top_symmDiff': ⊤ ∆ a = ￢atop_symmDiff' : ⊤: ?m.54521⊤ ∆ a: αa = ￢a: αa := byGoals accomplished! 🐙 ι: Type ?u.54496α: Type u_1β: Type ?u.54502π: ι → Type ?u.54507inst✝: CoheytingAlgebra αa: α⊤ ∆ a = ￢asimp [symmDiff: {α : Type ?u.54638} → [inst : Sup α] → [inst : SDiff α] → α → α → αsymmDiff]Goals accomplished! 🐙
#align top_symm_diff' top_symmDiff': ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ⊤ ∆ a = ￢atop_symmDiff'

@[simp]
theorem hnot_symmDiff_self: (￢a) ∆ a = ⊤hnot_symmDiff_self : (￢a: <```