awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
rw : s ∩ t ∪ s \ t = s
⊢ s \ t ∪ s ∩ t = s

Tactic:
rw [union_comm]

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

Tactic:
sup_inf_sdiff _ _

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

Tactic:
exact sup_inf_sdiff _ _

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

Tactic:
inter_union_diff _ _

Premises used: Set.Mem, setOf, Set.inter, Set.inter_union_diff, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ t ⊆ s ∩ t ∪ sᶜ

Tactic:
simp [inter_union_distrib_right]

Premises used: Set.inter_union_distrib_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ⊆ s ∩ t ∪ tᶜ

Tactic:
simp [inter_union_distrib_right]

Premises used: Set.inter_union_distrib_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t) ∩ sᶜ ⊆ t

Tactic:
simp [union_inter_distrib_right]

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t) ∩ tᶜ ⊆ s

Tactic:
simp [union_inter_distrib_right]

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s₁ s₂ t₁ t₂ : Set α
⊢ s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

Tactic:
show s₁ ≤ s₂ → t₂ ≤ t₁ → s₁ \ t₁ ≤ s₂ \ t₂ from sdiff_le_sdiff

Premises used: sdiff_le_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s₁ s₂ t : Set α
h : s₁ ⊆ s₂
⊢ s₁ \ t ⊆ s₂ \ t

Tactic:
sdiff_le_sdiff_right ‹s₁ ≤ s₂›

Premises used: sdiff_le_sdiff_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
h : t ⊆ u
⊢ s \ u ⊆ s \ t

Tactic:
sdiff_le_sdiff_left ‹t ≤ u›

Premises used: sdiff_le_sdiff_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t r : Set α
hs : s ⊆ r
ht : t ⊆ r
⊢ r \ s ⊆ r \ t ↔ t ⊆ s

Tactic:
sdiff_le_sdiff_iff_le hs ht

Premises used: sdiff_le_sdiff_iff_le
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ sᶜ = univ \ s

Tactic:
top_sdiff.symm

Premises used: top_sdiff, Eq.symm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ ∅ \ s = ∅

Tactic:
bot_sdiff

Premises used: bot_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s \ t = ∅ ↔ s ⊆ t

Tactic:
sdiff_eq_bot_iff

Premises used: sdiff_eq_bot_iff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ s \ ∅ = s

Tactic:
sdiff_bot

Premises used: sdiff_bot
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ s \ univ = ∅

Tactic:
diff_eq_empty.2 (subset_univ s)

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

Tactic:
sdiff_sdiff_left

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

Tactic:
sdiff_sdiff_comm

Premises used: sdiff_sdiff_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s \ t ⊆ u ↔ s ⊆ t ∪ u

Tactic:
show s \ t ≤ u ↔ s ≤ t ∪ u from sdiff_le_iff

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

Tactic:
show s ≤ s \ t ∪ t from le_sdiff_sup

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

Tactic:
Subset.antisymm (union_subset diff_subset h) (subset_diff_union _ _)

Premises used: Set.Subset.antisymm, Set.diff_subset, Set.union_subset, Set.subset_diff_union
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s \ t ⊆ u ↔ s \ u ⊆ t

Tactic:
show s \ t ≤ u ↔ s \ u ≤ t from sdiff_le_comm

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

Tactic:
sdiff_inf

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

Tactic:
sdiff_sup.symm

Premises used: sdiff_sup, Eq.symm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s \ tᶜ = s ∩ t

Tactic:
sdiff_compl

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

Tactic:
Eq.trans compl_sdiff himp_eq

Premises used: compl_sdiff, himp_eq, Eq.trans
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s \ (t \ u) = s \ t ∪ s ∩ u

Tactic:
sdiff_sdiff_right'

Premises used: sdiff_sdiff_right'
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
rw : s ∩ t ∩ uᶜ = s \ u ∩ t
rw₁ : s ∩ t ∩ uᶜ = s ∩ uᶜ ∩ t
rw₂ rw₃ : s ∩ uᶜ ∩ t = s ∩ uᶜ ∩ t
⊢ (s ∩ t) \ u = s \ u ∩ t

Tactic:
rw [diff_eq, diff_eq, inter_right_comm]

