awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
P : Prop
H₁ : x ∈ a ∪ b
H₂ : x ∈ a → P
H₃ : x ∈ b → P
⊢ P

Tactic:
Or.elim H₁ H₂ H₃

Premises used: Or.elim
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
⊢ x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b

Tactic:
Iff.rfl

Premises used: Set.union, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ a ∪ a = a

Tactic:
ext fun _ => or_self_iff

Premises used: Set.ext, or_self_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ a ∪ ∅ = a

Tactic:
ext fun _ => iff_of_eq (or_false _)

Premises used: Set.ext, Membership.mem, or_false, iff_of_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ ∅ ∪ a = a

Tactic:
ext fun _ => iff_of_eq (false_or _)

Premises used: Set.ext, Membership.mem, false_or, iff_of_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b : Set α
⊢ a ∪ b = b ∪ a

Tactic:
ext fun _ => or_comm

Premises used: Set.ext, or_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b c : Set α
⊢ a ∪ b ∪ c = a ∪ (b ∪ c)

Tactic:
ext fun _ => or_assoc

Premises used: Set.ext, or_assoc
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Associative fun (x1 x2 : Set α) ↦ x1 ∪ x2

Tactic:
⟨union_assoc⟩

Premises used: Std.Associative.mk, Set.union_assoc
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Commutative fun (x1 x2 : Set α) ↦ x1 ∪ x2

Tactic:
⟨union_comm⟩

Premises used: Set.union_comm, Std.Commutative.mk
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ s₃ : Set α
⊢ s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)

Tactic:
ext fun _ => or_left_comm

Premises used: Set.ext, or_left_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ s₃ : Set α
⊢ s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂

Tactic:
ext fun _ => or_right_comm

Premises used: Set.ext, or_right_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∪ t = s ↔ t ⊆ s

Tactic:
sup_eq_left

Premises used: sup_eq_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∪ t = t ↔ s ⊆ t

Tactic:
sup_eq_right

Premises used: sup_eq_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : s ⊆ t
⊢ s ∪ t = t

Tactic:
union_eq_right.mpr h

Premises used: Iff.mpr, Set.union_eq_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : t ⊆ s
⊢ s ∪ t = s

Tactic:
union_eq_left.mpr h

Premises used: Iff.mpr, Set.union_eq_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊆ s ∪ t

Tactic:
fun _ => Or.inl

Premises used: Set.union, Set.Mem, setOf, Set.Subset, Or.inl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ t ⊆ s ∪ t

Tactic:
fun _ => Or.inr

Premises used: Set.union, Set.Mem, setOf, Set.Subset, Or.inr
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t r : Set α
sr : s ⊆ r
tr : t ⊆ r
⊢ s ∪ t ⊆ r

Tactic:
fun _ =>
  Or.rec (@sr _) (@tr _)

Premises used: Set.union, Or.rec, Set.Mem, setOf, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

