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: Yaël Dillies

! This file was ported from Lean 3 source module order.heyting.boundary
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.BooleanAlgebra

/-!
# Co-Heyting boundary

The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation with
itself. The boundary in the co-Heyting algebra of closed sets coincides with the topological
boundary.

## Main declarations

* `Coheyting.boundary`: Co-Heyting boundary. `Coheyting.boundary a = a ⊓ ￢a`

## Notation

`∂ a` is notation for `Coheyting.boundary a` in locale `Heyting`.
-/

variable {α: Type ?u.5α : Type _: Type (?u.2+1)Type _}

namespace Coheyting

variable [CoheytingAlgebra: Type ?u.8964 → Type ?u.8964CoheytingAlgebra α: Type ?u.8559α] {a: αa b: αb : α: Type ?u.9794α}

/-- The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation
with itself. Note that this is always `⊥` for a boolean algebra. -/
def boundary: α → αboundary (a: αa : α: Type ?u.15α) : α: Type ?u.15α :=
a: αa ⊓ ￢a: αa
#align coheyting.boundary Coheyting.boundary: {α : Type u_1} → [inst : CoheytingAlgebra α] → α → αCoheyting.boundary

/-- The boundary of an element of a co-Heyting algebra. -/
scoped[Heyting] prefix:120 "∂ " => Coheyting.boundary: {α : Type u_1} → [inst : CoheytingAlgebra α] → α → αCoheyting.boundary
-- Porting note: Should the notation be automatically included in the current scope?
open Heyting

-- Porting note: Should hnot be named hNot?
theorem inf_hnot_self: ∀ (a : α), a ⊓ ￢a = ∂ ainf_hnot_self (a: αa : α: Type ?u.7905α) : a: αa ⊓ ￢a: αa = ∂ a: αa :=
rfl: ∀ {α : Sort ?u.7984} {a : α}, a = arfl
#align coheyting.inf_hnot_self Coheyting.inf_hnot_self: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), a ⊓ ￢a = ∂ aCoheyting.inf_hnot_self

theorem boundary_le: ∂ a ≤ aboundary_le : ∂ a: αa ≤ a: αa :=
inf_le_left: ∀ {α : Type ?u.8054} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_left
#align coheyting.boundary_le Coheyting.boundary_le: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, ∂ a ≤ aCoheyting.boundary_le

theorem boundary_le_hnot: ∂ a ≤ ￢aboundary_le_hnot : ∂ a: αa ≤ ￢a: αa :=
inf_le_right: ∀ {α : Type ?u.8194} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ binf_le_right
#align coheyting.boundary_le_hnot Coheyting.boundary_le_hnot: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, ∂ a ≤ ￢aCoheyting.boundary_le_hnot

@[simp]
theorem boundary_bot: ∀ {α : Type u_1} [inst : CoheytingAlgebra α], ∂ ⊥ = ⊥boundary_bot : ∂ (⊥: ?m.8272⊥ : α: Type ?u.8256α) = ⊥: ?m.8335⊥ :=
bot_inf_eq: ∀ {α : Type ?u.8372} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a : α}, ⊥ ⊓ a = ⊥bot_inf_eq
#align coheyting.boundary_bot Coheyting.boundary_bot: ∀ {α : Type u_1} [inst : CoheytingAlgebra α], ∂ ⊥ = ⊥Coheyting.boundary_bot

@[simp]
theorem boundary_top: ∂ ⊤ = ⊥boundary_top : ∂ (⊤: ?m.8575⊤ : α: Type ?u.8559α) = ⊥: ?m.8608⊥ := byGoals accomplished! 🐙 α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ ⊤ = ⊥rw [α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ ⊤ = ⊥boundary: {α : Type ?u.8719} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa, b: α⊤ ⊓ ￢⊤ = ⊥ α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ ⊤ = ⊥hnot_top: ∀ {α : Type ?u.8720} [inst : CoheytingAlgebra α], ￢⊤ = ⊥hnot_top,α: Type u_1inst✝: CoheytingAlgebra αa, b: α⊤ ⊓ ⊥ = ⊥ α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ ⊤ = ⊥inf_bot_eq: ∀ {α : Type ?u.8748} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a : α}, a ⊓ ⊥ = ⊥inf_bot_eqα: Type u_1inst✝: CoheytingAlgebra αa, b: α⊥ = ⊥]Goals accomplished! 🐙
#align coheyting.boundary_top Coheyting.boundary_top: ∀ {α : Type u_1} [inst : CoheytingAlgebra α], ∂ ⊤ = ⊥Coheyting.boundary_top