Premises used: Set.diff_eq, Set.inter_right_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
rw : s ∩ uᶜ ∩ t = (s ∩ t) \ u
rw₁ : s ∩ uᶜ ∩ t = s ∩ t ∩ uᶜ
rw₂ rw₃ : s ∩ t ∩ uᶜ = s ∩ t ∩ uᶜ
⊢ s \ u ∩ t = (s ∩ t) \ u

Tactic:
rw [diff_eq, diff_eq, inter_right_comm]

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

Tactic:
sup_sdiff_self _ _

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

Tactic:
sdiff_sup_self _ _

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

Tactic:
inf_sdiff_self_left

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

Tactic:
sdiff_inf_self_right _ _

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

Tactic:
sdiff_inf_self_left _ _

Premises used: sdiff_inf_self_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
⊢ s \ s = ∅

Tactic:
sdiff_self

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

Tactic:
sdiff_sdiff_right_self

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

Tactic:
sdiff_sdiff_eq_self h

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

Tactic:
sup_eq_sdiff_sup_sdiff_sup_inf

Premises used: sup_eq_sdiff_sup_sdiff_sup_inf
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
p : α → Prop
⊢ s \ {a : α | a ∈ s ∧ p a} = {a : α | a ∈ s ∧ ¬p a}

Tactic:
diff_self_inter

Premises used: Set.diff_self_inter, Set.Mem, Set.diff, setOf, Set.inter
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ Disjoint (t \ s) s

Tactic:
disjoint_sdiff_self_left

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

Tactic:
disjoint_sdiff_self_right

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

Tactic:
disjoint_of_subset_right inter_subset_right disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left, Set.disjoint_of_subset_right, Set.inter_subset_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t u : Set α
⊢ s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

Tactic:
le_iff_subset.symm.trans le_sdiff

Premises used: le_sdiff, Iff.trans, Set.le_iff_subset, Iff.symm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ Disjoint s t ↔ s = ∅

Tactic:
disjoint_of_le_iff_left_eq_bot h

Premises used: disjoint_of_le_iff_left_eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
rw : (t ∩ s).Nonempty ↔ (s ∩ t).Nonempty
rw₁ rw₂ : (s ∩ t).Nonempty ↔ (s ∩ t).Nonempty
⊢ ¬Disjoint t s ↔ (s ∩ t).Nonempty

Tactic:
rw [not_disjoint_iff_nonempty_inter, inter_comm]

Premises used: Set.not_disjoint_iff_nonempty_inter, Set.inter_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
⊢ t \ s ⊂ t

Tactic:
simpa [inter_eq_self_of_subset_right hst]

Premises used: Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s ⊂ t ↔ ∃ (a : α), a ∈ t ∧ s ⊆ t \ {a}

Tactic:
grind
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
a : α
⊢ s \ {a} ⊆ t ↔ s ⊆ insert a t

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
a : α
h : s ⊆ t
ha : ¬a ∈ s
⊢ s ⊆ t \ {a}

Tactic:
subset_inter h <| subset_compl_comm.1 <| singleton_subset_iff.2 ha

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Mem, Set.subset_compl_comm, Set.diff, setOf, Set.subset_inter, Iff.mp, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
x : α
s : Set α
rw rw₁ : s \ {x} ⊆ s \ {x}
⊢ s ⊆ insert x (s \ {x})

Tactic:
rw [← diff_singleton_subset_iff]

Premises used: Set.diff_singleton_subset_iff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
a : α
h : ¬a ∈ s
⊢ s \ insert a t = s \ t

Tactic:
grind
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t : Set α
a : α
s : Set α
h : a ∈ t
⊢ insert a s \ t = s \ t

Tactic:
grind
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t : Set α
a : α
s : Set α
h : ¬a ∈ t
⊢ insert a s \ t = insert a (s \ t)

Tactic:
grind
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
h₁ : ∀ (x : α), x ∈ insert a s \ {a} ↔ x ∈ s
⊢ insert a s \ {a} = s

Tactic:
ext x
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
x : α
⊢ x ∈ insert a s \ {a} ↔ x ∈ s

