awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Basic
Goal:
α_1 : Type u
s_1 t : Set α_1
ι : Type u
α : ι → Type v
inst : ∀ (i : ι), Nonempty.{v + 1} (α i)
s : Set ι
⊢ CanLift ((i : (↑s : Type u)) → α (↑i : ι)) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : (↑s : Type u)) ↦ f (↑i : ι))
    fun (x : (i : (↑s : Type u)) → α (↑i : ι)) ↦ True

Tactic:
PiSubtype.canLift ι α (· ∈ s)

Premises used: Membership.mem, PiSubtype.canLift
-- Module: Mathlib.Data.Set.Basic
Goal:
α_1 : Type u
s_1 t : Set α_1
ι : Type u
α : Type v
inst : Nonempty α
s : Set ι
⊢ CanLift ((↑s : Type u) → α) (ι → α) (fun (f : ι → α) (i : (↑s : Type u)) ↦ f (↑i : ι)) fun (x : (↑s : Type u) → α) ↦
    True

Tactic:
PiSetCoe.canLift ι (fun _ => α) s

Premises used: Set.PiSetCoe.canLift
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ (↑s : Type u) = { x : α // x ∈ s }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
⊢ (↑{x : α | p x} : Type u) = { x : α // p x }

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : (↑s : Type u) → Prop
⊢ (∀ (x : (↑s : Type u)), p x) ↔ ∀ (x : α) (h : x ∈ s), p (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)

Tactic:
Subtype.forall

Premises used: Subtype.forall
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : (↑s : Type u) → Prop
⊢ (∃ (x : (↑s : Type u)), p x) ↔ ∃ (x : α), ∃ (h : x ∈ s), p (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)

Tactic:
Subtype.exists

Premises used: Subtype.exists
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : (x : α) → x ∈ s → Prop
⊢ (∃ (x : α), ∃ (h : x ∈ s), p x h) ↔ ∃ (x : (↑s : Type u)), p (↑x : α) ⋯

Tactic:
(@SetCoe.exists _ _ fun x => p x.1 x.2).symm

Premises used: SetCoe.exists, Iff.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
p : (x : α) → x ∈ s → Prop
⊢ (∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : (↑s : Type u)), p (↑x : α) ⋯

Tactic:
(@SetCoe.forall _ _ fun x => p x.1 x.2).symm

Premises used: SetCoe.forall, Iff.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
a b : (↑s : Type u)
⊢ (↑a : α) = (↑b : α) → a = b

Tactic:
Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
a b : (↑s : Type u)
⊢ (↑a : α) = (↑b : α) ↔ a = b

Tactic:
Iff.intro SetCoe.ext fun h => h ▸ rfl

Premises used: SetCoe.ext, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s : Set α
p : (↑s : Type u_1)
⊢ (↑p : α) ∈ s

Tactic:
p.prop

Premises used: Subtype.prop
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
s t : Set α
hx : x ∈ s
h : s ⊆ t
⊢ x ∈ t

Tactic:
h hx
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Injective.{u + 1, u + 1} (α := α → Prop) setOf

Tactic:
injective_id

Premises used: setOf, Function.injective_id, Set
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p q : α → Prop
⊢ Eq.{u + 1} (α := Set α) {x : α | p x} {x : α | q x} ↔ p = q

Tactic:
Iff.rfl

Premises used: Iff.rfl, setOf, Set
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Bijective.{u + 1, u + 1} (α := α → Prop) setOf

Tactic:
bijective_id

Premises used: Function.bijective_id, setOf, Set
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
s : Set α
⊢ s ⊆ setOf p ↔ ∀ (x : α), x ∈ s → p x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
s : Set α
⊢ setOf p ⊆ s ↔ ∀ (x : α), p x → x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p q : α → Prop
⊢ Subset.{u} (α := Set α) {a : α | p a} {a : α | q a} ↔ ∀ (a : α), p a → q a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p q : α → Prop
⊢ Eq.{u + 1} (α := Set α) {a : α | p a ∧ q a} ({a : α | p a} ∩ {a : α | q a})

Tactic:
rfl

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

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Refl fun (x1 x2 : Set α) ↦ x1 ≤ x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsTrans.{u + 1} (Set α) fun (x1 x2 : Set α) ↦ x1 ≤ x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun (x1 x2 : Set α) ↦ x1 ≤ x2) (fun (x1 x2 : Set α) ↦ x1 ≤ x2) fun (x1 x2 : Set α) ↦ x1 ≤ x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Antisymm fun (x1 x2 : Set α) ↦ x1 ≤ x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Irrefl fun (x1 x2 : Set α) ↦ x1 < x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsTrans.{u + 1} (Set α) fun (x1 x2 : Set α) ↦ x1 < x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun (x1 x2 : Set α) ↦ x1 < x2) (fun (x1 x2 : Set α) ↦ x1 < x2) fun (x1 x2 : Set α) ↦ x1 < x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun (x1 x2 : Set α) ↦ x1 < x2) (fun (x1 x2 : Set α) ↦ x1 ≤ x2) fun (x1 x2 : Set α) ↦ x1 < x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun (x1 x2 : Set α) ↦ x1 ≤ x2) (fun (x1 x2 : Set α) ↦ x1 < x2) fun (x1 x2 : Set α) ↦ x1 < x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Std.Asymm fun (x1 x2 : Set α) ↦ x1 < x2

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsNonstrictStrictOrder.{u} (Set α) (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) fun (x1 x2 : Set α) ↦ x1 ⊂ x2