theorem boundary_hnot_le: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ∂ (￢a) ≤ ∂ aboundary_hnot_le (a: αa : α: Type ?u.8961α) : ∂ (￢a: αa) ≤ ∂ a: αa :=
inf_comm: ∀ {α : Type ?u.9058} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ⊓ ainf_comm.trans_le: ∀ {α : Type ?u.9075} [inst : Preorder α] {a b c : α}, a = b → b ≤ c → a ≤ ctrans_le <| inf_le_inf_right: ∀ {α : Type ?u.9162} [inst : SemilatticeInf α] (a : α) {b c : α}, b ≤ c → b ⊓ a ≤ c ⊓ ainf_le_inf_right _: ?m.9163_ hnot_hnot_le: ∀ {α : Type ?u.9186} [inst : CoheytingAlgebra α] {a : α}, ￢￢a ≤ ahnot_hnot_le
#align coheyting.boundary_hnot_le Coheyting.boundary_hnot_le: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ∂ (￢a) ≤ ∂ aCoheyting.boundary_hnot_le

@[simp]
theorem boundary_hnot_hnot: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ∂ (￢￢a) = ∂ (￢a)boundary_hnot_hnot (a: αa : α: Type ?u.9221α) : ∂ (￢￢a: αa) = ∂ (￢a: αa) := byGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ (￢￢a) = ∂ (￢a)simp_rw [α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ (￢￢a) = ∂ (￢a)boundary: {α : Type ?u.9366} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊓ ￢￢￢a = ￢a ⊓ ￢￢a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ (￢￢a) = ∂ (￢a)hnot_hnot_hnot: ∀ {α : Type ?u.9440} [inst : CoheytingAlgebra α] (a : α), ￢￢￢a = ￢ahnot_hnot_hnot,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊓ ￢a = ￢a ⊓ ￢￢a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ (￢￢a) = ∂ (￢a)inf_comm: ∀ {α : Type ?u.9478} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ⊓ ainf_commGoals accomplished! 🐙]Goals accomplished! 🐙
#align coheyting.boundary_hnot_hnot Coheyting.boundary_hnot_hnot: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ∂ (￢￢a) = ∂ (￢a)Coheyting.boundary_hnot_hnot

@[simp]
theorem hnot_boundary: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ￢∂ a = ⊤hnot_boundary (a: αa : α: Type ?u.9580α) : ￢∂ a: αa = ⊤: ?m.9628⊤ := byGoals accomplished! 🐙 α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢∂ a = ⊤rw [α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢∂ a = ⊤boundary: {α : Type ?u.9701} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢(a ⊓ ￢a) = ⊤ α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢∂ a = ⊤hnot_inf_distrib: ∀ {α : Type ?u.9702} [inst : CoheytingAlgebra α] (a b : α), ￢(a ⊓ b) = ￢a ⊔ ￢bhnot_inf_distrib,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢a ⊔ ￢￢a = ⊤ α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢∂ a = ⊤sup_hnot_self: ∀ {α : Type ?u.9736} [inst : CoheytingAlgebra α] (a : α), a ⊔ ￢a = ⊤sup_hnot_selfα: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α⊤ = ⊤]Goals accomplished! 🐙
#align coheyting.hnot_boundary Coheyting.hnot_boundary: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ￢∂ a = ⊤Coheyting.hnot_boundary

