awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Heyting.Basic
Goal:
⊢ ⊤ = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
⊢ ⊥ = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
a b : PUnit
⊢ max a b = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
a b : PUnit
⊢ min a b = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
a : PUnit
⊢ aᶜ = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
a b : PUnit
⊢ a \ b = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
a : PUnit
⊢ ￢a = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
a b : PUnit
⊢ a ⇨ b = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ a ⊓ ￢a = ∂ a

Tactic:
rfl

Premises used: Coheyting.boundary, rfl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ∂ a ≤ a

Tactic:
inf_le_left

Premises used: Coheyting.boundary, inf_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ∂ a ≤ ￢a

Tactic:
inf_le_right

Premises used: inf_le_right, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
⊢ Eq.{u_1 + 1} (α := α) (∂ ⊥) ⊥

Tactic:
bot_inf_eq _

Premises used: Coheyting.boundary, bot_inf_eq
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ￢⊤) ⊥
rw₁ : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ⊥) ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := α) (∂ ⊤) ⊥

Tactic:
rw [boundary, hnot_top, inf_bot_eq]

Premises used: hnot_top, Coheyting.boundary, inf_bot_eq
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ∂ (￢a) ≤ ∂ a

Tactic:
(inf_comm _ _).trans_le <| inf_le_inf_right _ hnot_hnot_le

Premises used: hnot_hnot_le, Eq.trans_le, inf_le_inf_right, inf_comm, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
simp_rw : ￢￢a ⊓ ￢￢￢a = ￢a ⊓ ￢￢a
simp_rw₁ : ￢￢a ⊓ ￢a = ￢a ⊓ ￢￢a
⊢ ∂ (￢￢a) = ∂ (￢a)

Tactic:
simp_rw [boundary, hnot_hnot_hnot, inf_comm]

Premises used: inf_comm, Coheyting.boundary, hnot_hnot_hnot
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢(a ⊓ ￢a) = ⊤
rw₁ : ￢a ⊔ ￢￢a = ⊤
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ ￢∂ a = ⊤

Tactic:
rw [boundary, hnot_inf_distrib, sup_hnot_self]

Premises used: sup_hnot_self, hnot_inf_distrib, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
unfold : a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
⊢ ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b

Tactic:
unfold boundary

Premises used: Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
rw : a ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
rw₁ : a ⊓ b ⊓ ￢a ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
rw₂ : a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
rw₃ rw₄ : a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)

Tactic:
rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]

Premises used: hnot_inf_distrib, inf_sup_left, inf_right_comm, inf_assoc
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊓ b) ≤ ∂ a ⊔ ∂ b

Tactic:
(boundary_inf _ _).trans_le <| sup_le_sup inf_le_left inf_le_right

Premises used: sup_le_sup, inf_le_right, Eq.trans_le, Coheyting.boundary_inf, inf_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
rw : a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
⊢ ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b

Tactic:
rw [boundary, inf_sup_right]

Premises used: inf_sup_right, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b

Tactic:
sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left)
      (inf_le_inf_left _ <| hnot_anti le_sup_right)

Premises used: sup_le_sup, le_sup_left, inf_le_inf_left, le_sup_right, hnot_anti
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b

Tactic:
exact
    sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left)
      (inf_le_inf_left _ <| hnot_anti le_sup_right)

Premises used: sup_le_sup, le_sup_left, inf_le_inf_left, le_sup_right, hnot_anti
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha_1 : a
right : b
ha : a
⊢ a ∨ ¬a

Tactic:
Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha_1 : a
right : b
ha : a
⊢ a ∨ ¬a

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha_1 : a
right : b
ha : a
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha : a
right hb : b
⊢ a ∨ ¬a

Tactic:
Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha : a
right hb : b
⊢ a ∨ ¬a

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha : a
right hb : b
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha : a
right : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha : a
right : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
ha : a
right : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a

Tactic:
Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

Tactic:
Or.inl

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab_1 : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
Or.inl

Premises used: Or.inl
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

Tactic:
Or.inr fun ha => hnab ⟨ha, hb⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

Tactic:
exact Or.inr fun ha => hnab ⟨ha, hb⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab_1 : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
Or.inr fun ha => hnab <| Or.inl ha

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a_1 b_1 : α
a b : Prop
hnab_1 : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
exact Or.inr fun ha => hnab <| Or.inl ha

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
simp :
  ((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)
⊢ ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Tactic:
simp only [boundary, sup_inf_left, sup_inf_right, sup_right_idem, le_inf_iff, sup_assoc,
    sup_comm _ a]

Premises used: sup_inf_right, sup_right_idem, sup_inf_left, sup_assoc, le_inf_iff, sup_comm, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
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)

Tactic:
⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
refine_2 : a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
refine_3 : a ⊓ ￢a ≤ a ⊔ b
refine_4 : a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
refine_5 : a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
refine_6 : a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(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)

Tactic:
refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

Tactic:
le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left, inf_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

Tactic:
exact le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

Tactic:
{ exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

Tactic:
try { exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)

Tactic:
le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left, inf_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)

Tactic:
exact le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)

Tactic:
{ exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)