Tactic:
(forall_congr' fun _ => or_imp).trans forall_and

Premises used: Set.union, Set.Mem, setOf, or_imp, Set.Subset, forall_congr', Iff.trans, forall_and
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ t₁ t₂ : Set α
h₁ : s₁ ⊆ s₂
h₂ : t₁ ⊆ t₂
⊢ s₁ ∪ t₁ ⊆ s₂ ∪ t₂

Tactic:
fun _ => Or.imp (@h₁ _) (@h₂ _)

Premises used: Set.union, Set.Mem, setOf, Set.Subset, Or.imp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ t : Set α
h : s₁ ⊆ s₂
⊢ s₁ ∪ t ⊆ s₂ ∪ t

Tactic:
union_subset_union h Subset.rfl

Premises used: Set.union_subset_union, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t₁ t₂ : Set α
h : t₁ ⊆ t₂
⊢ s ∪ t₁ ⊆ s ∪ t₂

Tactic:
union_subset_union Subset.rfl h

Premises used: Set.union_subset_union, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : s ⊆ t
u : Set α
⊢ s ⊆ t ∪ u

Tactic:
h.trans subset_union_left

Premises used: HasSubset.Subset.trans, Set.subset_union_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s u : Set α
h : s ⊆ u
t : Set α
⊢ s ⊆ t ∪ u

Tactic:
h.trans subset_union_right

Premises used: Set.subset_union_right, HasSubset.Subset.trans
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
ht : t ⊆ s ∪ u
hu : u ⊆ s ∪ t
⊢ s ∪ t = s ∪ u

Tactic:
sup_congr_left ht hu

Premises used: sup_congr_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
hs : s ⊆ t ∪ u
ht : t ⊆ s ∪ u
⊢ s ∪ u = t ∪ u

Tactic:
sup_congr_right hs ht

Premises used: sup_congr_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t

Tactic:
sup_eq_sup_iff_left

Premises used: sup_eq_sup_iff_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u

Tactic:
sup_eq_sup_iff_right

Premises used: sup_eq_sup_iff_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
simp : s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
simp only [← subset_empty_iff]

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅

Tactic:
union_subset_iff

Premises used: Set.union_subset_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅

Tactic:
exact union_subset_iff

Premises used: Set.union_subset_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s ∪ univ = univ

Tactic:
sup_top_eq _

Premises used: sup_top_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ univ ∪ s = univ

Tactic:
top_sup_eq _

Premises used: top_sup_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊂ s ∪ t ↔ ¬t ⊆ s

Tactic:
left_lt_sup

Premises used: left_lt_sup
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ t ⊂ s ∪ t ↔ ¬s ⊆ t

Tactic:
right_lt_sup

Premises used: right_lt_sup
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ = {a : α | a ∈ s₁ ∧ a ∈ s₂}

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
⊢ x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
ha : x ∈ a
hb : x ∈ b
⊢ x ∈ a ∩ b

Tactic:
⟨ha, hb⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
h : x ∈ a ∩ b
⊢ x ∈ a

Tactic:
h.left

Premises used: And.left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
h : x ∈ a ∩ b
⊢ x ∈ b

Tactic:
h.right

Premises used: And.right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ a ∩ a = a

Tactic:
ext fun _ => and_self_iff

Premises used: Set.ext, and_self_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ a ∩ ∅ = ∅

Tactic:
ext fun _ => iff_of_eq (and_false _)

Premises used: Set.ext, Membership.mem, and_false, iff_of_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ ∅ ∩ a = ∅

Tactic:
ext fun _ => iff_of_eq (false_and _)

Premises used: Set.ext, false_and, Membership.mem, iff_of_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b : Set α
⊢ a ∩ b = b ∩ a

Tactic:
ext fun _ => and_comm

Premises used: Set.ext, and_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b c : Set α
⊢ a ∩ b ∩ c = a ∩ (b ∩ c)

Tactic:
ext fun _ => and_assoc

Premises used: Set.ext, and_assoc
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Associative fun (x1 x2 : Set α) ↦ x1 ∩ x2

Tactic:
⟨inter_assoc⟩

Premises used: Std.Associative.mk, Set.inter_assoc
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Commutative fun (x1 x2 : Set α) ↦ x1 ∩ x2

Tactic:
⟨inter_comm⟩

Premises used: Set.inter_comm, Std.Commutative.mk
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ s₃ : Set α
⊢ s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

Tactic:
ext fun _ => and_left_comm

Premises used: Set.ext, and_left_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ s₃ : Set α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Tactic:
ext fun _ => and_right_comm

Premises used: Set.ext, and_right_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∩ t ⊆ s

Tactic:
fun _ => And.left

Premises used: Set.Mem, setOf, Set.inter, Set.Subset, And.left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∩ t ⊆ t

Tactic:
fun _ => And.right

Premises used: Set.Mem, setOf, Set.inter, Set.Subset, And.right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t r : Set α
rs : r ⊆ s
rt : r ⊆ t
⊢ r ⊆ s ∩ t

Tactic:
fun _ h =>
  ⟨rs h, rt h⟩

Premises used: Set.Mem, setOf, Set.inter, Set.Subset, And.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t r : Set α
⊢ r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t

Tactic:
(forall_congr' fun _ => imp_and).trans forall_and

Premises used: imp_and, Set.Mem, setOf, Set.inter, Set.Subset, forall_congr', Iff.trans, forall_and
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∩ t = s ↔ s ⊆ t

Tactic:
inf_eq_left

Premises used: inf_eq_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∩ t = t ↔ t ⊆ s

Tactic:
inf_eq_right

Premises used: inf_eq_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s = s ∩ t ↔ s ⊆ t

Tactic:
left_eq_inf

Premises used: left_eq_inf
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ t = s ∩ t ↔ t ⊆ s

Tactic:
right_eq_inf

Premises used: right_eq_inf
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊆ t → s ∩ t = s

Tactic:
inter_eq_left.mpr

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ t ⊆ s → s ∩ t = t

Tactic:
inter_eq_right.mpr

Premises used: Iff.mpr, Set.inter_eq_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
ht : s ∩ u ⊆ t
hu : s ∩ t ⊆ u
⊢ s ∩ t = s ∩ u

Tactic:
inf_congr_left ht hu

Premises used: inf_congr_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
hs : t ∩ u ⊆ s
ht : s ∩ u ⊆ t
⊢ s ∩ u = t ∩ u

Tactic:
inf_congr_right hs ht

Premises used: inf_congr_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u

Tactic:
inf_eq_inf_iff_left

Premises used: inf_eq_inf_iff_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t

Tactic:
inf_eq_inf_iff_right

Premises used: inf_eq_inf_iff_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ a ∩ univ = a

Tactic:
inf_top_eq _

Premises used: inf_top_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ univ ∩ a = a

Tactic:
top_inf_eq _

Premises used: top_inf_eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ t₁ t₂ : Set α
h₁ : s₁ ⊆ t₁
h₂ : s₂ ⊆ t₂
⊢ s₁ ∩ s₂ ⊆ t₁ ∩ t₂

Tactic:
fun _ => And.imp (@h₁ _) (@h₂ _)

Premises used: And.imp, Set.Mem, setOf, Set.inter, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
H : s ⊆ t
⊢ s ∩ u ⊆ t ∩ u

Tactic:
inter_subset_inter H Subset.rfl

Premises used: Set.inter_subset_inter, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
H : s ⊆ t
⊢ u ∩ s ⊆ u ∩ t

Tactic:
inter_subset_inter Subset.rfl H

Premises used: Set.inter_subset_inter, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∪ t) ∩ s = s

Tactic:
inter_eq_self_of_subset_right subset_union_left

Premises used: Set.subset_union_left, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∪ t) ∩ t = t