/-- **Leibniz rule** for the co-Heyting boundary. -/
theorem boundary_inf: ∀ (a b : α), ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ bboundary_inf (a: αa b: αb : α: Type ?u.9794α) : ∂ (a: αa ⊓ b: αb) = ∂ a: αa ⊓ b: αb ⊔ a: αa ⊓ ∂ b: αb := byGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: α∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ bunfold boundary: {α : Type u_1} → [inst : CoheytingAlgebra α] → α → αboundaryα: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: α∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ brw [α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)hnot_inf_distrib: ∀ {α : Type ?u.9944} [inst : CoheytingAlgebra α] (a b : α), ￢(a ⊓ b) = ￢a ⊔ ￢bhnot_inf_distrib,α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b) α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)inf_sup_left: ∀ {α : Type ?u.9980} [inst : DistribLattice α] {x y z : α}, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ zinf_sup_left,α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ ￢a ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b) α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)inf_right_comm: ∀ {α : Type ?u.10052} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ c ⊓ binf_right_comm,α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b) α: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)← inf_assoc: ∀ {α : Type ?u.10109} [inst : SemilatticeInf α] {a b c : α}, a ⊓ b ⊓ c = a ⊓ (b ⊓ c)inf_assocα: Type u_1inst✝: CoheytingAlgebra αa✝, b✝, a, b: αa ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b]Goals accomplished! 🐙
#align coheyting.boundary_inf Coheyting.boundary_inf: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a b : α), ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ bCoheyting.boundary_inf

theorem boundary_inf_le: ∂ (a ⊓ b) ≤ ∂ a ⊔ ∂ bboundary_inf_le : ∂ (a: αa ⊓ b: αb) ≤ ∂ a: αa ⊔ ∂ b: αb :=
(boundary_inf: ∀ {α : Type ?u.10438} [inst : CoheytingAlgebra α] (a b : α), ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ bboundary_inf _: ?m.10439_ _: ?m.10439_).trans_le: ∀ {α : Type ?u.10451} [inst : Preorder α] {a b c : α}, a = b → b ≤ c → a ≤ ctrans_le <| sup_le_sup: ∀ {α : Type ?u.10526} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ dsup_le_sup inf_le_left: ∀ {α : Type ?u.10571} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_left inf_le_right: ∀ {α : Type ?u.10613} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ binf_le_right
#align coheyting.boundary_inf_le Coheyting.boundary_inf_le: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α}, ∂ (a ⊓ b) ≤ ∂ a ⊔ ∂ bCoheyting.boundary_inf_le

theorem boundary_sup_le: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α}, ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ bboundary_sup_le : ∂ (a: αa ⊔ b: αb) ≤ ∂ a: αa ⊔ ∂ b: αb := byGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ brw [α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ bboundary: {α : Type ?u.10797} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa, b: α(a ⊔ b) ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ binf_sup_right: ∀ {α : Type ?u.10798} [inst : DistribLattice α] {x y z : α}, (y ⊔ z) ⊓ x = y ⊓ x ⊔ z ⊓ xinf_sup_rightα: Type u_1inst✝: CoheytingAlgebra αa, b: αa ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b]α: Type u_1inst✝: CoheytingAlgebra αa, b: αa ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ bexact
sup_le_sup: ∀ {α : Type ?u.10920} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ dsup_le_sup (inf_le_inf_left: ∀ {α : Type ?u.10973} [inst : SemilatticeInf α] (a : α) {b c : α}, b ≤ c → a ⊓ b ≤ a ⊓ cinf_le_inf_left _: ?m.10974_ <| hnot_anti: ∀ {α : Type ?u.11017} [inst : CoheytingAlgebra α], Antitone hnothnot_anti le_sup_left: ∀ {α : Type ?u.11039} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ ble_sup_left)
(inf_le_inf_left: ∀ {α : Type ?u.11072} [inst : SemilatticeInf α] (a : α) {b c : α}, b ≤ c → a ⊓ b ≤ a ⊓ cinf_le_inf_left _: ?m.11073_ <| hnot_anti: ∀ {α : Type ?u.11096} [inst : CoheytingAlgebra α], Antitone hnothnot_anti le_sup_right: ∀ {α : Type ?u.11115} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ ble_sup_right)Goals accomplished! 🐙
#align coheyting.boundary_sup_le Coheyting.boundary_sup_le: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α}, ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ bCoheyting.boundary_sup_le