Tactic:
simp [and_iff_left_of_imp (ne_of_mem_of_not_mem · h)]

Premises used: and_iff_left_of_imp, ne_of_mem_of_not_mem
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
h : ∀ (x : α), x ∈ insert a (s \ {a}) ↔ x ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
ext
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x : α
⊢ x ∈ insert a (s \ {a}) ↔ x ∈ s

Tactic:
simp +contextual [or_and_left, em, ha]

Premises used: em, or_and_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
b : α
hbt : ¬b ∈ t
⊢ b ∈ insert b (s \ t)

Tactic:
simp [*]
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
a b : α
hbt : ¬b ∈ t
hbs : b ∈ s
⊢ b ∈ insert a (s \ t)

Tactic:
simp [*]
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a : α
⊢ InvOn (insert a) (fun (s : Set α) ↦ s \ {a}) {s : Set α | a ∈ s} {s : Set α | ¬a ∈ s}

Tactic:
⟨fun _s ha ↦ insert_diff_self_of_mem ha, fun _s ↦ insert_diff_self_of_notMem⟩

Premises used: Set.InvOn, Set.insert_diff_self_of_notMem, And.intro, Set.insert_diff_self_of_mem
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint {a} s

Tactic:
simp [h]
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⊂ s ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a : α
⊢ insert a (s \ {a}) = insert a s

Tactic:
simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]

Premises used: Set.insert_eq, Set.singleton_union, Set.union_singleton, Set.union_diff_self
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b : α
hab : a ≠ b
s : Set α
simp_rw : s \ {b} ∪ {a} = (s ∪ {a}) \ {b}
simp_rw₁ : s \ {b} ∪ {a} = s \ {b} ∪ {a} \ {b}
⊢ insert a (s \ {b}) = insert a s \ {b}

Tactic:
simp_rw [← union_singleton, union_diff_distrib,
    diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]

Premises used: Iff.mpr, Set.diff_singleton_eq_self, Iff.not, Ne.symm, Set.mem_singleton_iff, Set.union_diff_distrib, Set.union_singleton
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
a : α
rw : insert a (s \ (t ∪ {a})) = insert a (s \ t)
rw₁ : insert a ((s \ t) \ {a}) = insert a (s \ t)
rw₂ rw₃ : insert a (s \ t) = insert a (s \ t)
⊢ insert a (s \ insert a t) = insert a (s \ t)

Tactic:
rw [← union_singleton (s := t), ← diff_diff, insert_diff_singleton]

Premises used: Set.diff_diff, Set.insert_diff_singleton, Set.union_singleton
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
a b : α
⊢ a ∈ s \ {b} ↔ a ∈ s ∧ a ≠ b

Tactic:
.rfl

Premises used: Set.Mem, Set.diff, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s : Set α
t : Set (Set α)
⊢ s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty

Tactic:
mem_diff_singleton.trans <| and_congr_right' nonempty_iff_ne_empty.symm

Premises used: and_congr_right', Set.nonempty_iff_ne_empty, Iff.trans, Iff.symm, Set.mem_diff_singleton
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
a : α
⊢ s ⊆ insert a t ↔ s ⊆ t ∨ a ∈ s ∧ s \ {a} ⊆ t

Tactic:
grind
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b : α
hab : a ≠ b
⊢ ¬Membership.mem (γ := Set α) {b} a

Tactic:
simpa
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b : α
hab : a ≠ b
rw : Eq (α := Set α) ({b} \ {a}) {b}
rw₁ rw₂ : Eq (α := Set α) {b} {b}
⊢ Eq (α := Set α) ({a, b} \ {a}) {b}

Tactic:
rw [insert_diff_of_mem _ (mem_singleton a), diff_singleton_eq_self (by simpa)]

Premises used: Set.mem_singleton, Set.diff_singleton_eq_self, Set.insert_diff_of_mem
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
a b : α
hab : a ≠ b
rw : Eq (α := Set α) ({b, a} \ {b}) {a}
rw₁ rw₂ : Eq (α := Set α) {a} {a}
⊢ Eq (α := Set α) ({a, b} \ {b}) {a}

Tactic:
rw [pair_comm, pair_diff_left hab.symm]

