awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Unique α
s : Set α
⊢ s = ∅ ∨ s = {default}

Tactic:
s.eq_empty_or_singleton_of_subsingleton.imp_right fun ⟨a, ha⟩ => Unique.eq_default a ▸ ha

Premises used: Set.eq_empty_or_singleton_of_subsingleton, Or.imp_right
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
mp : Subsingleton.{u + 1} (↑s : Type u) → s.Subsingleton
mpr : s.Subsingleton → Subsingleton.{u + 1} (↑s : Type u)
⊢ Subsingleton.{u + 1} (↑s : Type u) ↔ s.Subsingleton

Tactic:
constructor
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ Subsingleton.{u + 1} (↑s : Type u) → s.Subsingleton

Tactic:
fun h => fun a ha b hb => ?_

Premises used: Set.Subsingleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
mp : ∀ (h : Subsingleton.{u + 1} (↑s : Type u)) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s), a = b
⊢ Subsingleton.{u + 1} (↑s : Type u) → s.Subsingleton

Tactic:
refine fun h => fun a ha b hb => ?_
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
h : Subsingleton.{u + 1} (↑s : Type u)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Tactic:
SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)

Premises used: Iff.mpr, Subtype.mk, Subsingleton.elim, SetCoe.ext_iff
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
h : Subsingleton.{u + 1} (↑s : Type u)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Tactic:
exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)

Premises used: Iff.mpr, Subtype.mk, Subsingleton.elim, SetCoe.ext_iff
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton.{u + 1} (↑s : Type u)

Tactic:
fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

Premises used: SetCoe.ext, Subsingleton.intro, Subtype.property
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton.{u + 1} (↑s : Type u)

Tactic:
exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

Premises used: SetCoe.ext, Subsingleton.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton.{u + 1} (↑s : Type u)

Tactic:
s.subsingleton_coe.2

Premises used: Iff.mpr, Set.subsingleton_coe
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s_1 t : Set α
inst : Subsingleton α
s : Set α
rw : s.Subsingleton
⊢ Subsingleton.{u + 1} (↑s : Type u)

Tactic:
rw [s.subsingleton_coe]

Premises used: Set.subsingleton_coe
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s_1 t : Set α
inst : Subsingleton α
s : Set α
⊢ s.Subsingleton

Tactic:
subsingleton_of_subsingleton

Premises used: Set.subsingleton_of_subsingleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s_1 t : Set α
inst : Subsingleton α
s : Set α
⊢ s.Subsingleton

Tactic:
exact subsingleton_of_subsingleton

Premises used: Set.subsingleton_of_subsingleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
inst : LT α
hs : s.Subsingleton
⊢ DenselyOrdered.{u} (↑s : Type u)

Tactic:
have := (subsingleton_coe _).mpr hs
  ⟨fun _ _ h ↦ ⟨_, h.trans_eq (Subsingleton.elim _ _), h⟩⟩

Premises used: Iff.mpr, LT.lt.trans_eq, DenselyOrdered.mk, And.intro, Exists.intro, Set.subsingleton_coe, Subsingleton.elim
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ s.Nontrivial

Tactic:
⟨x, hx, y, hy, hxy⟩

Premises used: And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ hs.choose (s := s).fst ∈ s

Tactic:
hs.choose_spec.left

Premises used: Exists.choose_spec, Set.Mem, And.left, Classical.choose
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ hs.choose (s := s).snd ∈ s

Tactic:
hs.choose_spec.right.choose_spec.left

Premises used: Exists.choose_spec, Set.Mem, And.right, And.left, Classical.choose
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ hs.choose (s := s).fst ≠ hs.choose (s := s).snd

Tactic:
hs.choose_spec.right.choose_spec.right

Premises used: Exists.choose_spec, And.right, Classical.choose
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s t : Set α
hs : s.Nontrivial
hst : s ⊆ t
⊢ t.Nontrivial

Tactic:
let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨x, hst hx, y, hst hy, hxy⟩

Premises used: And.intro, Exists.intro, _private.0.Set.Nontrivial.mono.match_1, Set.Nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
x y : α
hxy : x ≠ y
⊢ Set.Nontrivial (α := α) {x, y}

Tactic:
⟨x, mem_insert _ _, y, mem_insert_of_mem _ (mem_singleton _), hxy⟩

Premises used: Set.mem_singleton, Set.mem_insert_of_mem, And.intro, Exists.intro, Set.mem_insert, Set.Nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x y : α
hxy : x ≠ y
h : {x, y} ⊆ s
⊢ s.Nontrivial

Tactic:
(nontrivial_pair hxy).mono h