/- The intuitionistic version of `Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left`. Either
proof can be obtained from the other using the equivalence of Heyting algebras and intuitionistic
logic and duality between Heyting and co-Heyting algebras. It is crucial that the following proof be
intuitionistic. -/
example: ∀ (a b : Prop), (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬aexample (a: Propa b: Propb : Prop: TypeProp) : (a: Propa ∧ b: Propb ∨ ¬(a: Propa ∧ b: Propb)) ∧ ((a: Propa ∨ b: Propb) ∨ ¬(a: Propa ∨ b: Propb)) → a: Propa ∨ ¬a: Propa := byGoals accomplished! 🐙
α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prop(a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬arintro ⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩: (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b))⟨⟨ha, _⟩: a ∧ b⟨ha: aha⟨ha, _⟩: a ∧ b, _: b_⟨ha, _⟩: a ∧ b⟩⟨ha, _⟩ | hnab: a ∧ b ∨ ¬(a ∧ b) | hnab: ¬(a ∧ b)hnab⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩: (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)), (ha | hb) | hnab: (a ∨ b) ∨ ¬(a ∨ b)(ha: ahaha | hb: a ∨ b | hb: bhb(ha | hb) | hnab: (a ∨ b) ∨ ¬(a ∨ b)) | hnab: ¬(a ∨ b)hnab⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩: (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b))⟩α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Propha✝: aright✝: bha: aintro.inl.intro.inl.inla ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Propha: aright✝, hb: bintro.inl.intro.inl.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Propha: aright✝: bhnab: ¬(a ∨ b)intro.inl.intro.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab: ¬(a ∧ b)ha: aintro.inr.inl.inla ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab: ¬(a ∧ b)hb: bintro.inr.inl.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab✝: ¬(a ∧ b)hnab: ¬(a ∨ b)intro.inr.inra ∨ ¬a α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prop(a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a<;>α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Propha✝: aright✝: bha: aintro.inl.intro.inl.inla ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Propha: aright✝, hb: bintro.inl.intro.inl.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Propha: aright✝: bhnab: ¬(a ∨ b)intro.inl.intro.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab: ¬(a ∧ b)ha: aintro.inr.inl.inla ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab: ¬(a ∧ b)hb: bintro.inr.inl.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab✝: ¬(a ∧ b)hnab: ¬(a ∨ b)intro.inr.inra ∨ ¬a α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prop(a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬atry α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab✝: ¬(a ∧ b)hnab: ¬(a ∨ b)intro.inr.inra ∨ ¬aexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ha: ahaGoals accomplished! 🐙
α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prop(a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a·α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab: ¬(a ∧ b)hb: bintro.inr.inl.inra ∨ ¬a α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab: ¬(a ∧ b)hb: bintro.inr.inl.inra ∨ ¬aα: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab✝: ¬(a ∧ b)hnab: ¬(a ∨ b)intro.inr.inra ∨ ¬aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr fun ha: ?m.11351ha => hnab: ¬(a ∧ b)hnab ⟨ha: ?m.11351ha, hb: bhb⟩Goals accomplished! 🐙
α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prop(a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a·α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab✝: ¬(a ∧ b)hnab: ¬(a ∨ b)intro.inr.inra ∨ ¬a α: Type ?u.11149inst✝: CoheytingAlgebra αa✝, b✝: αa, b: Prophnab✝: ¬(a ∧ b)hnab: ¬(a ∨ b)intro.inr.inra ∨ ¬aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr fun ha: ?m.11365ha => hnab: ¬(a ∨ b)hnab <| Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ha: ?m.11365haGoals accomplished! 🐙

theorem boundary_le_boundary_sup_sup_boundary_inf_left: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α}, ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)boundary_le_boundary_sup_sup_boundary_inf_left : ∂ a: αa ≤ ∂ (a: αa ⊔ b: αb) ⊔ ∂ (a: αa ⊓ b: αb) := byGoals accomplished! 🐙
-- Porting note: the following simp generates the same term as mathlib3 if you remove
-- sup_inf_right from both. With sup_inf_right included, mathlib4 and mathlib3 generate
-- different terms
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)simp only [boundary: {α : Type ?u.11562} → [inst : CoheytingAlgebra α] → α → αboundary, sup_inf_left: ∀ {α : Type ?u.11576} [inst : DistribLattice α] {x y z : α}, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)sup_inf_left, sup_inf_right: ∀ {α : Type ?u.11596} [inst : DistribLattice α] {x y z : α}, y ⊓ z ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)sup_inf_right, sup_right_idem: ∀ {α : Type ?u.11608} [inst : SemilatticeSup α] {a b : α}, a ⊔ b ⊔ b = a ⊔ bsup_right_idem, le_inf_iff: ∀ {α : Type ?u.11618} [inst : SemilatticeInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ cle_inf_iff, sup_assoc: ∀ {α : Type ?u.11645} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ⊔ c = a ⊔ (b ⊔ c)sup_assoc,
@sup_comm: ∀ {α : Type ?u.11662} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ asup_comm _: Type ?u.11662_ _ _: ?m.11663_ a: αa]α: Type u_1inst✝: CoheytingAlgebra αa, b: α((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧   a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)refine ⟨⟨⟨?_: ?m.12190?_, ?_: ?m.12191?_⟩, ⟨?_: ?m.12198?_, ?_: ?m.12199?_⟩⟩, ?_: ?m.12206?_, ?_: ?m.12207?_⟩α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_1a ⊓ ￢a ≤ a ⊔ (a ⊔ b)α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_2a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_3a ⊓ ￢a ≤ a ⊔ bα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ bα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_5a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b) α: Type u_1inst✝: CoheytingAlgebra αa, b: α((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧   a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)<;>α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_1a ⊓ ￢a ≤ a ⊔ (a ⊔ b)α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_2a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_3a ⊓ ￢a ≤ a ⊔ bα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ bα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_5a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b) α: Type u_1inst✝: CoheytingAlgebra αa, b: α((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧   a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)try α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_5a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)){α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)exact le_sup_of_le_left: ∀ {α : Type ?u.12322} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ ble_sup_of_le_left inf_le_left: ∀ {α : Type ?u.12299} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_leftα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b) }α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b) α: Type u_1inst✝: CoheytingAlgebra αa, b: α((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧   a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)<;>α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ bα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
α: Type u_1inst✝: CoheytingAlgebra αa, b: α((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧   a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)refine inf_le_of_right_le: ∀ {α : Type ?u.12865} [inst : SemilatticeInf α] {a b c : α}, b ≤ c → a ⊓ b ≤ cinf_le_of_right_le ?_: ?m.12844 ≤ ?m.12845?_α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)·α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4￢a ≤ ￢(a ⊔ b) ⊔ b α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4￢a ≤ ￢(a ⊔ b) ⊔ bα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)rw [α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4￢a ≤ ￢(a ⊔ b) ⊔ bhnot_le_iff_codisjoint_right: ∀ {α : Type ?u.12890} [inst : CoheytingAlgebra α] {a b : α}, ￢a ≤ b ↔ Codisjoint a bhnot_le_iff_codisjoint_right,α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4Codisjoint a (￢(a ⊔ b) ⊔ b) α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4￢a ≤ ￢(a ⊔ b) ⊔ bcodisjoint_left_comm: ∀ {α : Type ?u.12919} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)codisjoint_left_commα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4Codisjoint (￢(a ⊔ b)) (a ⊔ b)]α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4Codisjoint (￢(a ⊔ b)) (a ⊔ b)
α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_4￢a ≤ ￢(a ⊔ b) ⊔ bexact codisjoint_hnot_left: ∀ {α : Type ?u.13036} [inst : CoheytingAlgebra α] {a : α}, Codisjoint (￢a) acodisjoint_hnot_leftGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)·α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b) α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)refine le_sup_of_le_right: ∀ {α : Type ?u.13061} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ ble_sup_of_le_right ?_: ?m.13066 ≤ ?m.13065?_α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊓ b)
α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)rw [α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊓ b)hnot_le_iff_codisjoint_right: ∀ {α : Type ?u.13088} [inst : CoheytingAlgebra α] {a b : α}, ￢a ≤ b ↔ Codisjoint a bhnot_le_iff_codisjoint_rightα: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6Codisjoint a (￢(a ⊓ b))]α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6Codisjoint a (￢(a ⊓ b))
α: Type u_1inst✝: CoheytingAlgebra αa, b: αrefine_6￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)exact codisjoint_hnot_right: ∀ {α : Type ?u.13121} [inst : CoheytingAlgebra α] {a : α}, Codisjoint a (￢a)codisjoint_hnot_right.mono_right: ∀ {α : Type ?u.13133} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b c : α}, b ≤ c → Codisjoint a b → Codisjoint a cmono_right (hnot_anti: ∀ {α : Type ?u.13184} [inst : CoheytingAlgebra α], Antitone hnothnot_anti inf_le_left: ∀ {α : Type ?u.13203} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_left)Goals accomplished! 🐙
#align coheyting.boundary_le_boundary_sup_sup_boundary_inf_left Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α}, ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left

