awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
simp_rw : a ≤ b ⊔ (c ⊔ d) ↔ a ≤ b ⊔ c ⊔ d
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d

Tactic:
simp_rw [sdiff_le_iff, sup_assoc]

Premises used: sup_assoc, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a \ b) \ c = a \ (b ⊔ c)

Tactic:
sdiff_sdiff _ _ _

Premises used: sdiff_sdiff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
simp_rw : a \ (b ⊔ c) = a \ (c ⊔ b)
⊢ (a \ b) \ c = (a \ c) \ b

Tactic:
simp_rw [sdiff_sdiff, sup_comm]

Premises used: sdiff_sdiff, sup_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a \ b) \ c = (a \ c) \ b

Tactic:
sdiff_right_comm _ _ _

Premises used: sdiff_right_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ (b ⊔ b) = a \ b
rw₁ rw₂ : a \ b = a \ b
⊢ (a \ b) \ b = a \ b

Tactic:
rw [sdiff_sdiff_left, sup_idem]

Premises used: sup_idem, sdiff_sdiff_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (a \ a) \ b = ⊥
rw₁ : ⊥ \ b = ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := α) ⊥ ⊥
⊢ (a \ b) \ a = ⊥

Tactic:
rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]

Premises used: bot_sdiff, sdiff_sdiff_comm, sdiff_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
simp_rw : a ⊔ b ≤ c ⊔ d ↔ a \ c ⊔ b \ c ≤ d
simp_rw₁ : a ≤ c ⊔ d ∧ b ≤ c ⊔ d ↔ a \ c ≤ d ∧ b \ c ≤ d
⊢ (a ⊔ b) \ c ≤ d ↔ a \ c ⊔ b \ c ≤ d

Tactic:
simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]

Premises used: sup_le_iff, sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
rw : a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d
⊢ a \ (b ⊓ c) ≤ d ↔ a \ b ⊔ a \ c ≤ d

Tactic:
rw [sup_le_iff, sdiff_le_comm, le_inf_iff]

Premises used: le_inf_iff, sup_le_iff, sdiff_le_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d

Tactic:
simp_rw [sdiff_le_comm]

Premises used: sdiff_le_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a ⊔ b) \ c = a \ c ⊔ b \ c

Tactic:
sup_sdiff_distrib _ _ _

Premises used: sup_sdiff_distrib
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ b ⊔ b \ b = a \ b
rw₁ : a \ b ⊔ ⊥ = a \ b
rw₂ rw₃ : a \ b = a \ b
⊢ (a ⊔ b) \ b = a \ b

Tactic:
rw [sup_sdiff, sdiff_self, sup_bot_eq]

Premises used: sdiff_self, sup_bot_eq, sup_sdiff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : (b ⊔ a) \ a = b \ a
rw₁ rw₂ : b \ a = b \ a
⊢ (a ⊔ b) \ a = b \ a

Tactic:
rw [sup_comm, sup_sdiff_right_self]

Premises used: sup_sdiff_right_self, sup_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ≤ b
⊢ a \ c ≤ b \ c

Tactic:
sdiff_le_iff.2 <| h.trans <| le_sup_sdiff

Premises used: Iff.mpr, le_sup_sdiff, sdiff_le_iff, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ≤ b
⊢ c \ b ≤ c \ a

Tactic:
sdiff_le_iff.2 <| le_sup_sdiff.trans <| sup_le_sup_right h _

Premises used: Iff.mpr, sup_le_sup_right, le_sup_sdiff, sdiff_le_iff, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a \ d ≤ b \ c

Tactic:
(sdiff_le_sdiff_right hab).trans <| sdiff_le_sdiff_left hcd

Premises used: sdiff_le_sdiff_right, LE.le.trans, sdiff_le_sdiff_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (b ⊓ c) = a \ b ⊔ a \ c

Tactic:
sdiff_inf_distrib _ _ _

Premises used: sdiff_inf_distrib
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : a \ a ⊔ a \ b = a \ b
rw₁ : ⊥ ⊔ a \ b = a \ b
rw₂ rw₃ : a \ b = a \ b
⊢ a \ (a ⊓ b) = a \ b