Premises used: Set.nontrivial_pair, Set.Nontrivial.mono
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ ∃ (x : α), ∃ (y : α), x ≠ y ∧ {x, y} ⊆ s

Tactic:
let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨x, y, hxy, insert_subset hx <| singleton_subset_iff.2 hy⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Exists, Insert.insert, HasSubset.Subset, Ne, And, And.intro, Exists.intro, _private.0.Set.Nontrivial.mono.match_1, Singleton.singleton, Set.insert_subset
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ s.Nontrivial ↔ ∃ (x : α), ∃ (y : α), x ≠ y ∧ {x, y} ⊆ s

Tactic:
⟨Nontrivial.pair_subset, fun H =>
    let ⟨_, _, hxy, h⟩ := H
    nontrivial_of_pair_subset hxy h⟩

Premises used: Set.Nontrivial.pair_subset, _private.0.Set.nontrivial_iff_pair_subset.match_1, Set.nontrivial_of_pair_subset, Iff.intro, Set.Nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hx : x ∈ s
h : ∃ (y : α), y ∈ s ∧ y ≠ x
⊢ s.Nontrivial

Tactic:
let ⟨y, hy, hyx⟩ := h
  ⟨y, hy, x, hx, hyx⟩

Premises used: _private.0.Set.nontrivial_of_exists_ne.match_1, And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
by_contra! : ∀ (H : ∀ (x : α) (_ : x ∈ s), x = z), False
⊢ ∃ (x : α), x ∈ s ∧ x ≠ z

Tactic:
by_contra! H
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
H : ∀ (x : α) (_ : x ∈ s), x = z
rcases : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), False
⊢ False

Tactic:
rcases hs with ⟨x, hx, y, hy, hxy⟩
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
z : α
H : ∀ (x : α) (_ : x ∈ s), x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ z ≠ z

Tactic:
rw [H x hx, H y hy] at hxy
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
z : α
H : ∀ (x : α) (_ : x ∈ s), x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False

Tactic:
hxy rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
z : α
H : ∀ (x : α) (_ : x ∈ s), x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False

Tactic:
exact hxy rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hx : x ∈ s
⊢ s.Nontrivial ↔ ∃ (y : α), y ∈ s ∧ y ≠ x

Tactic:
⟨fun H => H.exists_ne _, nontrivial_of_exists_ne hx⟩

Premises used: Set.Nontrivial.exists_ne, Set.nontrivial_of_exists_ne, Iff.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
inst : Preorder α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : x < y
⊢ s.Nontrivial

Tactic:
⟨x, hx, y, hy, ne_of_lt hxy⟩

Premises used: And.intro, Exists.intro, Set.Nontrivial, ne_of_lt
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
inst : Preorder α
H : ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x < y
⊢ s.Nontrivial

Tactic:
let ⟨_, hx, _, hy, hxy⟩ := H
  nontrivial_of_lt hx hy hxy

Premises used: Set.nontrivial_of_lt, Set.Nontrivial, _private.0.Set.nontrivial_of_exists_lt.match_1
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
inst : LinearOrder α
hs : s.Nontrivial
⊢ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x < y

Tactic:
let ⟨x, hx, y, hy, hxy⟩ := hs
  Or.elim (lt_or_gt_of_ne hxy) (fun H => ⟨x, hx, y, hy, H⟩) fun H => ⟨y, hy, x, hx, H⟩

Premises used: lt_or_gt_of_ne, Membership.mem, Exists, And, And.intro, LT.lt, Exists.intro, _private.0.Set.Nontrivial.mono.match_1, Or.elim
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
inst : LinearOrder α
⊢ s.Nontrivial ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x < y

Tactic:
⟨Nontrivial.exists_lt, nontrivial_of_exists_lt⟩

Premises used: Set.Nontrivial.exists_lt, Set.nontrivial_of_exists_lt, Iff.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ s.Nonempty

Tactic:
let ⟨x, hx, _⟩ := hs
  ⟨x, hx⟩

Premises used: Set.Nonempty, Exists.intro, _private.0.Set.Nontrivial.nonempty.match_1
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ s ≠ ∅

Tactic:
hs.nonempty.ne_empty

Premises used: Set.Nonempty.ne_empty, Set.Nontrivial.nonempty
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ ¬s ⊆ ∅

Tactic:
hs.nonempty.not_subset_empty

Premises used: Set.Nontrivial.nonempty, Set.Nonempty.not_subset_empty
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
⊢ ¬Set.Nontrivial.{u} (α := α) ∅

Tactic:
fun h => h.ne_empty rfl