Tactic:
⟨fun _ _ => Iff.rfl⟩

Premises used: Iff.rfl, IsNonstrictStrictOrder.mk
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ⊆ t) = ∀ (x : α), x ∈ s → x ∈ t

Tactic:
rfl

Premises used: Set.Subset, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ⊂ t) = (s ⊆ t ∧ ¬t ⊆ s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : Set α
⊢ a ⊆ a

Tactic:
fun _ => id

Premises used: id, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s ⊆ s

Tactic:
Subset.refl s

Premises used: Set.Subset.refl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b c : Set α
ab : a ⊆ b
bc : b ⊆ c
⊢ a ⊆ c

Tactic:
fun _ h => bc <| ab h

Premises used: Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x y : α
s : Set α
hx : x = y
h : y ∈ s
⊢ x ∈ s

Tactic:
hx.symm ▸ h

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b : Set α
h₁ : a ⊆ b
h₂ : b ⊆ a
⊢ a = b

Tactic:
Set.ext fun _ => ⟨@h₁ _, @h₂ _⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b : Set α
⊢ a = b ↔ a ⊆ b ∧ b ⊆ a

Tactic:
⟨fun e => ⟨e.subset, e.symm.subset⟩, fun ⟨h₁, h₂⟩ => Subset.antisymm h₁ h₂⟩

Premises used: Set.Subset.antisymm, _private.0.Set.Subset.antisymm_iff.match_1, Eq.subset, And.intro, Iff.intro, Eq.symm, Eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a b : Set α
⊢ a ⊆ b → b ⊆ a → a = b

Tactic:
Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ : Set α
a : α
h : s₁ ⊆ s₂
⊢ a ∈ s₁ → a ∈ s₂

Tactic:
@h _
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : α
s t : Set α
h : s ⊆ t
⊢ ¬a ∈ t → ¬a ∈ s

Tactic:
mt <| mem_of_subset_of_mem h

Premises used: Set.mem_of_subset_of_mem, mt
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
simp only [subset_def, not_imp_not]

Premises used: Set.subset_def, not_imp_not
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ (a : α), a ∈ s ∧ ¬a ∈ t

Tactic:
simp only [subset_def, not_forall, exists_prop]

Premises used: Set.subset_def, exists_prop, Classical.not_forall
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ ¬univ ⊆ s ↔ ∃ (a : α), ¬a ∈ s

Tactic:
simp [not_subset]

Premises used: Set.not_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ ¬⊤ ⊆ s ↔ ∃ (a : α), ¬a ∈ s

Tactic:
not_univ_subset

Premises used: Set.not_univ_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : ∀ (u : Set α), s ⊆ u ↔ t ⊆ u
⊢ s = t

Tactic:
eq_of_forall_ge_iff h

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

Tactic:
eq_or_lt_of_le h

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : s ⊂ t
⊢ ∃ (x : α), x ∈ t ∧ ¬x ∈ s

Tactic:
not_subset.1 h.2

Premises used: And.right, Set.not_subset, Iff.mp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊂ t ↔ s ⊆ t ∧ s ≠ t

Tactic:
@lt_iff_le_and_ne (Set α) _ s t

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : s ⊆ t
⊢ s ⊂ t ↔ ∃ (x : α), x ∈ t ∧ ¬x ∈ s

Tactic:
⟨exists_of_ssubset, fun ⟨_, hxt, hxs⟩ => ⟨h, fun h => hxs <| h hxt⟩⟩

Premises used: _private.0.Set.ssubset_iff_of_subset.match_1, Set.exists_of_ssubset, HasSSubset.SSubset, And.intro, Iff.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ⊂ t ↔ s ⊆ t ∧ ∃ (x : α), x ∈ t ∧ ¬x ∈ s

Tactic:
⟨fun h ↦ ⟨h.le, Set.exists_of_ssubset h⟩, fun ⟨h1, h2⟩ ↦ (Set.ssubset_iff_of_subset h1).mpr h2⟩

Premises used: Iff.mpr, Set.exists_of_ssubset, HasSSubset.SSubset, LT.lt.le, _private.0.Set.ssubset_iff_exists.match_1, And.intro, Iff.intro, Set.ssubset_iff_of_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ s₃ : Set α
hs₁s₂ : s₁ ⊂ s₂
hs₂s₃ : s₂ ⊆ s₃
⊢ s₁ ⊂ s₃

Tactic:
⟨Subset.trans hs₁s₂.1 hs₂s₃, fun hs₃s₁ => hs₁s₂.2 (Subset.trans hs₂s₃ hs₃s₁)⟩

Premises used: Set.Subset.trans, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ s₃ : Set α
hs₁s₂ : s₁ ⊆ s₂
hs₂s₃ : s₂ ⊂ s₃
⊢ s₁ ⊂ s₃

Tactic:
⟨Subset.trans hs₁s₂ hs₂s₃.1, fun hs₃s₁ => hs₂s₃.2 (Subset.trans hs₃s₁ hs₁s₂)⟩

Premises used: Set.Subset.trans, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
⊢ ¬Membership.mem (γ := Set α) ∅ x

Tactic:
id

Premises used: Set.Mem, id, Not
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
a : α
s : Set α
⊢ ¬¬a ∈ s ↔ a ∈ s

Tactic:
not_not

Premises used: Classical.not_not
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty

Tactic:
nonempty_subtype

Premises used: Set.Nonempty, nonempty_subtype
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s.Nonempty ↔ ∃ (x : α), x ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
x : α
h : x ∈ s
⊢ s.Nonempty

Tactic:
⟨x, h⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
h : s.Nonempty
⊢ h.some (s := s) ∈ s

Tactic:
Classical.choose_spec h

Premises used: Set.Mem, Classical.choose_spec, Set.Nonempty.some
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
ht : s ⊆ t
hs : s.Nonempty
⊢ t.Nonempty

Tactic:
hs.imp ht

Premises used: Exists.imp, Set.Nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : ¬s ⊆ t
⊢ (s \ t).Nonempty

Tactic:
let ⟨x, xs, xt⟩ := not_subset.1 h
  ⟨x, xs, xt⟩

Premises used: SDiff.sdiff, Set.Nonempty, _private.0.Set.nonempty_of_not_subset.match_1, And.intro, Set.not_subset, Exists.intro, Iff.mp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
ht : s ⊂ t
⊢ (t \ s).Nonempty

Tactic:
nonempty_of_not_subset ht.2

Premises used: And.right, Set.nonempty_of_not_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : (s \ t).Nonempty
⊢ s.Nonempty

Tactic:
h.imp fun _ => And.left

Premises used: Exists.imp, Set.Nonempty, And.left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
ht : s ⊂ t
⊢ t.Nonempty

Tactic:
(nonempty_of_ssubset ht).of_diff

Premises used: Set.nonempty_of_ssubset, Set.Nonempty.of_diff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
hs : s.Nonempty
⊢ (s ∪ t).Nonempty

Tactic:
hs.imp fun _ => Or.inl

Premises used: Exists.imp, Set.Nonempty, Or.inl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
ht : t.Nonempty
⊢ (s ∪ t).Nonempty

Tactic:
ht.imp fun _ => Or.inr

Premises used: Exists.imp, Set.Nonempty, Or.inr
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty

Tactic:
exists_or

Premises used: exists_or, Set.union, Set.Mem, setOf, Set.Nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : (s ∩ t).Nonempty
⊢ s.Nonempty

Tactic:
h.imp fun _ => And.left

Premises used: Exists.imp, Set.Nonempty, And.left
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : (s ∩ t).Nonempty
⊢ t.Nonempty

Tactic:
h.imp fun _ => And.right

Premises used: Exists.imp, Set.Nonempty, And.right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ (x : α), x ∈ s ∧ x ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.Nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ (x : α), x ∈ s ∧ x ∈ t

Tactic:
simp_rw [inter_nonempty]

Premises used: Set.inter_nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Nonempty α ↔ Set.Nonempty.{u} (α := α) univ

Tactic:
⟨fun ⟨x⟩ => ⟨x, trivial⟩, fun ⟨x, _⟩ => ⟨x⟩⟩

Premises used: trivial, Set.univ, Nonempty.intro, _private.0.Set.nonempty_iff_univ_nonempty.match_2, Set.Nonempty, Iff.intro, _private.0.Set.nonempty_iff_univ_nonempty.match_1, Exists.intro, Nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s.Nonempty → Nonempty.{u + 1} (↑s : Type u)

Tactic:
nonempty_subtype.2

Premises used: Iff.mpr, Set.Nonempty, nonempty_subtype
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s.Nonempty → Nonempty α

Tactic:
fun ⟨x, _⟩ => ⟨x⟩

Premises used: _private.0.Set.Nonempty.to_type.match_1, Nonempty.intro, Nonempty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst : Nonempty α
⊢ Nonempty.{u + 1} (↑univ : Type u)

Tactic:
Set.univ_nonempty.to_subtype

Premises used: Set.univ_nonempty, Set.Nonempty.to_subtype
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst : Nonempty α
⊢ Nonempty.{u + 1} (↑⊤ : Type u)

Tactic:
inferInstanceAs (Nonempty (univ : Set α))

Premises used: _private.0.Set.instNonemptyTop._proof_1
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
inst : Nonempty.{u + 1} (↑s : Type u)
⊢ s.Nonempty

Tactic:
nonempty_subtype.mp ‹_›

Premises used: Set.Nonempty, nonempty_subtype, Iff.mp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) ∅ {_x : α | False}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
⊢ Membership.mem (γ := Set α) ∅ x ↔ False

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) {_a : α | False} ∅

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) {_x : α | ⊥} ∅

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ ∅ ⊆ s