theorem boundary_le_boundary_sup_sup_boundary_inf_right: ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)boundary_le_boundary_sup_sup_boundary_inf_right : ∂ b: αb ≤ ∂ (a: αa ⊔ b: αb) ⊔ ∂ (a: αa ⊓ b: αb) := byGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)rw [α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)@sup_comm: ∀ {α : Type ?u.13483} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ asup_comm _: Type ?u.13483_ _ a: αa,α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (a ⊓ b) α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)inf_comm: ∀ {α : Type ?u.13521} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ⊓ ainf_commα: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)]α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
α: Type u_1inst✝: CoheytingAlgebra αa, b: α∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)exact boundary_le_boundary_sup_sup_boundary_inf_left: ∀ {α : Type ?u.13618} [inst : CoheytingAlgebra α] {a b : α}, ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)boundary_le_boundary_sup_sup_boundary_inf_leftGoals accomplished! 🐙
#align coheyting.boundary_le_boundary_sup_sup_boundary_inf_right Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a b : α}, ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right

theorem boundary_sup_sup_boundary_inf: ∀ (a b : α), ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) = ∂ a ⊔ ∂ bboundary_sup_sup_boundary_inf (a: αa b: αb : α: Type ?u.13665α) : ∂ (a: αa ⊔ b: αb) ⊔ ∂ (a: αa ⊓ b: αb) = ∂ a: αa ⊔ ∂ b: αb :=
le_antisymm: ∀ {α : Type ?u.13814} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm (sup_le: ∀ {α : Type ?u.13837} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le boundary_sup_le: ∀ {α : Type ?u.13915} [inst : CoheytingAlgebra α] {a b : α}, ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ bboundary_sup_le boundary_inf_le: ∀ {α : Type ?u.13941} [inst : CoheytingAlgebra α] {a b : α}, ∂ (a ⊓ b) ≤ ∂ a ⊔ ∂ bboundary_inf_le) <|
sup_le: ∀ {α : Type ?u.13966} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ csup_le boundary_le_boundary_sup_sup_boundary_inf_left: ∀ {α : Type ?u.13990} [inst : CoheytingAlgebra α] {a b : α}, ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)boundary_le_boundary_sup_sup_boundary_inf_left
boundary_le_boundary_sup_sup_boundary_inf_right: ∀ {α : Type ?u.14009} [inst : CoheytingAlgebra α] {a b : α}, ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)boundary_le_boundary_sup_sup_boundary_inf_right
#align coheyting.boundary_sup_sup_boundary_inf Coheyting.boundary_sup_sup_boundary_inf: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a b : α), ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) = ∂ a ⊔ ∂ bCoheyting.boundary_sup_sup_boundary_inf

