awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
le : ∀ {x y : α}, LE.le.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_1} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_sdiff :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
map_himp :
  ∀ (a b : α), Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
⊢ BooleanAlgebra α

Tactic:
apply e.injective.booleanAlgebra

Premises used: Function.Injective.booleanAlgebra, Equiv.injective
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x_1 y_1 : α
⊢ LE.le.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 ≤ y_1

Tactic:
rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x_1 y_1 : α
⊢ LE.le.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 ≤ y_1

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x_1 y_1 : α
⊢ LT.lt.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 < y_1

Tactic:
rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x_1 y_1 : α
⊢ LT.lt.{u_1} (α := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y_1 : β) ↔ x_1 < y_1

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a : α
⊢ Eq.{u_1 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a b : α
⊢ Eq.{u_1 + 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.BooleanAlgebra.Defs
Goal:
⊢ (fun (x1 x2 : Bool) ↦ max x1 x2) = or

Tactic:
dsimp
-- Module: Mathlib.Order.BooleanAlgebra.Defs
Goal:
⊢ (fun (x1 x2 : Bool) ↦ min x1 x2) = and

Tactic:
dsimp
-- Module: Mathlib.Order.BooleanAlgebra.Defs
Goal:
⊢ compl = not

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanAlgebra.Defs
Goal:
α : Type u
β : Type u_1
x y z : α
⊢ ∀ (x y z : PUnit.{u_2 + 1}), min (max x y) (max x z) ≤ max x (min y z)

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b c : Set α
⊢ (a ∩ b) \ c = a ∩ (b \ c)

Tactic:
inf_sdiff_assoc ..

Premises used: inf_sdiff_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s \ t ∩ u = (s ∩ u) \ t

Tactic:
sdiff_inf_right_comm ..

Premises used: sdiff_inf_right_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s ∩ (t \ u) = t ∩ (s \ u)

Tactic:
inf_sdiff_left_comm ..

Premises used: inf_sdiff_left_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
hts : t ⊆ s
hut : u ⊆ t
⊢ s \ t ∪ t \ u = s \ u

Tactic:
sdiff_sup_sdiff_cancel hts hut

Premises used: sdiff_sup_sdiff_cancel
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
hi : s ∩ u ⊆ t
hu : t ⊆ s ∪ u
⊢ s \ t ∪ t \ u = s \ u

Tactic:
sdiff_sup_sdiff_cancel' hi hu

Premises used: sdiff_sup_sdiff_cancel'
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
h : u ⊆ s
⊢ s \ (t \ u) = s \ t ∪ u

Tactic:
sdiff_sdiff_eq_sdiff_sup h

Premises used: sdiff_sdiff_eq_sdiff_sup
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)

Tactic:
inf_sdiff_distrib_left _ _ _

Premises used: inf_sdiff_distrib_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s \ t ∩ u = (s ∩ u) \ (t ∩ u)

Tactic:
inf_sdiff_distrib_right _ _ _

Premises used: inf_sdiff_distrib_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t r : Set α
⊢ (t ∩ r) \ s = t \ s ∩ (r \ s)

Tactic:
inf_sdiff

Premises used: inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ = {x : α | ¬x ∈ s}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ

Tactic:
h

Premises used: Set.Mem, setOf, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_3
p : α → Prop
⊢ Eq.{u_3 + 1} (α := Set α) {a : α | p a}ᶜ {a : α | ¬p a}

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
x : α
h : x ∈ sᶜ
⊢ ¬x ∈ s

Tactic:
h

Premises used: Set.Mem, setOf, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ sᶜ ↔ x ∈ s

Tactic:
not_not

Premises used: Classical.not_not, Set.Mem, setOf, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ s ∩ sᶜ = ∅

Tactic:
inf_compl_eq_bot

Premises used: inf_compl_eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ ∩ s = ∅

Tactic:
compl_inf_eq_bot

Premises used: compl_inf_eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) ∅ᶜ univ

Tactic:
compl_bot