Premises used: Set.Nontrivial.ne_empty, Not, rfl
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
x : α
H : Set.Nontrivial (α := α) {x}
⊢ ∃ (y : α), Membership.mem (γ := Set α) {x} y ∧ y ≠ x

Tactic:
rw [nontrivial_iff_exists_ne (mem_singleton x)] at H

Premises used: Set.mem_singleton, Set.nontrivial_iff_exists_ne
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
x : α
H : ∃ (y : α), Membership.mem (γ := Set α) {x} y ∧ y ≠ x
let : ∀ (y : α) (hy : Membership.mem (γ := Set α) {x} y) (hya : y ≠ x), False
⊢ False

Tactic:
let ⟨y, hy, hya⟩ := H
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
x : α
H : ∃ (y : α), Membership.mem (γ := Set α) {x} y ∧ y ≠ x
y : α
hy : Membership.mem (γ := Set α) {x} y
hya : y ≠ x
⊢ False

Tactic:
hya (mem_singleton_iff.1 hy)

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
x : α
H : ∃ (y : α), Membership.mem (γ := Set α) {x} y ∧ y ≠ x
y : α
hy : Membership.mem (γ := Set α) {x} y
hya : y ≠ x
⊢ False

Tactic:
exact hya (mem_singleton_iff.1 hy)

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hs : s.Nontrivial
H : s = {x}
⊢ Set.Nontrivial (α := α) {x}

Tactic:
rw [H] at hs
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hs : s.Nontrivial
H : s = {x}
hs₁ : Set.Nontrivial (α := α) {x}
⊢ s = {x}

Tactic:
rw [H] at hs
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hs : Set.Nontrivial (α := α) {x}
H : s = {x}
⊢ False

Tactic:
not_nontrivial_singleton hs

Premises used: Set.not_nontrivial_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hs : Set.Nontrivial (α := α) {x}
H : s = {x}
⊢ False

Tactic:
exact not_nontrivial_singleton hs

Premises used: Set.not_nontrivial_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
x : α
hs : s.Nontrivial
⊢ ¬s ⊆ {x}

Tactic:
(not_congr subset_singleton_iff_eq).2 (not_or_intro hs.ne_empty hs.ne_singleton)

Premises used: Iff.mpr, Set.Nontrivial.ne_empty, not_or_intro, Set.subset_singleton_iff_eq, Set.Nontrivial.ne_singleton, not_congr
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Nontrivial α
⊢ Set.Nontrivial.{u} (α := α) univ

Tactic:
let ⟨x, y, hxy⟩ := exists_pair_ne α
  ⟨x, mem_univ _, y, mem_univ _, hxy⟩

Premises used: _private.0.Set.nontrivial_univ.match_1, Set.univ, And.intro, Exists.intro, Set.mem_univ, Set.Nontrivial, exists_pair_ne
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
h : Set.Nontrivial.{u} (α := α) univ
⊢ Nontrivial α

Tactic:
let ⟨x, _, y, _, hxy⟩ := h
  ⟨⟨x, y, hxy⟩⟩

Premises used: Nontrivial, _private.0.Set.nontrivial_of_univ_nontrivial.match_1, Nontrivial.mk, Exists.intro
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
⊢ Set.Nontrivial.{u} (α := α) univ ↔ Nontrivial α

Tactic:
⟨nontrivial_of_univ_nontrivial, fun h => @nontrivial_univ _ h⟩

Premises used: Set.nontrivial_of_univ_nontrivial, Iff.intro, Set.nontrivial_univ
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Nontrivial α
a : α
⊢ Ne (α := Set α) {a} univ

Tactic:
fun h ↦ nontrivial_univ.not_subset_singleton h.superset

Premises used: Set.Nontrivial.not_subset_singleton, Set.nontrivial_univ, Not, Eq.superset
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : Nontrivial α
a : α
⊢ SSubset (α := Set α) {a} univ

Tactic:
ssubset_univ_iff.mpr <| singleton_ne_univ a

Premises used: Iff.mpr, Set.singleton_ne_univ, Set.ssubset_univ_iff
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : s.Nontrivial
⊢ Nontrivial α

Tactic:
let ⟨x, _, y, _, hxy⟩ := hs
  ⟨⟨x, y, hxy⟩⟩

Premises used: Nontrivial, Nontrivial.mk, Exists.intro, _private.0.Set.Nontrivial.mono.match_1
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ Nontrivial.{u} (↑s : Type u) ↔ s.Nontrivial

Tactic:
simp [← nontrivial_univ_iff, Set.Nontrivial]