Premises used: Set.pair_diff_left, Ne.symm, Set.pair_comm
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' : Set α
rw : (s ∩ t ∪ s' \ t) ∩ t = s ∩ t
rw₁ : s ∩ t ∩ t ∪ s' \ t ∩ t = s ∩ t
rw₂ : s ∩ t ∩ t ∪ ∅ = s ∩ t
rw₃ : s ∩ (t ∩ t) ∪ ∅ = s ∩ t
rw₄ : s ∩ t ∪ ∅ = s ∩ t
rw₅ rw₆ : s ∩ t = s ∩ t
⊢ t.ite s s' ∩ t = s ∩ t

Tactic:
rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]

Premises used: Set.ite, Set.union_empty, Set.inter_self, Set.diff_inter_self, Set.union_inter_distrib_right, Set.inter_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' : Set α
rw : s ∩ tᶜ ∪ s' \ tᶜ = t.ite s' s
rw₁ : s ∩ tᶜ ∪ s' \ tᶜ = s' ∩ t ∪ s \ t
rw₂ : s ∩ tᶜ ∪ s' ∩ t = s' ∩ t ∪ s \ t
rw₃ : s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s \ t
rw₄ rw₅ : s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s ∩ tᶜ
⊢ tᶜ.ite s s' = t.ite s' s

Tactic:
rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]

Premises used: Set.ite, Set.diff_eq, Set.union_comm, Set.diff_compl
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' : Set α
rw : tᶜ.ite s' s ∩ tᶜ = s' ∩ tᶜ
rw₁ rw₂ : s' ∩ tᶜ = s' ∩ tᶜ
⊢ t.ite s s' ∩ tᶜ = s' ∩ tᶜ

Tactic:
rw [← ite_compl, ite_inter_self]

Premises used: Set.ite_compl, Set.ite_inter_self
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' : Set α
⊢ t.ite s s' \ t = s' \ t

Tactic:
ite_inter_compl_self t s s'

Premises used: Set.Mem, Set.diff, setOf, Set.ite_inter_compl_self, Not
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s : Set α
⊢ t.ite s s = s

Tactic:
inter_union_diff _ _

Premises used: Set.ite, Set.inter_union_diff
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s t : Set α
⊢ s.ite s t = s ∪ t

Tactic:
simp [Set.ite]

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