Tactic:
inter_eq_self_of_subset_right subset_union_right

Premises used: Set.subset_union_right, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
⊢ s ∩ {a : α | p a} = {a : α | a ∈ s ∧ p a}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
s : Set α
⊢ {a : α | p a} ∩ s = {a : α | a ∈ s ∧ p a}

Tactic:
inter_comm _ _

Premises used: Set.Mem, setOf, Set.inter, Set.inter_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
rw : s ∩ {a : α | p a} = s ∩ {x : α | x ∈ t ∧ p x}
rw₁ : s ∩ {a : α | p a} = s ∩ (t ∩ {a : α | p a})
rw₂ : s ∩ {a : α | p a} = s ∩ t ∩ {a : α | p a}
rw₃ rw₄ : s ∩ {a : α | p a} = s ∩ {a : α | p a}
⊢ {x : α | x ∈ s ∧ p x} = s ∩ {x : α | x ∈ t ∧ p x}

Tactic:
rw [← inter_setOf_eq_sep s p, ← inter_setOf_eq_sep t p,
    ← inter_assoc, ← left_eq_inter.mpr hst]

Premises used: Iff.mpr, Set.left_eq_inter, Set.inter_setOf_eq_sep, Set.inter_assoc
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∩ t ⊂ t ↔ ¬t ⊆ s

Tactic:
inf_lt_right

Premises used: inf_lt_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ∩ t ⊂ s ↔ ¬s ⊆ t

Tactic:
inf_lt_left

Premises used: inf_lt_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Tactic:
inf_sup_left _ _ _

Premises used: inf_sup_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Tactic:
inf_sup_right _ _ _

Premises used: inf_sup_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

Tactic:
sup_inf_left _ _ _

Premises used: sup_inf_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

Tactic:
sup_inf_right _ _ _

Premises used: sup_inf_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

Tactic:
sup_sup_distrib_left _ _ _

Premises used: sup_sup_distrib_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

Tactic:
sup_sup_distrib_right _ _ _

Premises used: sup_sup_distrib_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

Tactic:
inf_inf_distrib_left _ _ _

Premises used: inf_inf_distrib_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u : Set α
⊢ s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