Premises used: Set.Nontrivial, Set.nontrivial_univ_iff
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
hs : Nontrivial.{u} (↑s : Type u)
⊢ Nontrivial α

Tactic:
nontrivial_of_nontrivial <| nontrivial_coe_sort.1 hs

Premises used: Set.nontrivial_of_nontrivial, Iff.mp, Set.nontrivial_coe_sort
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : Nontrivial.{u_1} (↑s : Type u_1)
⊢ Nontrivial.{u_1} (↑t : Type u_1)

Tactic:
Nontrivial.coe_sort <| (nontrivial_coe_sort.1 hs).mono hst

Premises used: Set.Nontrivial.coe_sort, Iff.mp, Set.Nontrivial.mono, Set.nontrivial_coe_sort
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
simp_rw : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ s.Nontrivial
simp_rw₁ : (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x ≠ y
simp_rw₂ :
  (∃ (x : α), ∃ (h : x ∈ s), ∃ (x_1 : α), ∃ (x_2 : x_1 ∈ s), ¬x = x_1) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : α), y ∈ s ∧ x ≠ y
⊢ ¬s.Subsingleton ↔ s.Nontrivial

Tactic:
simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]

Premises used: exists_prop, Set.Subsingleton, Set.Nontrivial, Classical.not_forall
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ ¬s.Nontrivial ↔ s.Subsingleton

Tactic:
Iff.not_left not_subsingleton_iff.symm

Premises used: Set.not_subsingleton_iff, Iff.not_left, Iff.symm
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
simp [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
ha : a ∈ s
rw : s.Subsingleton ∨ s.Nontrivial
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← subsingleton_iff_singleton ha]

Premises used: Set.subsingleton_iff_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
s.subsingleton_or_nontrivial

Premises used: Set.subsingleton_or_nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
exact s.subsingleton_or_nontrivial

Premises used: Set.subsingleton_or_nontrivial
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Nontrivial ↔ s ≠ {a}

Tactic:
⟨Nontrivial.ne_singleton, (eq_singleton_or_nontrivial ha).resolve_left⟩

Premises used: Or.resolve_left, Iff.intro, Set.eq_singleton_or_nontrivial, Set.Nontrivial.ne_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
s : Set α
⊢ s.Nonempty → (∃ (a : α), s = {a}) ∨ s.Nontrivial

Tactic:
fun ⟨a, ha⟩ ↦ (eq_singleton_or_nontrivial ha).imp_left <| Exists.intro a

Premises used: Or.imp_left, Exists, _private.0.Set.Subsingleton.eq_empty_or_singleton.match_1, Exists.intro, Or, Set.eq_singleton_or_nontrivial, Set.Nontrivial, Singleton.singleton, Eq
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
x : Prop
⊢ x = True ∨ x = False

Tactic:
Classical.propComplete x

Premises used: Classical.propComplete
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
x : Prop
⊢ x = True ∨ x = False

Tactic:
exact Classical.propComplete x

Premises used: Classical.propComplete
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : IsEmpty α
S : Set α
hS : Membership.mem (γ := Set (Set α)) univ S
⊢ Membership.mem (γ := Set (Set α)) {∅} S

Tactic:
simp [Set.eq_empty_of_isEmpty S]

Premises used: Set.eq_empty_of_isEmpty
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
inst : IsEmpty α
⊢ Subset (α := Set (Set α)) {∅} univ

Tactic:
simp
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
h : IsEmpty α
⊢ Eq (α := Set (Set α)) univ {∅}

Tactic:
simp
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
refine : ∀ (h : Eq (α := Set (Set α)) univ {∅}), IsEmpty α
⊢ Eq (α := Set (Set α)) univ {∅} ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ by simp⟩
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
h : Eq (α := Set (Set α)) univ {∅}
this : Membership.mem (γ := Set (Set α)) univ univ
⊢ IsEmpty α

Tactic:
aesop
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
h : Eq (α := Set (Set α)) univ {∅}
suffices : Membership.mem (γ := Set (Set α)) univ univ
⊢ IsEmpty α

Tactic:
suffices @univ α ∈ univ by aesop
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
h : Eq (α := Set (Set α)) univ {∅}
⊢ Membership.mem (γ := Set (Set α)) univ univ

Tactic:
simp
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : s.Subsingleton
⊢ MonotoneOn f s

Tactic:
fun _ ha _ hb _ => (congr_arg _ (h ha hb)).le

Premises used: Eq.le, congr_arg, MonotoneOn
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : s.Subsingleton
⊢ AntitoneOn f s

Tactic:
fun _ ha _ hb _ => (congr_arg _ (h hb ha)).le