Tactic:
simp [Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s s' : Set α
⊢ Set.ite ∅ s s' = s'

Tactic:
simp [Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
s s' : Set α
⊢ Set.ite univ s s' = s

Tactic:
simp [Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s : Set α
⊢ t.ite ∅ s = s \ t

Tactic:
simp [Set.ite]

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

Tactic:
simp [Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₁' s₂ s₂' : Set α
h : s₁ ⊆ s₂
h' : s₁' ⊆ s₂'
⊢ t.ite s₁ s₁' ⊆ t.ite s₂ s₂'

Tactic:
union_subset_union (inter_subset_inter_left _ h) (diff_subset_diff_left h')

Premises used: Set.ite, Set.union_subset_union, Set.diff_subset_diff_left, Set.inter_subset_inter_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' : Set α
⊢ t.ite s s' ⊆ s ∪ s'

Tactic:
union_subset_union inter_subset_left diff_subset

Premises used: Set.diff_subset, Set.ite, Set.union_subset_union, Set.inter_subset_left
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' : Set α
⊢ s ∩ s' ⊆ t.ite s s'

Tactic:
ite_same t (s ∩ s') ▸ ite_mono _ inter_subset_left inter_subset_right

Premises used: Eq.rec, Set.ite_same, Set.inter_subset_left, Inter.inter, Set.ite_mono, Set.inter_subset_right
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
h : ∀ (x : α), x ∈ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ t.ite s₁ s₁' ∩ t.ite s₂ s₂'
⊢ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Tactic:
ext x
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ s : Set α
rw : t.ite s₁ s₂ ∩ t.ite s s = t.ite s₁ s₂ ∩ s
rw₁ rw₂ : t.ite s₁ s₂ ∩ s = t.ite s₁ s₂ ∩ s
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

Tactic:
rw [ite_inter_inter, ite_same]

Premises used: Set.ite_same, Set.ite_inter_inter
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
rw : t.ite (s₁ ∩ s) (s₂ ∩ s) = s₁ ∩ s
rw₁ : t.ite (s₁ ∩ s) (s₁ ∩ s) = s₁ ∩ s
rw₂ rw₃ : s₁ ∩ s = s₁ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s

Tactic:
rw [← ite_inter, ← h, ite_same]

Premises used: Set.ite_same, Set.ite_inter
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' u : Set α
simp : (∀ (x : α), x ∈ u → x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
⊢ u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

Tactic:
simp only [subset_def, ← forall_and]

Premises used: Set.subset_def, forall_and
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' u : Set α
⊢ (∀ (x : α), x ∈ u → x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' u : Set α
refine : ∀ (x : α), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
⊢ (∀ (x : α), x ∈ u → x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
refine forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' u : Set α
x : α
pos : ∀ (hx : x ∈ t), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
neg : ∀ (hx : ¬x ∈ t), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
by_cases hx : x ∈ t
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' u : Set α
x : α
hx : x ∈ t
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
simp [*, Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s s' u : Set α
x : α
hx : ¬x ∈ t
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
simp [*, Set.ite]

Premises used: Set.ite
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₁ : ∀ (x : α), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
⊢ t.ite s₁ s₂ = s₁ ∪ s₂ \ t

Tactic:
ext x
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
pos : ∀ (hx : x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
neg : ∀ (hx : ¬x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
by_cases hx : x ∈ t
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
simp [*, Set.ite, or_iff_right_of_imp (@h x)]

Premises used: Set.ite, or_iff_right_of_imp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t

Tactic:
simp [*, Set.ite, or_iff_right_of_imp (@h x)]

Premises used: Set.ite, or_iff_right_of_imp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₁ : ∀ (x : α), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
⊢ t.ite s₁ s₂ = s₁ ∩ t ∪ s₂

Tactic:
ext x
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
pos : ∀ (hx : x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
neg : ∀ (hx : ¬x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

Tactic:
by_cases hx : x ∈ t
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
hx : x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

Tactic:
simp [*, Set.ite, or_iff_left_of_imp (@h x)]

Premises used: Set.ite, or_iff_left_of_imp
-- Module: Mathlib.Order.BooleanAlgebra.Set
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
hx : ¬x ∈ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

Tactic:
simp [*, Set.ite, or_iff_left_of_imp (@h x)]

Premises used: Set.ite, or_iff_left_of_imp
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : a ≤ sSup S
obtain : ∀ (C : Set α) (hC : ∀ x ∈ C, IsCompactElement x) (ha : sSup C ≤ sSup S), ∃ T ⊆ S, sSup C = sSup T
⊢ ∃ T ⊆ S, a = sSup T

Tactic:
obtain ⟨C, hC, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq a

Premises used: IsCompactlyGenerated.exists_sSup_eq, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
b : α
hb : IsCompactElement b
hbS : b ≤ sSup S
obtain : ∀ (s : Finset α) (hs₁ : (↑s : Set α) ⊆ S) (hs₂ : b ≤ s.sup id), ∃ T ⊆ S, b = sSup T
⊢ ∃ T ⊆ S, b = sSup T

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := (isCompactElement_iff_exists_le_sSup_of_le_sSup α b).1 hb S hbS

Premises used: Iff.mp, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
b : α
hb : IsCompactElement b
hbS : b ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
hs₂ : b ≤ s.sup id
obtain :
  ∀ (t : Finset α) (ht : t ⊆ s) (hb : IsCompactElement (t.sup id)) (hbS : t.sup id ≤ sSup S)
    (hs₂ : t.sup id ≤ s.sup id), ∃ T ⊆ S, t.sup id = sSup T
⊢ ∃ T ⊆ S, b = sSup T

Tactic:
obtain ⟨t, ht, rfl⟩ := hS.finitelyAtomistic s b hs₁ hb hs₂

Premises used: IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ∃ T ⊆ S, t.sup id = sSup T

Tactic:
⟨t, ?_, Finset.sup_id_eq_sSup t⟩

Premises used: SetLike.coe, And.intro, Exists.intro, Finset.sup_id_eq_sSup