Tactic:
nofun

Premises used: Membership.mem, Set.Subset, _private.0.Set.empty_subset.match_1
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s ⊆ ∅ ↔ s = ∅

Tactic:
(Subset.antisymm_iff.trans <| and_iff_left (empty_subset _)).symm

Premises used: and_iff_left, Set.Subset.antisymm_iff, Set.empty_subset, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s = ∅ ↔ ∀ (x : α), ¬x ∈ s

Tactic:
subset_empty_iff.symm

Premises used: Set.Mem, Set.Subset, Set.subset_empty_iff, Not, Iff.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
h : ∀ (x : α), ¬x ∈ s
⊢ s = ∅

Tactic:
subset_empty_iff.1 h

Premises used: Iff.mp, Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s ⊆ ∅ → s = ∅

Tactic:
subset_empty_iff.1

Premises used: Iff.mp, Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ ¬s.Nonempty ↔ s = ∅

Tactic:
simp only [Set.Nonempty, not_exists, eq_empty_iff_forall_notMem]

Premises used: not_exists, Set.Nonempty, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s.Nonempty ↔ s ≠ ∅

Tactic:
not_nonempty_iff_eq_empty.not_right

Premises used: Set.not_nonempty_iff_eq_empty, Iff.not_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s.Nonempty ↔ ∅ ≠ s