Premises used: Set.Mem, setOf, compl_bot
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t)ᶜ = sᶜ ∩ tᶜ

Tactic:
compl_sup

Premises used: Set.Mem, setOf, compl_sup
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s ∩ t)ᶜ = sᶜ ∪ tᶜ

Tactic:
compl_inf

Premises used: compl_inf, Set.Mem, setOf
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) univᶜ ∅

Tactic:
compl_top

Premises used: Set.Mem, setOf, compl_top
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ = ∅ ↔ s = univ

Tactic:
compl_eq_bot

Premises used: compl_eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ = univ ↔ s = ∅

Tactic:
compl_eq_top

Premises used: compl_eq_top
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ ≠ univ ↔ s.Nonempty

Tactic:
compl_univ_iff.not.trans nonempty_iff_ne_empty.symm

Premises used: Iff.not, Set.nonempty_iff_ne_empty, Iff.trans, Iff.symm, Set.compl_univ_iff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ

Tactic:
grind
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ.Nonempty ↔ s ≠ univ

Tactic:
(ne_univ_iff_exists_notMem s).symm

Premises used: Set.Mem, setOf, Set.ne_univ_iff_exists_notMem, Set.Nonempty, Not, Iff.symm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ∪ t = (sᶜ ∩ tᶜ)ᶜ

Tactic:
ext fun _ => or_iff_not_and_not

Premises used: Set.ext, or_iff_not_and_not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ∩ t = (sᶜ ∪ tᶜ)ᶜ

Tactic:
ext fun _ => and_iff_not_or_not

Premises used: Set.ext, and_iff_not_or_not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ s ∪ sᶜ = univ

Tactic:
eq_univ_iff_forall.2 fun _ => em _

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Membership.mem, em
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
rw : s ∪ sᶜ = univ
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ sᶜ ∪ s = univ

Tactic:
rw [union_comm, union_compl_self]

Premises used: Set.union_comm, Set.union_compl_self
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ sᶜ ⊆ t ↔ tᶜ ⊆ s

Tactic:
@compl_le_iff_compl_le _ s _ _

Premises used: compl_le_iff_compl_le
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ⊆ tᶜ ↔ t ⊆ sᶜ

Tactic:
@le_compl_iff_le_compl _ _ _ t

Premises used: le_compl_iff_le_compl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ sᶜ ⊆ tᶜ ↔ t ⊆ s

Tactic:
@compl_le_compl_iff_le (Set α) _ _ _

Premises used: compl_le_compl_iff_le
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
h : t ⊆ s
⊢ sᶜ ⊆ tᶜ

Tactic:
compl_subset_compl.2 h

Premises used: Iff.mpr, Set.compl_subset_compl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t

Tactic:
(@isCompl_compl _ u _).le_sup_right_iff_inf_left_le

Premises used: IsCompl.le_sup_right_iff_inf_left_le, isCompl_compl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ sᶜ ⊆ t ↔ s ∪ t = univ

Tactic:
Iff.symm <| eq_univ_iff_forall.trans <| forall_congr' fun _ => or_iff_not_imp_left

Premises used: Set.eq_univ_iff_forall, Classical.or_iff_not_imp_left, forall_congr', Iff.trans, Iff.symm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b c : Set α
⊢ a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c

Tactic:
forall_congr' fun _ => and_imp.trans <| imp_congr_right fun _ => imp_iff_not_or

Premises used: imp_congr_right, and_imp, Set.Subset, imp_iff_not_or, forall_congr', Iff.trans
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
x : α
⊢ x ∈ s ∧ ¬x ∈ t ↔ x ∈ s ∩ tᶜ

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ⊆ tᶜ ↔ Disjoint t s

Tactic:
le_compl_iff_disjoint_left

Premises used: le_compl_iff_disjoint_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ⊆ tᶜ ↔ Disjoint s t

Tactic:
le_compl_iff_disjoint_right

Premises used: le_compl_iff_disjoint_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ Disjoint sᶜ t ↔ t ⊆ s