Tactic:
rw [sdiff_inf, sdiff_self, bot_sup_eq]

Premises used: sdiff_self, bot_sup_eq, sdiff_inf
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
rw : b \ a ⊔ b \ b = b \ a
rw₁ : b \ a ⊔ ⊥ = b \ a
rw₂ rw₃ : b \ a = b \ a
⊢ b \ (a ⊓ b) = b \ a

Tactic:
rw [sdiff_inf, sdiff_self, sup_bot_eq]

Premises used: sdiff_self, sup_bot_eq, sdiff_inf
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ ⊥
| a

Tactic:
rw [← @sdiff_bot _ _ a]

Premises used: sdiff_bot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
conv_rhs : a \ b = a \ ⊥
⊢ a \ b = a

Tactic:
conv_rhs => rw [← @sdiff_bot _ _ a]

Premises used: sdiff_bot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b = a \ (a ⊓ b)
rw₁ rw₂ : a \ b = a \ b
⊢ a \ b = a \ ⊥

Tactic:
rw [← h.eq_bot, sdiff_inf_self_left]

Premises used: sdiff_inf_self_left, Disjoint.eq_bot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ b \ a = b

Tactic:
h.symm.sdiff_eq_left

Premises used: Disjoint.sdiff_eq_left, Disjoint.symm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ a ⊔ b \ a = b
rw₁ : ⊥ ⊔ b \ a = b
rw₂ : b \ a = b
rw₃ rw₄ : b = b
⊢ (a ⊔ b) \ a = b

Tactic:
rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]

Premises used: Disjoint.sdiff_eq_right, sdiff_self, bot_sup_eq, sup_sdiff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
rw : a \ b ⊔ b \ b = a
rw₁ : a \ b ⊔ ⊥ = a
rw₂ : a \ b = a
rw₃ rw₄ : a = a
⊢ (a ⊔ b) \ b = a

Tactic:
rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]

Premises used: sdiff_self, sup_bot_eq, Disjoint.sdiff_eq_left, sup_sdiff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hac : Disjoint a c
hab : a ≤ b
⊢ a ≤ b \ c

Tactic:
hac.sdiff_eq_left.ge.trans <| sdiff_le_sdiff_right hab

Premises used: Eq.ge, sdiff_le_sdiff_right, Disjoint.sdiff_eq_left, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (a \ b) ≤ b

Tactic:
sdiff_le_iff.2 le_sdiff_sup

Premises used: Iff.mpr, sdiff_le_iff, le_sdiff_sup
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = b \ a ↔ a = b

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ≠ b \ a ↔ a ≠ b

Tactic:
sdiff_eq_sdiff_iff.not

Premises used: sdiff_eq_sdiff_iff, Iff.not
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
rw : a \ (a \ b) ≤ c ⊔ b \ c
⊢ a \ c ≤ a \ b ⊔ b \ c

Tactic:
rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]

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

Tactic:
sdiff_sdiff_le.trans le_sup_sdiff

Premises used: le_sup_sdiff, sdiff_sdiff_le, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c

Tactic:
exact sdiff_sdiff_le.trans le_sup_sdiff

Premises used: le_sup_sdiff, sdiff_sdiff_le, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ a \ b ⊔ b \ c = a \ c

Tactic:
(sdiff_triangle _ _ _).antisymm' <| sup_le (sdiff_le_sdiff_left hcb) (sdiff_le_sdiff_right hba)

Premises used: LE.le.antisymm', sdiff_le_sdiff_right, sup_le, sdiff_le_sdiff_left, sdiff_triangle
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ b \ c ≤ a \ c