Tactic:
nonempty_iff_ne_empty.trans ne_comm

Premises used: Set.nonempty_iff_ne_empty, Iff.trans, ne_comm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
rw : (¬∃ (a : α), a ∈ s) ↔ s = ∅
rw₁ : (∀ (x : α), ¬x ∈ s) ↔ s = ∅
rw₂ rw₃ : (∀ (x : α), ¬x ∈ s) ↔ ∀ (x : α), ¬x ∈ s
⊢ ¬Nonempty.{u + 1} (↑s : Type u) ↔ s = ∅

Tactic:
rw [nonempty_subtype, not_exists, eq_empty_iff_forall_notMem]

Premises used: not_exists, nonempty_subtype, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ Nonempty.{u + 1} (↑s : Type u) ↔ s ≠ ∅

Tactic:
not_nonempty_iff_eq_empty'.not_right

Premises used: Set.not_nonempty_iff_eq_empty', Iff.not_right
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ ¬Set.Nonempty.{u} (α := α) ∅

Tactic:
fun ⟨_, hx⟩ => hx

Premises used: False, _private.0.Set.not_nonempty_empty.match_1, Not
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ ¬IsEmpty.{u + 1} (↑s : Type u) ↔ ¬s = ∅

Tactic:
simpa using nonempty_iff_ne_empty

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
inst simpa : IsEmpty.{u + 1} (↑s : Type u)
⊢ s = ∅