Tactic:
disjoint_compl_left_iff

Premises used: disjoint_compl_left_iff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ Disjoint s tᶜ ↔ s ⊆ t

Tactic:
disjoint_compl_right_iff

Premises used: disjoint_compl_right_iff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
inst : Nontrivial α
x : α
⊢ Set.Nonempty (α := α) {x}ᶜ

Tactic:
exists_ne x

Premises used: Set.Mem, setOf, exists_ne, Set.Nonempty, Set.singleton, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b : α
⊢ Membership.mem (γ := Set α) {b}ᶜ a ↔ a ≠ b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {a}ᶜ {x : α | x ≠ a}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.singleton, rfl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {x : α | x ≠ a}ᶜ {a}

Tactic:
compl_compl _

Premises used: compl_compl, Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
⊢ s ⊆ {a}ᶜ ↔ ¬a ∈ s

Tactic:
subset_compl_comm.trans singleton_subset_iff

Premises used: Set.singleton_subset_iff, Set.subset_compl_comm, Iff.trans
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
x : α
hx : x ∈ t
⊢ ¬x ∈ s \ t

Tactic:
fun h => h.2 hx

Premises used: And.right, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
x : α
h : x ∈ s \ t
⊢ x ∈ s

Tactic:
h.left

Premises used: And.left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
x : α
h : x ∈ s \ t
⊢ ¬x ∈ t

Tactic:
h.right

Premises used: And.right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
rw : s ∩ tᶜ = tᶜ ∩ s
rw₁ rw₂ : tᶜ ∩ s = tᶜ ∩ s
⊢ s \ t = tᶜ ∩ s

Tactic:
rw [diff_eq, inter_comm]

Premises used: Set.diff_eq, Set.inter_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s \ t).Nonempty ↔ ¬s ⊆ t

Tactic:
inter_compl_nonempty_iff

Premises used: Set.Mem, Set.diff, setOf, Set.inter_compl_nonempty_iff, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s \ t ⊆ s

Tactic:
show s \ t ≤ s from sdiff_le

Premises used: sdiff_le
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s \ t ⊆ tᶜ

Tactic:
diff_eq_compl_inter ▸ inter_subset_left

Premises used: Set.diff_eq_compl_inter, Eq.rec, Set.inter_subset_left, Eq.symm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
h₁ : s ⊆ t
h₂ : t ⊆ u
⊢ t ∪ u \ s = u

Tactic:
sup_sdiff_cancel' h₁ h₂

Premises used: sup_sdiff_cancel'
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s ∪ t \ s = t

Tactic:
sup_sdiff_cancel_right h

Premises used: sup_sdiff_cancel_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
h : s ∩ t ⊆ ∅
⊢ (s ∪ t) \ s = t

Tactic:
Disjoint.sup_sdiff_cancel_left <| disjoint_iff_inf_le.2 h

Premises used: Iff.mpr, Disjoint.sup_sdiff_cancel_left, disjoint_iff_inf_le
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
h : s ∩ t ⊆ ∅
⊢ (s ∪ t) \ t = s

Tactic:
Disjoint.sup_sdiff_cancel_right <| disjoint_iff_inf_le.2 h

Premises used: Iff.mpr, disjoint_iff_inf_le, Disjoint.sup_sdiff_cancel_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t) \ s = t \ s

Tactic:
sup_sdiff_left_self

Premises used: sup_sdiff_left_self
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t) \ t = s \ t

Tactic:
sup_sdiff_right_self

Premises used: sup_sdiff_right_self
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ (s ∪ t) \ u = s \ u ∪ t \ u

Tactic:
sup_sdiff

Premises used: sup_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b : Set α
⊢ a ∩ (b \ a) = ∅

Tactic:
inf_sdiff_self_right

Premises used: inf_sdiff_self_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ∩ t ∪ s \ t = s

Tactic:
sup_inf_sdiff s t

Premises used: sup_inf_sdiff