Tactic:
simpa [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
refine : a \ b ≤ a \ c
⊢ a \ b ⊔ b \ c = a \ c

Tactic:
refine (sdiff_triangle ..).antisymm' <| sup_le ?_ <| by simpa [sup_comm]

Premises used: LE.le.antisymm', sup_le, sdiff_triangle
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
rw : a \ b ≤ a \ (a ⊓ c)
⊢ a \ b ≤ a \ c

Tactic:
rw [← sdiff_inf_self_left (b := c)]

Premises used: sdiff_inf_self_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ≤ a \ (a ⊓ c)

Tactic:
sdiff_le_sdiff_left hinf

Premises used: sdiff_le_sdiff_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ≤ a \ (a ⊓ c)

Tactic:
exact sdiff_le_sdiff_left hinf

Premises used: sdiff_le_sdiff_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
rw : (c ⊔ a) \ c ≤ (c ⊔ b) \ c
⊢ a \ c ≤ b \ c

Tactic:
rw [← sup_sdiff_left_self, ← @sup_sdiff_left_self _ _ _ b]

Premises used: sup_sdiff_left_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ (c ⊔ b) \ c

Tactic:
sdiff_le_sdiff_right h

Premises used: sdiff_le_sdiff_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ (c ⊔ b) \ c

Tactic:
exact sdiff_le_sdiff_right h

Premises used: sdiff_le_sdiff_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
rw : (a ⊔ c) \ c ≤ (b ⊔ c) \ c
⊢ a \ c ≤ b \ c

Tactic:
rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]

Premises used: sup_sdiff_right_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c

Tactic:
sdiff_le_sdiff_right h

Premises used: sdiff_le_sdiff_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c

Tactic:
exact sdiff_le_sdiff_right h

Premises used: sdiff_le_sdiff_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ⊓ (a ⊔ b) = a \ c

Tactic:
inf_of_le_left <| sdiff_le.trans le_sup_left

Premises used: le_sup_left, inf_of_le_left, sdiff_le, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ⊓ (b ⊔ a) = a \ c

Tactic:
inf_of_le_left <| sdiff_le.trans le_sup_right

Premises used: inf_of_le_left, le_sup_right, sdiff_le, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : GeneralizedCoheytingAlgebra α
a : α
⊢ GaloisConnection (fun (x : α) ↦ x \ a) fun (x : α) ↦ a ⊔ x

Tactic:
fun _ _ ↦ sdiff_le_iff

Premises used: sdiff_le_iff, GaloisConnection
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d 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, GeneralizedCoheytingAlgebra.sdiff_le_iff
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)

Tactic:
rfl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d : α
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 : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d : α
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 : GeneralizedCoheytingAlgebra α
a_1 b_1 c_1 d : α
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_1
α_1 : Type u_2
β : Type u_3
inst : GeneralizedCoheytingAlgebra α_1
a b c d : α_1
α : ι → Type u_4
inst_1 : (i : ι) → GeneralizedCoheytingAlgebra (α i)
i : (i : ι) → α i
⊢ ∀ (b c : (i : ι) → α i), i \ b ≤ c ↔ i ≤ b ⊔ c

Tactic:
simp [le_def]

Premises used: Pi.le_def
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ⇨ ⊥ = aᶜ

Tactic:
HeytingAlgebra.himp_bot _

Premises used: HeytingAlgebra.himp_bot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ ⊥ ⇨ a = ⊤

Tactic:
himp_eq_top_iff.2 bot_le

Premises used: Iff.mpr, himp_eq_top_iff, bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
simp_rw : a ⊔ b ⇨ ⊥ = (a ⇨ ⊥) ⊓ (b ⇨ ⊥)
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Tactic:
simp_rw [← himp_bot, sup_himp_distrib]

Premises used: himp_bot, sup_himp_distrib
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ

Tactic:
compl_sup_distrib _ _

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

Tactic:
(himp_bot _).ge.trans <| himp_le_himp_left bot_le

Premises used: Eq.ge, himp_bot, himp_le_himp_left, LE.le.trans, bot_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ aᶜ ⊔ b ≤ a ⇨ b

Tactic:
sup_le compl_le_himp le_himp

Premises used: compl_le_himp, sup_le, le_himp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ b ⊔ aᶜ ≤ a ⇨ b

Tactic:
sup_le le_himp compl_le_himp

Premises used: compl_le_himp, sup_le, le_himp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : a ⇨ a ⇨ ⊥ = a ⇨ ⊥
rw₁ : a ⊓ a ⇨ ⊥ = a ⇨ ⊥
rw₂ rw₃ : a ⇨ ⊥ = a ⇨ ⊥
⊢ a ⇨ aᶜ = aᶜ