Tactic:
inf_inf_distrib_right _ _ _

Premises used: inf_inf_distrib_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u v : Set α
⊢ s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

Tactic:
sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t u v : Set α
⊢ s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

Tactic:
inf_inf_inf_comm _ _ _ _

Premises used: inf_inf_inf_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
x : α
xs : x ∈ s
px : p x
⊢ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x

Tactic:
⟨xs, px⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ {x : α | x ∈ s ∧ x ∈ t} = s ∩ t

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
x : α
⊢ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ x ∈ s ∧ p x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p q : α → Prop
simp_rw :
  (∀ (x : α),
      Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) {x : α | x ∈ s ∧ q x} x) ↔
    ∀ (x : α), x ∈ s → (p x ↔ q x)
simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ s ∧ q x) ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} {x : α | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, Set.mem_sep_iff, Set.ext_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : s ⊆ t
⊢ {x : α | x ∈ t ∧ x ∈ s} = s

Tactic:
inter_eq_self_of_subset_right h

Premises used: setOf, Set.inter, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
⊢ {x : α | x ∈ s ∧ p x} ⊆ s

Tactic:
fun _ => And.left

Premises used: Set.Mem, setOf, Set.Subset, And.left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
⊢ Subset.{u} (α := Set α) {x : α | x ∈ s ∧ p x} {x : α | p x}

Tactic:
fun _ => And.right

Premises used: Set.Mem, setOf, Set.Subset, And.right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
simp_rw : (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x
simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x
⊢ {x : α | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]

Premises used: Set.mem_sep_iff, Set.ext_iff, and_iff_left_iff_imp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : α → Prop
simp_rw :
  (∀ (x : α), Membership.mem (γ := Set α) {x : α | x ∈ s ∧ p x} x ↔ Membership.mem (γ := Set α) ∅ x) ↔
    ∀ (x : α), x ∈ s → ¬p x
simp_rw₁ : (∀ (x : α), x ∈ s ∧ p x ↔ Membership.mem (γ := Set α) ∅ x) ↔ ∀ (x : α), x ∈ s → ¬p x
simp_rw₂ : (∀ (x : α), x ∈ s ∧ p x ↔ False) ↔ ∀ (x : α), x ∈ s → ¬p x
simp_rw₃ : (∀ (x : α), ¬(x ∈ s ∧ p x)) ↔ ∀ (x : α), x ∈ s → ¬p x
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x} ∅ ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]

Premises used: iff_false, Set.mem_sep_iff, Set.mem_empty_iff_false, Set.ext_iff, not_and
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ {x : α | x ∈ s ∧ True} = s

Tactic:
inter_univ s

Premises used: Set.Mem, Set.univ, Set.inter_univ, setOf, Set.inter
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ False} ∅

Tactic:
inter_empty s

Premises used: Set.Mem, setOf, Set.inter, Set.inter_empty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | Membership.mem (γ := Set α) ∅ x ∧ p x} ∅

Tactic:
empty_inter {x | p x}

Premises used: Set.Mem, setOf, Set.empty_inter, Set.inter
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | Membership.mem (γ := Set α) univ x ∧ p x} {x : α | p x}

Tactic:
univ_inter {x | p x}

Premises used: Set.Mem, setOf, Set.inter, Set.univ_inter
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
p : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | (x ∈ s ∨ x ∈ t) ∧ p x} ({x : α | x ∈ s ∧ p x} ∪ {x : α | x ∈ t ∧ p x})

Tactic:
union_inter_distrib_right { x | x ∈ s } { x | x ∈ t } {x | p x}

Premises used: Set.union, Set.Mem, setOf, Membership.mem, Set.inter, Set.union_inter_distrib_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
p : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | (x ∈ s ∧ x ∈ t) ∧ p x} ({x : α | x ∈ s ∧ p x} ∩ {x : α | x ∈ t ∧ p x})

Tactic:
inter_inter_distrib_right s t {x | p x}

Premises used: Set.inter_inter_distrib_right, Set.Mem, setOf, Set.inter
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p q : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ p x ∧ q x} ({x : α | x ∈ s ∧ p x} ∩ {x : α | x ∈ s ∧ q x})

Tactic:
inter_inter_distrib_left s {x | p x} {x | q x}

