no goals
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
h : ￢a = ⊤
⊢ ∂ a = a
rw [boundary, h, inf_top_eq]
case intro
α : Type u_1
inst✝ : CoheytingAlgebra α
b✝ b : α
⊢ ￢∂ b = ⊤
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤
rintro ⟨b, rfl⟩
no goals
case intro
α : Type u_1
inst✝ : CoheytingAlgebra α
b✝ b : α
⊢ ￢∂ b = ⊤
exact hnot_boundary _