Tactic:
rw [← himp_bot, himp_himp, inf_idem]

Premises used: himp_bot, himp_himp, inf_idem
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
simp_rw : a ⇨ b ⇨ ⊥ = b ⇨ a ⇨ ⊥
⊢ a ⇨ bᶜ = b ⇨ aᶜ

Tactic:
simp_rw [← himp_bot, himp_left_comm]

Premises used: himp_bot, himp_left_comm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
rw : a ≤ b ⇨ ⊥ ↔ Disjoint a b
rw₁ : a ⊓ b ≤ ⊥ ↔ Disjoint a b
rw₂ rw₃ : a ⊓ b ≤ ⊥ ↔ a ⊓ b ≤ ⊥
⊢ a ≤ bᶜ ↔ Disjoint a b

Tactic:
rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]

Premises used: himp_bot, le_himp_iff, disjoint_iff_inf_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ Disjoint b a

Tactic:
le_compl_iff_disjoint_right.trans disjoint_comm

Premises used: disjoint_comm, Iff.trans, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
rw : Disjoint a b ↔ b ≤ aᶜ
rw₁ rw₂ : Disjoint a b ↔ Disjoint a b
⊢ a ≤ bᶜ ↔ b ≤ aᶜ

Tactic:
rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]

Premises used: le_compl_iff_disjoint_left, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ Disjoint aᶜ a

Tactic:
disjoint_iff_inf_le.mpr <| le_himp_iff.1 (himp_bot _).ge

Premises used: Iff.mpr, Eq.ge, himp_bot, le_himp_iff, Iff.mp, disjoint_iff_inf_le
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ Disjoint a aᶜ

Tactic:
disjoint_compl_left.symm

Premises used: disjoint_compl_left, Disjoint.symm
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : b ≤ a
⊢ Disjoint aᶜ b

Tactic:
_root_.disjoint_compl_left.mono_right h

Premises used: disjoint_compl_left, Disjoint.mono_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : a ≤ b
⊢ Disjoint a bᶜ

Tactic:
_root_.disjoint_compl_right.mono_left h

Premises used: Disjoint.mono_left, disjoint_compl_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : IsCompl a b
⊢ aᶜ = b

Tactic:
h.1.le_compl_left.antisymm' <| Disjoint.le_of_codisjoint disjoint_compl_left h.2

Premises used: Disjoint.le_of_codisjoint, LE.le.antisymm', disjoint_compl_left, Disjoint.le_compl_left, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : IsCompl a b
⊢ a = bᶜ

Tactic:
h.1.le_compl_right.antisymm <| Disjoint.le_of_codisjoint disjoint_compl_left h.2.symm

Premises used: Disjoint.le_of_codisjoint, LE.le.antisymm, disjoint_compl_left, Disjoint.le_compl_right, Codisjoint.symm, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h₀ : a ⊓ b = ⊥
h₁ : a ⊔ b = ⊤
⊢ aᶜ = b

Tactic:
(IsCompl.of_eq h₀ h₁).compl_eq

Premises used: IsCompl.compl_eq, IsCompl.of_eq
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ⊓ aᶜ = ⊥

Tactic:
disjoint_compl_right.eq_bot

Premises used: disjoint_compl_right, Disjoint.eq_bot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ aᶜ ⊓ a = ⊥

Tactic:
disjoint_compl_left.eq_bot

Premises used: disjoint_compl_left, Disjoint.eq_bot
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ⊓ aᶜ = ⊥

Tactic:
inf_compl_self _

Premises used: inf_compl_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ aᶜ ⊓ a = ⊥

Tactic:
compl_inf_self _

Premises used: compl_inf_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : Disjoint a ⊤ ↔ a ≤ ⊥
rw₁ : a = ⊥ ↔ a ≤ ⊥
rw₂ rw₃ : a = ⊥ ↔ a = ⊥
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

Premises used: le_bot_iff, disjoint_top, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
rw : Eq.{u_2 + 1} (α := α) (⊥ ⇨ ⊥) ⊤
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) ⊤ ⊤
⊢ Eq.{u_2 + 1} (α := α) ⊥ᶜ ⊤