Tactic:
simpa using ‹IsEmpty s›

Premises used: Set.Elem, IsEmpty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s = ∅ ∨ s.Nonempty

Tactic:
or_iff_not_imp_left.2 nonempty_iff_ne_empty.2

Premises used: Iff.mpr, Classical.or_iff_not_imp_left, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
h : t ⊆ s
e : s = ∅
⊢ t = ∅

Tactic:
subset_empty_iff.1 <| e ▸ h

Premises used: Eq.rec, Iff.mp, Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : α → Prop
⊢ (∀ (x : α), Membership.mem (γ := Set α) ∅ x → p x) ↔ True

Tactic:
iff_true_intro fun _ => False.elim

Premises used: False.elim, iff_true_intro
-- Module: Mathlib.Data.Set.Basic
Goal:
α_1 : Type u
β : Type v
a b : α_1
s s₁ s₂ t t₁ t₂ u : Set α_1
α : Type u
⊢ IsEmpty.{u + 1} (↑∅ : Type u)

Tactic:
⟨fun x => x.2⟩

Premises used: IsEmpty.mk, Subtype.property
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ ∅ ⊂ s ↔ s.Nonempty

Tactic:
(@bot_lt_iff_ne_bot (Set α) _ _ _).trans nonempty_iff_ne_empty.symm

Premises used: bot_lt_iff_ne_bot, Set.nonempty_iff_ne_empty, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) {_x : α | True} univ

Tactic:
rfl

Premises used: Set.univ, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) {_x : α | ⊤} univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) univ ∅ ↔ IsEmpty α

Tactic:
eq_empty_iff_forall_notMem.trans
    ⟨fun H => ⟨fun x => H x trivial⟩, fun H x _ => @IsEmpty.false α H x⟩

Premises used: trivial, IsEmpty.mk, Set.eq_empty_iff_forall_notMem, Iff.intro, Iff.trans, IsEmpty.false
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
inst : Nonempty α
⊢ Ne.{u + 1} (α := Set α) ∅ univ

Tactic:
fun e =>
  not_isEmpty_of_nonempty α <| univ_eq_empty_iff.1 e.symm