Tactic:
try { exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

Tactic:
le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left, inf_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

Tactic:
exact le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

Tactic:
{ exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

Tactic:
try { exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

Tactic:
le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left, inf_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

Tactic:
exact le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

Tactic:
{ exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

Tactic:
try { exact le_sup_of_le_left inf_le_left }

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
le_sup_of_le_left inf_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
inf_le_of_right_le ?_

Premises used: inf_le_of_right_le
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_4 : ￢a ≤ ￢(a ⊔ b) ⊔ b
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
refine inf_le_of_right_le ?_

Premises used: inf_le_of_right_le
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
inf_le_of_right_le ?_

Premises used: inf_le_of_right_le
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_6 : ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine inf_le_of_right_le ?_

Premises used: inf_le_of_right_le
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_4 : Codisjoint (￢(a ⊔ b)) (a ⊔ b)
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]

Premises used: codisjoint_left_comm, hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)

Tactic:
codisjoint_hnot_left

Premises used: codisjoint_hnot_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)

Tactic:
exact codisjoint_hnot_left

Premises used: codisjoint_hnot_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
le_sup_of_le_right ?_

Premises used: le_sup_of_le_right
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_6 : ￢a ≤ ￢(a ⊓ b)
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine le_sup_of_le_right ?_

Premises used: le_sup_of_le_right
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_6 : Codisjoint a (￢(a ⊓ b))
⊢ ￢a ≤ ￢(a ⊓ b)

Tactic:
rw [hnot_le_iff_codisjoint_right]

Premises used: hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))

Tactic:
codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)

Premises used: codisjoint_hnot_right, Codisjoint.mono_right, inf_le_left, hnot_anti
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))

Tactic:
exact codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)

Premises used: codisjoint_hnot_right, Codisjoint.mono_right, inf_le_left, hnot_anti
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
rw : ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Tactic:
rw [sup_comm a, inf_comm]

Premises used: inf_comm, sup_comm
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)

Tactic:
boundary_le_boundary_sup_sup_boundary_inf_left

Premises used: Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)

Tactic:
exact boundary_le_boundary_sup_sup_boundary_inf_left

Premises used: Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) = ∂ a ⊔ ∂ b

Tactic:
le_antisymm (sup_le boundary_sup_le boundary_inf_le) <|
    sup_le boundary_le_boundary_sup_sup_boundary_inf_left
      boundary_le_boundary_sup_sup_boundary_inf_right

Premises used: Coheyting.boundary_sup_le, Coheyting.boundary_inf_le, Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left, le_antisymm, sup_le, Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ∂ a ⊓ ￢∂ a = ∂ a
rw₁ : ∂ a ⊓ ⊤ = ∂ a
rw₂ rw₃ : ∂ a = ∂ a
⊢ ∂ ∂ a = ∂ a

Tactic:
rw [boundary, hnot_boundary, inf_top_eq]

Premises used: Coheyting.hnot_boundary, inf_top_eq, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a ≤ a
⊢ ￢￢a ⊔ ∂ a = a

Tactic:
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]

Premises used: inf_top_eq, sup_inf_left, Coheyting.boundary, sup_eq_right, hnot_sup_self
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Tactic:
hnot_hnot_le

Premises used: hnot_hnot_le
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Tactic:
exact hnot_hnot_le

Premises used: hnot_hnot_le
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
⊢ a \ ∂ a = ￢￢a

Tactic:
rw (occs := [1]) [← hnot_hnot_sup_boundary a]

Premises used: Coheyting.hnot_hnot_sup_boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
rw₁ : ￢￢a \ ∂ a ⊔ ⊥ = ￢￢a
rw₂ : ￢￢a \ ∂ a = ￢￢a
rw₃ : ￢∂ a \ ￢a = ￢￢a
rw₄ : ⊤ \ ￢a = ￢￢a
rw₅ rw₆ : ￢￢a = ￢￢a
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a

Tactic:
rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']

Premises used: Coheyting.hnot_boundary, sdiff_self, hnot_sdiff_comm, sup_bot_eq, sup_sdiff_distrib, top_sdiff'
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
h : ￢a = ⊤
rw : a ⊓ ￢a = a
rw₁ : a ⊓ ⊤ = a
rw₂ rw₃ : a = a
⊢ ∂ a = a

Tactic:
rw [boundary, h, inf_top_eq]

Premises used: inf_top_eq, Coheyting.boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
b : α
⊢ ￢∂ b = ⊤

Tactic:
hnot_boundary _

Premises used: Coheyting.hnot_boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : CoheytingAlgebra α
b : α
⊢ ￢∂ b = ⊤

Tactic:
exact hnot_boundary _

Premises used: Coheyting.hnot_boundary
-- Module: Mathlib.Order.Heyting.Boundary
Goal:
α : Type u_1
inst : BooleanAlgebra α
a : α
⊢ ∂ a = ⊥

Tactic:
inf_compl_eq_bot

Premises used: Coheyting.boundary, inf_compl_eq_bot
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
x : HeytingAlgebra β
inst_2 : HeytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₂ : β
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₄ : β
rw₅ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₆ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]

Premises used: HeytingHomClass.map_himp, himp_self