Tactic:
rw [← himp_bot, himp_self]

Premises used: himp_bot, himp_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
rw : Disjoint a a ↔ a = ⊥
rw₁ rw₂ : a = ⊥ ↔ a = ⊥
⊢ a ≤ aᶜ ↔ a = ⊥

Tactic:
rw [le_compl_iff_disjoint_left, disjoint_self]

Premises used: le_compl_iff_disjoint_left, disjoint_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
inst_1 : Nontrivial α
h : a = aᶜ
⊢ Eq.{u_2 + 1} (α := α) ⊥ ⊥ᶜ

Tactic:
cases le_compl_self.1 (le_of_eq h)

Premises used: le_compl_self, Iff.mp, le_of_eq
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
inst_1 : Nontrivial α
h : Eq.{u_2 + 1} (α := α) ⊥ ⊥ᶜ
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
inst_1 : Nontrivial α
⊢ aᶜ ≠ a

Tactic:
ne_comm.1 ne_compl_self

Premises used: Iff.mp, ne_comm, ne_compl_self
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
inst_1 : Nontrivial α
rw : a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
⊢ a < aᶜ ↔ a = ⊥

Tactic:
rw [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
inst_1 : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ a ≤ aᶜᶜ

Tactic:
disjoint_compl_right.le_compl_right

Premises used: Disjoint.le_compl_right, disjoint_compl_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
⊢ Antitone.{u_2, u_2} (α := α) compl

Tactic:
fun _ _ h =>
  le_compl_comm.1 <| h.trans le_compl_compl

Premises used: Antitone, Iff.mp, le_compl_comm, le_compl_compl, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
h : a ≤ b
⊢ bᶜ ≤ aᶜ

Tactic:
compl_anti h

Premises used: compl_anti
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a : α
⊢ aᶜᶜᶜ = aᶜ

Tactic:
(compl_anti le_compl_compl).antisymm le_compl_compl

Premises used: compl_anti, LE.le.antisymm, le_compl_compl
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
simp_rw : b ≤ aᶜᶜᶜ ↔ b ≤ aᶜ
⊢ Disjoint aᶜᶜ b ↔ Disjoint a b

Tactic:
simp_rw [← le_compl_iff_disjoint_left, compl_compl_compl]

Premises used: compl_compl_compl, le_compl_iff_disjoint_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
simp_rw : a ≤ bᶜᶜᶜ ↔ a ≤ bᶜ
⊢ Disjoint a bᶜᶜ ↔ Disjoint a b

Tactic:
simp_rw [← le_compl_iff_disjoint_right, compl_compl_compl]

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

Tactic:
sup_le (compl_anti inf_le_left) <| compl_anti inf_le_right

Premises used: compl_anti, inf_le_right, sup_le, inf_le_left
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

Tactic:
((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_

Premises used: compl_sup_compl_le, compl_anti, LE.le.antisymm, Eq.le, compl_sup_distrib, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
refine : aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ
⊢ (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ

Tactic:
refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_

Premises used: compl_sup_compl_le, compl_anti, LE.le.antisymm, Eq.le, compl_sup_distrib, LE.le.trans
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
rw : Disjoint (a ⊓ b) (a ⊓ b)ᶜ
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
    disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]

Premises used: disjoint_left_comm, disjoint_compl_compl_left_iff, disjoint_assoc, inf_comm, le_compl_iff_disjoint_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ

Tactic:
disjoint_compl_right

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

Tactic:
exact disjoint_compl_right

Premises used: disjoint_compl_right
-- Module: Mathlib.Order.Heyting.Basic
Goal:
α : Type u_2
inst : HeytingAlgebra α
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 : HeytingAlgebra α
a b : α
a₁ : ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ
⊢ (a ⇨ b)ᶜᶜ ≤ aᶜᶜ ⇨ bᶜᶜ

Tactic:
rw [le_himp_iff, ← compl_compl_inf_distrib]

Premises used: le_himp_iff, compl_compl_inf_distrib