awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ

Tactic:
compl_anti (compl_anti himp_inf_le)

Premises used: himp_inf_le, compl_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ

Tactic:
exact compl_anti (compl_anti himp_inf_le)

Premises used: himp_inf_le, compl_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ

Tactic:
le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)

Premises used: compl_anti, compl_sup_le_himp, Iff.mp, le_compl_comm, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
a₁ : (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ
⊢ aᶜᶜ ⇨ bᶜᶜ ≤ (a ⇨ b)ᶜᶜ

Tactic:
refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)

Premises used: compl_anti, compl_sup_le_himp, Iff.mp, le_compl_comm, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
a₁ : aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ
⊢ (aᶜ ⊔ b)ᶜ ≤ (aᶜᶜ ⇨ bᶜᶜ)ᶜ

Tactic:
rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
      le_compl_iff_disjoint_right]

Premises used: disjoint_right_comm, compl_sup_distrib, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ

Tactic:
inf_himp_le

Premises used: inf_himp_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ (aᶜᶜ ⇨ bᶜᶜ) ≤ bᶜᶜ

Tactic:
exact inf_himp_le

Premises used: inf_himp_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
rw : (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b

Tactic:
le_himp_iff

Premises used: le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) b ⇨ (ofDual : (a : αᵒᵈ) → α) a : α) ≤ c ↔ a ≤ c ⊔ b

Tactic:
exact le_himp_iff