Premises used: not_isEmpty_of_nonempty, Set.univ_eq_empty_iff, Iff.mp, Eq.symm, Not
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s ⊆ univ

Tactic:
fun _ _ => trivial

Premises used: trivial, Set.Mem, Set.univ, setOf, Set.Subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ univ ⊆ s ↔ s = univ

Tactic:
@top_le_iff _ _ _ s

Premises used: top_le_iff
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s = univ ↔ ∀ (x : α), x ∈ s

Tactic:
univ_subset_iff.symm.trans <| forall_congr' fun _ => imp_iff_right trivial

Premises used: Set.univ_subset_iff, trivial, imp_iff_right, forall_congr', Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ (∀ (x : α), x ∈ s) → s = univ

Tactic:
eq_univ_iff_forall.2

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
inst : Subsingleton α
x : α
hx : x ∈ s
y : α
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ y ∈ s

Tactic:
rwa [Subsingleton.elim y x]

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
inst : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ

Tactic:
exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

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

Tactic:
eq_univ_of_univ_subset <| (hs ▸ h : univ ⊆ t)

Premises used: Eq.rec, Set.eq_univ_of_univ_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s : Set α
rw : s ≠ univ ↔ ¬∀ (x : α), x ∈ s
rw₁ rw₂ : s ≠ univ ↔ ¬s = univ
⊢ s ≠ univ ↔ ∃ (a : α), ¬a ∈ s

Tactic:
rw [← not_forall, ← eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, Classical.not_forall
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ (x : α), x ∈ s ∧ ¬x ∈ t

Tactic:
simp [subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
inst : Unique α
⊢ Eq (α := Set α) univ {default}

Tactic:
Set.ext fun x => iff_of_true trivial <| Subsingleton.elim x default

Premises used: Set.ext, Inhabited.default, trivial, iff_of_true, Subsingleton.elim
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ s ⊂ univ ↔ s ≠ univ

Tactic:
lt_top_iff_ne_top

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
rw : (s ⊆ univ ∧ ∃ (a : α), ¬a ∈ s) ↔ ∃ (x : α), x ∈ sᶜ
⊢ s ⊂ univ ↔ sᶜ.Nonempty

Tactic:
rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]

Premises used: Set.ssubset_def, Set.nonempty_def, Set.not_univ_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ (s ⊆ univ ∧ ∃ (a : α), ¬a ∈ s) ↔ ∃ (x : α), x ∈ sᶜ

Tactic:
simp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
rw : (sᶜ ⊆ univ ∧ ∃ (a : α), ¬a ∈ sᶜ) ↔ ∃ (x : α), x ∈ s
⊢ sᶜ ⊂ univ ↔ s.Nonempty

Tactic:
rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]

Premises used: Set.ssubset_def, Set.nonempty_def, Set.not_univ_subset
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s : Set α
⊢ (sᶜ ⊆ univ ∧ ∃ (a : α), ¬a ∈ sᶜ) ↔ ∃ (x : α), x ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
β : Type v
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst : Nonempty α
⊢ Nontrivial.{u} (Set α)

Tactic:
⟨⟨∅, univ, empty_ne_univ⟩⟩

Premises used: Set.univ, Nontrivial.mk, Exists.intro, EmptyCollection.emptyCollection, Set.empty_ne_univ
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s₁ s₂ : Set α
⊢ s₁ ∪ s₂ = {a : α | a ∈ s₁ ∨ a ∈ s₂}

Tactic:
rfl

Premises used: Set.union, setOf, rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
⊢ x ∈ a → x ∈ a ∪ b

Tactic:
Or.inl

Premises used: Set.union, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
b a : Set α
⊢ x ∈ b → x ∈ a ∪ b

Tactic:
Or.inr

Premises used: Set.union, Set.Mem, setOf, Or.inr
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
x : α
a b : Set α
H : x ∈ a ∪ b
⊢ x ∈ a ∨ x ∈ b

Tactic:
H

Premises used: Set.union, Set.Mem, setOf