Premises used: Eq.le, congr_arg, AntitoneOn
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : s.Subsingleton
⊢ StrictMonoOn f s

Tactic:
fun _ ha _ hb hlt => (hlt.ne (h ha hb)).elim

Premises used: False.elim, StrictMonoOn, LT.lt.ne
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : s.Subsingleton
⊢ StrictAntiOn f s

Tactic:
fun _ ha _ hb hlt => (hlt.ne (h ha hb)).elim

Premises used: False.elim, StrictAntiOn, LT.lt.ne
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
a : α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ MonotoneOn f {a}

Tactic:
subsingleton_singleton.monotoneOn f

Premises used: Set.subsingleton_singleton, Set.Subsingleton.monotoneOn
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
a : α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ AntitoneOn f {a}

Tactic:
subsingleton_singleton.antitoneOn f

Premises used: Set.Subsingleton.antitoneOn, Set.subsingleton_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
a : α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictMonoOn f {a}

Tactic:
subsingleton_singleton.strictMonoOn f

Premises used: Set.Subsingleton.strictMonoOn, Set.subsingleton_singleton
-- Module: Mathlib.Data.Set.Subsingleton
Goal:
α : Type u
β : Type v
a : α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictAntiOn f {a}

Tactic:
subsingleton_singleton.strictAntiOn f

Premises used: Set.Subsingleton.strictAntiOn, Set.subsingleton_singleton
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
c : α
⊢ c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

Tactic:
simp [(· ⊻ ·)]

Premises used: HasSups.sups
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a b : α
⊢ a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t

Tactic:
mem_image2_of_mem

Premises used: Set.Mem, Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s₁ s₂ t₁ t₂ : Set α
⊢ s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂

Tactic:
image2_subset

Premises used: Set.image2_subset
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t₁ t₂ : Set α
⊢ t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂

Tactic:
image2_subset_left

Premises used: Set.image2_subset_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s₁ s₂ t : Set α
⊢ s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t

Tactic:
image2_subset_right

Premises used: Set.image2_subset_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
b : α
⊢ b ∈ t → (fun (a : α) ↦ a ⊔ b) '' s ⊆ s ⊻ t

Tactic:
image_subset_image2_left

Premises used: Set.image_subset_image2_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ s → (fun (x1 x2 : α) ↦ x1 ⊔ x2) a '' t ⊆ s ⊻ t

Tactic:
image_subset_image2_right

Premises used: Set.image_subset_image2_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
p : α → Prop
⊢ (∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)

Tactic:
forall_mem_image2

Premises used: Set.forall_mem_image2, Set.Mem
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t u : Set α
⊢ s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u

Tactic:
image2_subset_iff

Premises used: Set.image2_subset_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ (s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image2_nonempty_iff

Premises used: Set.image2_nonempty_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty

Tactic:
Nonempty.image2

Premises used: Set.Nonempty.image2
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ (s ⊻ t).Nonempty → s.Nonempty

Tactic:
Nonempty.of_image2_left

Premises used: Set.Nonempty.of_image2_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ (s ⊻ t).Nonempty → t.Nonempty

Tactic:
Nonempty.of_image2_right

Premises used: Set.Nonempty.of_image2_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
t : Set α
⊢ ∅ ⊻ t = ∅

Tactic:
image2_empty_left

Premises used: Set.image2_empty_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Set α
⊢ s ⊻ ∅ = ∅

Tactic:
image2_empty_right

Premises used: Set.image2_empty_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
image2_eq_empty_iff

Premises used: Set.image2_eq_empty_iff
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
t : Set α
a : α
⊢ {a} ⊻ t = (fun (b : α) ↦ a ⊔ b) '' t

Tactic:
image2_singleton_left

Premises used: Set.image2_singleton_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s : Set α
b : α
⊢ s ⊻ {b} = (fun (a : α) ↦ a ⊔ b) '' s

Tactic:
image2_singleton_right

Premises used: Set.image2_singleton_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
a b : α
⊢ Eq (α := Set α) ({a} ⊻ {b}) {a ⊔ b}

Tactic:
image2_singleton

Premises used: Set.image2_singleton
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s₁ s₂ t : Set α
⊢ (s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t

Tactic:
image2_union_left

Premises used: Set.image2_union_left
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s t₁ t₂ : Set α
⊢ s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂

Tactic:
image2_union_right

Premises used: Set.image2_union_right
-- Module: Mathlib.Data.Set.Sups
Goal:
α : Type u_2
inst : SemilatticeSup α
s₁ s₂ t : Set α
⊢ (s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t

Tactic:
image2_inter_subset_left

Premises used: Set.image2_inter_subset_left