Premises used: le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (￢a) : α) (((ofDual : (a : αᵒᵈ) → α) a)ᶜ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) aᶜ : αᵒᵈ) (￢(toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ⊤ \ a = ￢a

Tactic:
CoheytingAlgebra.top_sdiff _

Premises used: CoheytingAlgebra.top_sdiff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ a \ ⊤ = ⊥

Tactic:
sdiff_eq_bot_iff.2 le_top

Premises used: Iff.mpr, sdiff_eq_bot_iff, le_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
simp_rw : ⊤ \ (a ⊓ b) = ⊤ \ a ⊔ ⊤ \ b
⊢ ￢(a ⊓ b) = ￢a ⊔ ￢b

Tactic:
simp_rw [← top_sdiff', sdiff_inf_distrib]

Premises used: sdiff_inf_distrib, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ a \ b ≤ ￢b

Tactic:
(sdiff_le_sdiff_right le_top).trans_eq <| top_sdiff' _

Premises used: LE.le.trans_eq, sdiff_le_sdiff_right, le_top, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ a \ b ≤ a ⊓ ￢b

Tactic:
le_inf sdiff_le sdiff_le_hnot

Premises used: sdiff_le_hnot, le_inf, sdiff_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 a b c : α
simp_rw : (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]

Premises used: le_inf_iff, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : (⊤ \ a) \ a = ⊤ \ a
rw₁ : ⊤ \ (a ⊔ a) = ⊤ \ a
rw₂ rw₃ : ⊤ \ a = ⊤ \ a
⊢ ￢a \ a = ￢a

Tactic:
rw [← top_sdiff', sdiff_sdiff, sup_idem]

Premises used: sup_idem, sdiff_sdiff, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
simp_rw : (⊤ \ a) \ b = (⊤ \ b) \ a
⊢ ￢a \ b = ￢b \ a

Tactic:
simp_rw [← top_sdiff', sdiff_right_comm]

Premises used: sdiff_right_comm, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
rw : ⊤ \ a ≤ b ↔ Codisjoint a b
rw₁ : ⊤ ≤ a ⊔ b ↔ Codisjoint a b
rw₂ rw₃ : ⊤ ≤ a ⊔ b ↔ ⊤ ≤ a ⊔ b
⊢ ￢a ≤ b ↔ Codisjoint a b

Tactic:
rw [← top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]

Premises used: codisjoint_iff_le_sup, sdiff_le_iff, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ b ↔ Codisjoint b a

Tactic:
hnot_le_iff_codisjoint_right.trans codisjoint_comm

Premises used: codisjoint_comm, Iff.trans, hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
rw : Codisjoint a b ↔ ￢b ≤ a
rw₁ rw₂ : Codisjoint a b ↔ Codisjoint a b
⊢ ￢a ≤ b ↔ ￢b ≤ a

Tactic:
rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]

Premises used: hnot_le_iff_codisjoint_left, hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ Codisjoint a (￢a)

Tactic:
codisjoint_iff_le_sup.2 <| sdiff_le_iff.1 (top_sdiff' _).le

Premises used: Iff.mpr, Eq.le, codisjoint_iff_le_sup, Iff.mp, sdiff_le_iff, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ Codisjoint (￢a) a

Tactic:
codisjoint_hnot_right.symm

Premises used: codisjoint_hnot_right, Codisjoint.symm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : a ≤ b
⊢ Codisjoint (￢a) b

Tactic:
_root_.codisjoint_hnot_left.mono_right h

Premises used: codisjoint_hnot_left, Codisjoint.mono_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : b ≤ a
⊢ Codisjoint a (￢b)

Tactic:
_root_.codisjoint_hnot_right.mono_left h

Premises used: codisjoint_hnot_right, Codisjoint.mono_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ ￢a = b

Tactic:
h.2.hnot_le_right.antisymm <| Disjoint.le_of_codisjoint h.1.symm codisjoint_hnot_right

Premises used: Disjoint.le_of_codisjoint, codisjoint_hnot_right, LE.le.antisymm, Codisjoint.hnot_le_right, Disjoint.symm, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ a = ￢b

Tactic:
h.2.hnot_le_left.antisymm' <| Disjoint.le_of_codisjoint h.1 codisjoint_hnot_right

Premises used: Disjoint.le_of_codisjoint, LE.le.antisymm', codisjoint_hnot_right, Codisjoint.hnot_le_left, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ a ⊔ ￢a = ⊤

Tactic:
Codisjoint.eq_top codisjoint_hnot_right

Premises used: codisjoint_hnot_right, Codisjoint.eq_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ￢a ⊔ a = ⊤

Tactic:
Codisjoint.eq_top codisjoint_hnot_left

Premises used: codisjoint_hnot_left, Codisjoint.eq_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
rw : Codisjoint a ⊥ ↔ ⊤ ≤ a
rw₁ : a = ⊤ ↔ ⊤ ≤ a
rw₂ rw₃ : a = ⊤ ↔ a = ⊤
⊢ ￢⊥ ≤ a ↔ ⊤ ≤ a

Tactic:
rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]

Premises used: codisjoint_bot, hnot_le_iff_codisjoint_left, top_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
rw : Eq.{u_2 + 1} (α := α) (⊤ \ ⊤) ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := α) (￢⊤) ⊥

Tactic:
rw [← top_sdiff', sdiff_self]

Premises used: sdiff_self, top_sdiff'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Tactic:
codisjoint_hnot_right.hnot_le_left

Premises used: codisjoint_hnot_right, Codisjoint.hnot_le_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
⊢ Antitone.{u_2, u_2} (α := α) hnot

Tactic:
fun _ _ h => hnot_le_comm.1 <| hnot_hnot_le.trans h

Premises used: hnot_hnot_le, Antitone, Iff.mp, LE.le.trans, hnot_le_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
h : a ≤ b
⊢ ￢b ≤ ￢a

Tactic:
hnot_anti h

Premises used: hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ ￢￢￢a = ￢a

Tactic:
hnot_hnot_le.antisymm <| hnot_anti hnot_hnot_le

Premises used: hnot_hnot_le, LE.le.antisymm, hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
simp_rw : ￢￢￢a ≤ b ↔ ￢a ≤ b
⊢ Codisjoint (￢￢a) b ↔ Codisjoint a b

Tactic:
simp_rw [← hnot_le_iff_codisjoint_right, hnot_hnot_hnot]

Premises used: hnot_hnot_hnot, hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
simp_rw : ￢￢￢b ≤ a ↔ ￢b ≤ a
⊢ Codisjoint a (￢￢b) ↔ Codisjoint a b

Tactic:
simp_rw [← hnot_le_iff_codisjoint_left, hnot_hnot_hnot]

Premises used: hnot_le_iff_codisjoint_left, hnot_hnot_hnot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢(a ⊔ b) ≤ ￢a ⊓ ￢b

Tactic:
le_inf (hnot_anti le_sup_left) <| hnot_anti le_sup_right

Premises used: le_sup_left, le_sup_right, le_inf, hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

Tactic:
((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' ?_

Premises used: Eq.ge, LE.le.antisymm', le_hnot_inf_hnot, hnot_inf_distrib, LE.le.trans, hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
refine : ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b
⊢ ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b

Tactic:
refine ((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' ?_

Premises used: Eq.ge, LE.le.antisymm', le_hnot_inf_hnot, hnot_inf_distrib, LE.le.trans, hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
rw : Codisjoint (a ⊔ b) (￢(a ⊔ b))
⊢ ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b

Tactic:
rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff,
    codisjoint_left_comm, codisjoint_hnot_hnot_left_iff, ← codisjoint_assoc, sup_comm]

Premises used: hnot_le_iff_codisjoint_left, codisjoint_assoc, sup_comm, codisjoint_hnot_hnot_left_iff, codisjoint_left_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint (a ⊔ b) (￢(a ⊔ b))

Tactic:
codisjoint_hnot_right

Premises used: codisjoint_hnot_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ Codisjoint (a ⊔ b) (￢(a ⊔ b))

Tactic:
exact codisjoint_hnot_right

Premises used: codisjoint_hnot_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
a₁ : ￢￢(a \ b) ≤ ￢￢a \ ￢￢b
a₂ : ￢￢a \ ￢￢b ≤ ￢￢(a \ b)
⊢ ￢￢(a \ b) = ￢￢a \ ￢￢b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b

Tactic:
hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' ?_)

Premises used: sdiff_le_inf_hnot, Iff.mp, hnot_anti, hnot_le_comm, LE.le.trans'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
a₁ : ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b

Tactic:
refine hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' ?_)

Premises used: sdiff_le_inf_hnot, Iff.mp, hnot_anti, hnot_le_comm, LE.le.trans'
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
a₁ : ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)

Tactic:
rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ←
      hnot_le_iff_codisjoint_right]

Premises used: hnot_inf_distrib, codisjoint_left_comm, hnot_le_iff_codisjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b

Tactic:
le_sdiff_sup

Premises used: le_sdiff_sup
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b

Tactic:
exact le_sdiff_sup

Premises used: le_sdiff_sup
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
a₁ : ￢￢a ≤ ￢￢(b ⊔ a \ b)
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)

Tactic:
rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]

Premises used: sdiff_le_iff, hnot_hnot_sup_distrib
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)

Tactic:
hnot_anti (hnot_anti le_sup_sdiff)

Premises used: le_sup_sdiff, hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)

Tactic:
exact hnot_anti (hnot_anti le_sup_sdiff)

Premises used: le_sup_sdiff, hnot_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
rw : a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ⊓ a ≤ c
⊢ a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ a ⊓ b ≤ c

Tactic:
rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
⊢ a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ⊓ a ≤ c

Tactic:
sdiff_le_iff

Premises used: sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
⊢ a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ⊓ a ≤ c

Tactic:
exact sdiff_le_iff

Premises used: sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) aᶜ : α) (￢(ofDual : (a : αᵒᵈ) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (a ⇨ b) : α) ((ofDual : (a : αᵒᵈ) → α) b \ (ofDual : (a : αᵒᵈ) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (￢a) : αᵒᵈ) (((toDual : (a : α) → αᵒᵈ) a)ᶜ : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (a \ b) : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b ⇨ (toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : BiheytingAlgebra α
a : α
⊢ aᶜ ≤ ￢a

Tactic:
(disjoint_compl_left : Disjoint _ a).le_of_codisjoint codisjoint_hnot_right

Premises used: Disjoint.le_of_codisjoint, codisjoint_hnot_right, disjoint_compl_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
p q : Prop
⊢ p ⇨ q ↔ p → q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
p : Prop
⊢ pᶜ ↔ ¬p

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
pos : ∀ (h : b ≤ c), a ≤ ⊤ ↔ min a b ≤ c
neg : ∀ (h : ¬b ≤ c), a ≤ c ↔ min a b ≤ c
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ min a b ≤ c

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : b ≤ c
⊢ a ≤ ⊤ ↔ min a b ≤ c

Tactic:
iff_of_true le_top (inf_le_of_right_le h)

Premises used: inf_le_of_right_le, iff_of_true, le_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : b ≤ c
⊢ a ≤ ⊤ ↔ min a b ≤ c

Tactic:
exact iff_of_true le_top (inf_le_of_right_le h)

Premises used: inf_le_of_right_le, iff_of_true, le_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : ¬b ≤ c
neg : a ≤ c ↔ a ≤ c ∨ b ≤ c
neg₁ neg₂ : a ≤ c ↔ a ≤ c
⊢ a ≤ c ↔ min a b ≤ c

Tactic:
rw [inf_le_iff, or_iff_left h]

Premises used: inf_le_iff, or_iff_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
pos : ∀ (h : a ≤ b), ⊥ ≤ c ↔ a ≤ max b c
neg : ∀ (h : ¬a ≤ b), a ≤ c ↔ a ≤ max b c
⊢ (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ max b c

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : a ≤ b
⊢ ⊥ ≤ c ↔ a ≤ max b c

Tactic:
iff_of_true bot_le (le_sup_of_le_left h)

Premises used: le_sup_of_le_left, iff_of_true, bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : a ≤ b
⊢ ⊥ ≤ c ↔ a ≤ max b c

Tactic:
exact iff_of_true bot_le (le_sup_of_le_left h)

Premises used: le_sup_of_le_left, iff_of_true, bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : ¬a ≤ b
neg : a ≤ c ↔ a ≤ b ∨ a ≤ c
neg₁ neg₂ : a ≤ c ↔ a ≤ c
⊢ a ≤ c ↔ a ≤ max b c

Tactic:
rw [le_sup_iff, or_iff_right h]

Premises used: or_iff_right, le_sup_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ≤ ⊤
⊢ a ≤ ⊤

Tactic:
rw [← le, map_top]
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
rw : f a ≤ f (b ⇨ c) ↔ a ⊓ b ≤ c
rw₁ : f a ≤ f (b ⇨ c) ↔ f (a ⊓ b) ≤ f c
rw₂ : f a ≤ f b ⇨ f c ↔ f (a ⊓ b) ≤ f c
rw₃ : f a ≤ f b ⇨ f c ↔ f a ⊓ f b ≤ f c
rw₄ rw₅ : f a ⊓ f b ≤ f c ↔ f a ⊓ f b ≤ f c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
rw [← le, ← le, map_himp, map_inf, le_himp_iff]

Premises used: le_himp_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
rw : ⊥ ≤ f a
⊢ ⊥ ≤ a

Tactic:
rw [← le, map_bot]
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ ⊥ ≤ f a

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ ⊥ ≤ f a

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
rw : f (a \ b) ≤ f c ↔ a ≤ b ⊔ c
rw₁ : f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)
rw₂ : f a \ f b ≤ f c ↔ f a ≤ f (b ⊔ c)
rw₃ : f a \ f b ≤ f c ↔ f a ≤ f b ⊔ f c
rw₄ rw₅ : f a ≤ f b ⊔ f c ↔ f a ≤ f b ⊔ f c
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]

Premises used: sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : HImp α
inst_8 : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : ⊥ ≤ f a
⊢ ⊥ ≤ a

Tactic:
rw [← le, map_bot]