@[simp]
theorem boundary_idem: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ∂ ∂ a = ∂ aboundary_idem (a: αa : α: Type ?u.14033α) : ∂ ∂ a: αa = ∂ a: αa := byGoals accomplished! 🐙 α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ ∂ a = ∂ arw [α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ ∂ a = ∂ aboundary: {α : Type ?u.14101} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ a ⊓ ￢∂ a = ∂ a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ ∂ a = ∂ ahnot_boundary: ∀ {α : Type ?u.14102} [inst : CoheytingAlgebra α] (a : α), ￢∂ a = ⊤hnot_boundary,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ a ⊓ ⊤ = ∂ a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ ∂ a = ∂ ainf_top_eq: ∀ {α : Type ?u.14130} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = ainf_top_eqα: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α∂ a = ∂ a]Goals accomplished! 🐙
#align coheyting.boundary_idem Coheyting.boundary_idem: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ∂ ∂ a = ∂ aCoheyting.boundary_idem

theorem hnot_hnot_sup_boundary: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ￢￢a ⊔ ∂ a = ahnot_hnot_sup_boundary (a: αa : α: Type ?u.14338α) : ￢￢a: αa ⊔ ∂ a: αa = a: αa := byGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = arw [α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = aboundary: {α : Type ?u.14475} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ a ⊓ ￢a = a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = asup_inf_left: ∀ {α : Type ?u.14476} [inst : DistribLattice α] {x y z : α}, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)sup_inf_left,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α(￢￢a ⊔ a) ⊓ (￢￢a ⊔ ￢a) = a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = ahnot_sup_self: ∀ {α : Type ?u.14553} [inst : CoheytingAlgebra α] (a : α), ￢a ⊔ a = ⊤hnot_sup_self,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α(￢￢a ⊔ a) ⊓ ⊤ = a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = ainf_top_eq: ∀ {α : Type ?u.14601} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = ainf_top_eq,α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ a = a α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = asup_eq_right: ∀ {α : Type ?u.14784} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ↔ a ≤ bsup_eq_rightα: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ≤ a]α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ≤ a
α: Type u_1inst✝: CoheytingAlgebra αa✝, b, a: α￢￢a ⊔ ∂ a = aexact hnot_hnot_le: ∀ {α : Type ?u.14877} [inst : CoheytingAlgebra α] {a : α}, ￢￢a ≤ ahnot_hnot_leGoals accomplished! 🐙
#align coheyting.hnot_hnot_sup_boundary Coheyting.hnot_hnot_sup_boundary: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ￢￢a ⊔ ∂ a = aCoheyting.hnot_hnot_sup_boundary

