[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ ⊤ = ⊥
[PROOFSTEP]
rw [boundary, hnot_top, inf_bot_eq]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ∂ (￢￢a) = ∂ (￢a)
[PROOFSTEP]
simp_rw [boundary, hnot_hnot_hnot, inf_comm]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢∂ a = ⊤
[PROOFSTEP]
rw [boundary, hnot_inf_distrib, sup_hnot_self]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ a b : α
⊢ ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b
[PROOFSTEP]
unfold boundary
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ a b : α
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
[PROOFSTEP]
rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b
[PROOFSTEP]
rw [boundary, inf_sup_right]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
[PROOFSTEP]
exact sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left) (inf_le_inf_left _ <| hnot_anti le_sup_right)
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
⊢ (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a
[PROOFSTEP]
rintro ⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩
[GOAL]
case intro.inl.intro.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inl.intro.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inl.intro.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inl.intro.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inl.intro.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inl.intro.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inr.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inr fun ha => hnab ⟨ha, hb⟩
[GOAL]
case intro.inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inr fun ha => hnab <| Or.inl ha
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
[PROOFSTEP]
simp only [boundary, sup_inf_left, sup_inf_right, sup_right_idem, le_inf_iff, sup_assoc, @sup_comm _ _ _ a]
[GOAL]
α : Type u_1
inst✝ : 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)
[PROOFSTEP]
refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
[GOAL]
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
refine inf_le_of_right_le ?_
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
refine inf_le_of_right_le ?_
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)
[PROOFSTEP]
exact codisjoint_hnot_left
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
refine le_sup_of_le_right ?_
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊓ b)
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_right]
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))
[PROOFSTEP]
exact codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
[PROOFSTEP]
rw [@sup_comm _ _ a, inf_comm]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
[PROOFSTEP]
exact boundary_le_boundary_sup_sup_boundary_inf_left
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ∂ ∂ a = ∂ a
[PROOFSTEP]
rw [boundary, hnot_boundary, inf_top_eq]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ⊔ ∂ a = a
[PROOFSTEP]
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ≤ a
[PROOFSTEP]
exact hnot_hnot_le
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
h : ￢a = ⊤
⊢ ∂ a = a
[PROOFSTEP]
rw [boundary, h, inf_top_eq]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤
[PROOFSTEP]
rintro ⟨b, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CoheytingAlgebra α
b✝ b : α
⊢ ￢∂ b = ⊤
[PROOFSTEP]
exact hnot_boundary _