Premises used: Set.Mem, setOf, Set.inter, Set.inter_inter_distrib_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p q : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | x ∈ s ∧ (p x ∨ q x)} ({x : α | x ∈ s ∧ p x} ∪ {x : α | x ∈ s ∧ q x})

Tactic:
inter_union_distrib_left s {x | p x} {x | q x}

Premises used: Set.union, Set.Mem, setOf, Set.inter, Set.inter_union_distrib_left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p q : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | Membership.mem (γ := Set α) {y : α | p y} x ∧ q x} {x : α | p x ∧ q x}

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x s : Set α
h : x ⊆ s
⊢ x ∈ 𝒫 s

Tactic:
@h

Premises used: Set.Mem, setOf, Set.powerset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x s : Set α
h : x ∈ 𝒫 s
⊢ x ⊆ s

Tactic:
@h

Premises used: Set.Mem, setOf, Set.powerset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x s : Set α
⊢ x ∈ 𝒫 s ↔ x ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.powerset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ 𝒫 (s ∩ t) = 𝒫 s ∩ 𝒫 t

Tactic:
ext fun _ => subset_inter_iff

Premises used: Set.ext, Set.subset_inter_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ 𝒫 s ⊆ 𝒫 t ↔ s ⊆ t

Tactic:
⟨fun h => @h _ (fun _ h => h), fun h _ hu _ ha => h (hu ha)⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Monotone.{u, u} (α := Set α) powerset

Tactic:
fun _ _ => powerset_mono.2

Premises used: Iff.mpr, Monotone, Set.powerset_mono
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ (𝒫 s).Nonempty

Tactic:
⟨∅, fun _ h => empty_subset s h⟩

Premises used: Set.Nonempty, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq (α := Set (Set α)) (𝒫 ∅) {∅}

Tactic:
ext fun _ => subset_empty_iff

Premises used: Set.ext, Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set (Set α)) (𝒫 univ) univ

Tactic:
eq_univ_of_forall subset_univ

Premises used: Set.subset_univ, Set.eq_univ_of_forall
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : p → Set α
x : α
⊢ Membership.mem (γ := Set α) (if h : p then t h else univ) x ↔ ∀ (h : p), x ∈ t h

Tactic:
simp [mem_dite]

Premises used: mem_dite
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : Set α
x : α
⊢ (x ∈ if p then t else univ) ↔ p → x ∈ t

Tactic:
mem_dite_univ_right p (fun _ => t) x

Premises used: Set.Mem, Set.mem_dite_univ_right, ite
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
pos : p → (Membership.mem (γ := Set α) univ x ↔ ∀ (h : ¬p), x ∈ t h)
neg : ∀ (h : ¬p), x ∈ t h ↔ ∀ (h : ¬p), x ∈ t h
⊢ Membership.mem (γ := Set α) (if h : p then univ else t h) x ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
split_ifs
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
h : p
⊢ Membership.mem (γ := Set α) univ x ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
h : ¬p
⊢ x ∈ t h ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : Set α
x : α
⊢ (x ∈ if p then univ else t) ↔ ¬p → x ∈ t

Tactic:
mem_dite_univ_left p (fun _ => t) x

Premises used: Set.Mem, Set.mem_dite_univ_left, ite
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : p → Set α
x : α
simp : (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ (h : p), x ∈ t h
⊢ Membership.mem (γ := Set α) (if h : p then t h else ∅) x ↔ ∃ (h : p), x ∈ t h

Tactic:
simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]

Premises used: mem_dite, Classical.not_not, imp_false, Set.mem_empty_iff_false
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ (h : p), x ∈ t h

Tactic:
⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩

Premises used: And, And.right, And.left, And.intro, Iff.intro, Exists.intro, _private.0.Set.mem_dite_empty_right.match_2
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ (h : p), x ∈ t h

Tactic:
exact ⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : Set α
x : α
⊢ (∃ (h : p), x ∈ t) ↔ p ∧ x ∈ t

Tactic:
simp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
simp : (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h
⊢ Membership.mem (γ := Set α) (if h : p then ∅ else t h) x ↔ ∃ (h : ¬p), x ∈ t h

Tactic:
simp only [mem_dite, mem_empty_iff_false, imp_false]

Premises used: mem_dite, imp_false, Set.mem_empty_iff_false