theorem hnot_eq_top_iff_exists_boundary: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, ￢a = ⊤ ↔ ∃ b, ∂ b = ahnot_eq_top_iff_exists_boundary : ￢a: αa = ⊤: ?m.14948⊤ ↔ ∃ b: ?m.14991b, ∂ b: ?m.14991b = a: αa :=
⟨fun h: ?m.15034h => ⟨a: αa, byGoals accomplished! 🐙 α: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤∂ a = arw [α: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤∂ a = aboundary: {α : Type ?u.15082} → [inst : CoheytingAlgebra α] → α → αboundary,α: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤a ⊓ ￢a = a α: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤∂ a = ah: ￢a = ⊤h,α: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤a ⊓ ⊤ = a α: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤∂ a = ainf_top_eq: ∀ {α : Type ?u.15086} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = ainf_top_eqα: Type u_1inst✝: CoheytingAlgebra αa, b: αh: ￢a = ⊤a = a]Goals accomplished! 🐙⟩, byGoals accomplished! 🐙
α: Type u_1inst✝: CoheytingAlgebra αa, b: α(∃ b, ∂ b = a) → ￢a = ⊤rintro ⟨b, rfl⟩: ∃ b, ∂ b = a⟨b: αb⟨b, rfl⟩: ∃ b, ∂ b = a, rfl: ∂ b = arfl⟨b, rfl⟩: ∃ b, ∂ b = a⟩α: Type u_1inst✝: CoheytingAlgebra αb✝, b: αintro￢∂ b = ⊤
α: Type u_1inst✝: CoheytingAlgebra αa, b: α(∃ b, ∂ b = a) → ￢a = ⊤exact hnot_boundary: ∀ {α : Type ?u.15314} [inst : CoheytingAlgebra α] (a : α), ￢∂ a = ⊤hnot_boundary _: ?m.15315_Goals accomplished! 🐙⟩
#align coheyting.hnot_eq_top_iff_exists_boundary Coheyting.hnot_eq_top_iff_exists_boundary: ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, ￢a = ⊤ ↔ ∃ b, ∂ b = aCoheyting.hnot_eq_top_iff_exists_boundary

end Coheyting

open Heyting

section BooleanAlgebra

variable [BooleanAlgebra: Type ?u.15360 → Type ?u.15360BooleanAlgebra α: Type ?u.15351α]

@[simp]
theorem Coheyting.boundary_eq_bot: ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a : α), ∂ a = ⊥Coheyting.boundary_eq_bot (a: αa : α: Type ?u.15357α) : ∂ a: αa = ⊥: ?m.15384⊥ :=
inf_compl_eq_bot: ∀ {α : Type ?u.15432} [inst : HeytingAlgebra α] {a : α}, a ⊓ aᶜ = ⊥inf_compl_eq_bot
#align coheyting.boundary_eq_bot Coheyting.boundary_eq_bot: ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a : α), ∂ a = ⊥Coheyting.boundary_eq_bot

end BooleanAlgebra
```