awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
inst : LE α
s t : Set α
h : s ⊆ t
x y : (↑s : Type u_1)
⊢ inclusion (s := s) (t := t) h x ≤ inclusion (s := s) (t := t) h y ↔ x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
inst : LT α
s t : Set α
h : s ⊆ t
x y : (↑s : Type u_1)
⊢ inclusion (s := s) (t := t) h x < inclusion (s := s) (t := t) h y ↔ x < y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
s : Set α
⊢ insert x s = {y : α | y = x ∨ y ∈ s}

Tactic:
rfl

Premises used: Set.insert, setOf, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
s : Set α
⊢ s ⊆ insert x s

Tactic:
fun _ => Or.inr

Premises used: Set.insert, Set.Mem, setOf, Set.Subset, Or.inr
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
s : Set α
⊢ x ∈ insert x s

Tactic:
Or.inl rfl

Premises used: Set.insert, Set.Mem, setOf, Or.inl, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
s : Set α
y : α
⊢ x ∈ s → x ∈ insert y s

Tactic:
Or.inr

Premises used: Set.insert, Set.Mem, setOf, Or.inr
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x a : α
s : Set α
⊢ x ∈ insert a s → x = a ∨ x ∈ s

Tactic:
id

Premises used: Set.insert, Set.Mem, setOf, id
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
⊢ b ∈ insert a s → b ≠ a → b ∈ s

Tactic:
Or.resolve_left

Premises used: Set.insert, Set.Mem, setOf, Or.resolve_left
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
⊢ b ∈ insert a s → ¬b ∈ s → b = a

Tactic:
Or.resolve_right

Premises used: Set.insert, Set.Mem, setOf, Or.resolve_right
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x a : α
s : Set α
⊢ x ∈ insert a s ↔ x = a ∨ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.insert, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s : Set α
h : a ∈ s
⊢ insert a s = s

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
⊢ ¬a ∈ s → s ≠ insert a t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ insert a s = s ↔ a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ insert a s ≠ s ↔ ¬a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ t
hs : s ⊆ t
⊢ insert a s ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
h : s ⊆ t
⊢ insert a s ⊆ insert a t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
⊢ s ⊂ t ↔ ∃ (a : α), ¬a ∈ s ∧ insert a s ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
hst : s ⊆ t
hat : a ∈ t
has : ¬a ∈ s
⊢ s ⊂ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ s ⊂ insert a s

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a b : α
s : Set α
⊢ insert a (insert b s) = insert b (insert a s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s : Set α
⊢ insert a (insert a s) = insert a s

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
⊢ insert a s ∪ t = insert a (s ∪ t)

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
⊢ s ∪ insert a t = insert a (s ∪ t)

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s : Set α
⊢ (insert a s).Nonempty

Tactic:
⟨a, mem_insert a s⟩

Premises used: Set.Nonempty, Exists.intro, Set.mem_insert
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 t : Set α
a_1 b a : α
s : Set α
⊢ Nonempty.{u_1 + 1} (↑(insert a s) : Type u_1)

Tactic:
(insert_nonempty a s).to_subtype

Premises used: Set.insert_nonempty, Set.Nonempty.to_subtype
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s t : Set α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s t : Set α
⊢ insert a (s ∪ t) = insert a s ∪ insert a t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
P : α → Prop
a : α
s : Set α
H : ∀ (x : α), x ∈ insert a s → P x
x : α
h : x ∈ s
⊢ P x

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
P : α → Prop
a : α
s : Set α
H : ∀ (x : α), x ∈ s → P x
ha : P a
x : α
h : x ∈ insert a s
⊢ P x

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
P : α → Prop
a : α
s : Set α
⊢ (∃ (x : α), x ∈ insert a s ∧ P x) ↔ P a ∨ ∃ (x : α), x ∈ s ∧ P x

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
P : α → Prop
a : α
s : Set α
⊢ (∀ (x : α), x ∈ insert a s → P x) ↔ P a ∧ ∀ (x : α), x ∈ s → P x

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t_1 : Set α
a b : α
inst : DecidableEq α
t : Set α
x : α
h_1 : ¬x ∈ t
y : { i : α // i ∈ insert x t }
h : ¬(↑y : α) = x
⊢ (↑y : α) ∈ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t_1 : Set α
a b : α
inst : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : Option { i : α // i ∈ t }
z : { i : α // i ∈ t }
⊢ (↑z : α) ∈ insert x t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t_1 : Set α
a b : α
inst : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : { i : α // i ∈ insert x t }
⊢ (fun (y : Option { i : α // i ∈ t }) ↦
        y.elim (Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) x ⋯) fun (z : { i : α // i ∈ t }) ↦
          Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) (↑z : α) ⋯)
      ((fun (y : { i : α // i ∈ insert x t }) ↦
          (if h : (↑y : α) = x then none else some (Subtype.mk (p := fun (i : α) ↦ i ∈ t) (↑y : α) ⋯) :
            Option { i : α // i ∈ t }))
        y) =
    y

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t_1 : Set α
a b : α
inst : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
⊢ Eq.{u_1 + 1} (α := Option { i : α // i ∈ t })
    ((fun (y : { i : α // i ∈ insert x t }) ↦
        (if h : (↑y : α) = x then none else some (Subtype.mk (p := fun (i : α) ↦ i ∈ t) (↑y : α) ⋯) :
          Option { i : α // i ∈ t }))
      ((fun (y : Option { i : α // i ∈ t }) ↦
          y.elim (Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) x ⋯) fun (z : { i : α // i ∈ t }) ↦
            Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) (↑z : α) ⋯)
        none))
    none

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t_1 : Set α
a b : α
inst : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : { i : α // i ∈ t }
⊢ (fun (y : { i : α // i ∈ insert x t }) ↦
        (if h : (↑y : α) = x then none else some (Subtype.mk (p := fun (i : α) ↦ i ∈ t) (↑y : α) ⋯) :
          Option { i : α // i ∈ t }))
      ((fun (y : Option { i : α // i ∈ t }) ↦
          y.elim (Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) x ⋯) fun (z : { i : α // i ∈ t }) ↦
            Subtype.mk (p := fun (i : α) ↦ i ∈ insert x t) (↑z : α) ⋯)
        (some y)) =
    some y

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t : Set α
a_1 b x a : α
simp : a = x ↔ Membership.mem (γ := Set α) {x} a
⊢ Membership.mem (γ := Set α) (insert x ∅) a ↔ Membership.mem (γ := Set α) {x} a

Tactic:
simp only [mem_empty_iff_false, mem_insert_iff, or_false]

Premises used: Set.mem_empty_iff_false, or_false, Set.mem_insert_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t : Set α
a_1 b x a : α
⊢ a = x ↔ Membership.mem (γ := Set α) {x} a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
s t : Set α
a_1 b x a : α
⊢ a = x ↔ Membership.mem (γ := Set α) {x} a

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {a} (insert a ∅)

Tactic:
(insert_empty_eq a).symm

Premises used: LawfulSingleton.insert_empty_eq, Eq.symm
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a b : α
⊢ Membership.mem (γ := Set α) {b} a ↔ a = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a b : α
⊢ ¬Membership.mem (γ := Set α) {b} a ↔ a ≠ b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {n : α | n = a} {a}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {x : α | a = x} {a}

Tactic:
ext fun _ => eq_comm

Premises used: Set.ext, eq_comm
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Set α) {a} a

Tactic:
@rfl _ _

Premises used: Set.Mem, setOf, Set.singleton, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x y : α
h : Membership.mem (γ := Set α) {y} x
⊢ x = y

Tactic:
h

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x y : α
⊢ Eq (α := Set α) {x} {y} ↔ x = y

Tactic:
Set.ext_iff.trans eq_iff_eq_cancel_left

Premises used: eq_iff_eq_cancel_left, Iff.trans, Set.ext_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
⊢ Injective (β := Set α) singleton

Tactic:
fun _ _ =>
  singleton_eq_singleton_iff.mp

Premises used: Set.singleton_eq_singleton_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x y : α
H : x = y
⊢ Membership.mem (γ := Set α) {y} x

Tactic:
H

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
s : Set α
⊢ insert x s = {x} ∪ s

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Set.singleton, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Set.Nonempty (α := α) {a}

Tactic:
⟨a, rfl⟩

Premises used: Set.Nonempty, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Ne (α := Set α) {a} ∅

Tactic:
(singleton_nonempty _).ne_empty

Premises used: Set.singleton_nonempty, Set.Nonempty.ne_empty
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Ne (α := Set α) ∅ {a}

Tactic:
(singleton_ne_empty a).symm

Premises used: Ne.symm, Set.singleton_ne_empty
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ SSubset (α := Set α) ∅ {a}

Tactic:
(singleton_nonempty _).empty_ssubset

Premises used: Set.singleton_nonempty, Set.Nonempty.empty_ssubset
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s : Set α
⊢ {a} ⊆ s ↔ a ∈ s

Tactic:
forall_eq

Premises used: Set.Mem, setOf, forall_eq, Set.Subset, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a b : α
⊢ Subset (α := Set α) {a} {b} ↔ a = b

Tactic:
simp
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {b : α | b = a} {a}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ {a} ∪ s = insert a s

Tactic:
rfl

Premises used: Set.insert, Set.Mem, setOf, Set.singleton, rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ s ∪ {a} = insert a s

Tactic:
union_comm _ _

Premises used: Set.insert, Set.Mem, setOf, Set.union_comm, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ ({a} ∩ s).Nonempty ↔ a ∈ s

Tactic:
simp only [Set.Nonempty, mem_inter_iff, mem_singleton_iff, exists_eq_left]

Premises used: Set.mem_inter_iff, exists_eq_left, Set.Nonempty, Set.mem_singleton_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
rw : ({a} ∩ s).Nonempty ↔ a ∈ s
rw₁ rw₂ : a ∈ s ↔ a ∈ s
⊢ (s ∩ {a}).Nonempty ↔ a ∈ s

Tactic:
rw [inter_comm, singleton_inter_nonempty]

Premises used: Set.inter_comm, Set.singleton_inter_nonempty
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ {a} ∩ s = ∅ ↔ ¬a ∈ s

Tactic:
not_nonempty_iff_eq_empty.symm.trans singleton_inter_nonempty.not

Premises used: Set.not_nonempty_iff_eq_empty, Iff.not, Iff.trans, Set.singleton_inter_nonempty, Iff.symm
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
rw : {a} ∩ s = ∅ ↔ ¬a ∈ s
rw₁ rw₂ : ¬a ∈ s ↔ ¬a ∈ s
⊢ s ∩ {a} = ∅ ↔ ¬a ∈ s

Tactic:
rw [inter_comm, singleton_inter_eq_empty]

Premises used: Set.singleton_inter_eq_empty, Set.inter_comm
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ {a} ∩ s = {a}

Tactic:
simpa
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
simpa
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
⊢ ¬Membership.mem (γ := Set (Set α)) {∅} s ↔ s.Nonempty

Tactic:
nonempty_iff_ne_empty.symm

Premises used: Set.Mem, setOf, Set.singleton, Set.nonempty_iff_ne_empty, Iff.symm
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a

Tactic:
Subset.antisymm_iff.trans <| and_comm.trans <| and_congr_left' singleton_subset_iff

Premises used: Set.singleton_subset_iff, Set.Subset.antisymm_iff, and_comm, and_congr_left', Iff.trans
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ s = {a} ↔ s.Nonempty ∧ ∀ (x : α), x ∈ s → x = a

Tactic:
eq_singleton_iff_unique_mem.trans <|
    and_congr_left fun H => ⟨fun h' => ⟨_, h'⟩, fun ⟨x, h⟩ => H x h ▸ h⟩

Premises used: Membership.mem, Eq.rec, and_congr_left, Iff.intro, Exists.intro, Iff.trans, _private.0.Set.eq_singleton_iff_nonempty_unique_mem.match_1, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
h_1 : ∃ (a : α), s = {a}
a : α
h : s = {a}
⊢ (fun (a : α) ↦ a ∈ s) a ∧ ∀ (y : α), (fun (a : α) ↦ a ∈ s) y → y = a

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
h_1 : ∃! a : α, a ∈ s
a : α
h : (fun (a : α) ↦ a ∈ s) a ∧ ∀ (y : α), (fun (a : α) ↦ a ∈ s) y → y = a
⊢ s = {a}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
l : List α
a : α
⊢ Eq (α := Set α) {x : α | x ∈ l} {a} ↔ ∃ (n : ℕ), n > 0 ∧ l = List.replicate n a

Tactic:
simpa +contextual [Set.ext_iff, iff_iff_implies_and_implies, forall_and, List.eq_replicate_iff,
    List.length_pos_iff_exists_mem] using ⟨fun _ _ ↦ ⟨_, ‹_›⟩, fun x hx h ↦ h _ hx ▸ hx⟩

Premises used: iff_iff_implies_and_implies, List.length_pos_iff_exists_mem, List.eq_replicate_iff, Set.ext_iff, forall_and
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
l : List α
H : l.Nodup
a : α
mp : Eq (α := Set α) {x : α | x ∈ l} {a} → l = [a]
mpr : l = [a] → Eq (α := Set α) {x : α | x ∈ l} {a}
⊢ Eq (α := Set α) {x : α | x ∈ l} {a} ↔ l = [a]

Tactic:
constructor
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
l : List α
H : l.Nodup
a : α
mp : (∃ (n : ℕ), n > 0 ∧ l = List.replicate n a) → l = [a]
⊢ Eq (α := Set α) {x : α | x ∈ l} {a} → l = [a]

Tactic:
rw [setOf_mem_list_eq_replicate]

Premises used: Set.setOf_mem_list_eq_replicate
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : (List.replicate n a).Nodup
⊢ n ≤ 1

Tactic:
simp only [List.nodup_replicate] at H

Premises used: List.nodup_replicate
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : n ≤ 1
⊢ n = 1

Tactic:
lia
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : n ≤ 1
⊢ List.replicate n a = [a]

Tactic:
simp [show n = 1 by lia]
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
H : [a].Nodup
⊢ Eq (α := Set α) {x : α | x ∈ [a]} {a}

Tactic:
simp
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
⊢ default = Subtype.mk (p := fun (x_1 : α) ↦ Membership.mem (γ := Set α) {x} x_1) x ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_3
s : Set α
x : α
⊢ s ⊆ {x} ↔ ∀ (y : α), y ∈ s → y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x : α
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
h : s.Nonempty
⊢ s ⊆ {a} ↔ s = {a}

Tactic:
subset_singleton_iff_eq.trans <| or_iff_right h.ne_empty

Premises used: Set.Nonempty.ne_empty, or_iff_right, Iff.trans, Set.subset_singleton_iff_eq
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x : α
rw : s = ∅ → s ≠ {x}
⊢ s ⊂ {x} ↔ s = ∅

Tactic:
rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
    and_iff_left_iff_imp]

Premises used: and_not_self_iff, Set.subset_singleton_iff_eq, or_false, or_and_right, and_iff_left_iff_imp, ssubset_iff_subset_ne
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}

Tactic:
fun h => h ▸ empty_ne_singleton _

Premises used: Eq.rec, Set.empty_ne_singleton, Eq.symm
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x : α
⊢ s = ∅ → s ≠ {x}

Tactic:
exact fun h => h ▸ empty_ne_singleton _
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x : α
hs : s ⊂ {x}
⊢ s = ∅

Tactic:
ssubset_singleton_iff.1 hs

Premises used: Iff.mp, Set.ssubset_singleton_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_3
inst : Subsingleton α
s t : Set α
inst_1 : Nonempty.{u_3 + 1} (↑s : Type u_3)
inst_2 : Nonempty.{u_3 + 1} (↑t : Type u_3)
⊢ s = t

Tactic:
Nonempty.of_subtype.eq_univ.trans Nonempty.of_subtype.eq_univ.symm

Premises used: Set.Nonempty.of_subtype, Set.Nonempty.eq_univ, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_3
inst : Subsingleton α
s t : Set α
hs : s.Nonempty
inst_1 : Nonempty.{u_3 + 1} (↑t : Type u_3)
⊢ s = t

Tactic:
have := hs.to_subtype; eq_of_nonempty_of_subsingleton s t

Premises used: Set.Nonempty.to_subtype, Set.eq_of_nonempty_of_subsingleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
inst : Subsingleton α
inst_1 : Zero α
s : Set α
h : s.Nonempty
⊢ s = {0}

Tactic:
eq_of_nonempty_of_subsingleton' {0} h

Premises used: Singleton.singleton, OfNat.ofNat, Set.eq_of_nonempty_of_subsingleton'
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
inst : Subsingleton α
inst_1 : One α
s : Set α
h : s.Nonempty
⊢ s = {1}

Tactic:
eq_of_nonempty_of_subsingleton' {1} h

Premises used: Singleton.singleton, OfNat.ofNat, Set.eq_of_nonempty_of_subsingleton'
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ Disjoint {a} s ↔ ¬a ∈ s

Tactic:
simp [Set.disjoint_iff, subset_def]

Premises used: Set.subset_def, Set.disjoint_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ Disjoint s {a} ↔ ¬a ∈ s

Tactic:
disjoint_comm.trans disjoint_singleton_left

Premises used: Set.disjoint_singleton_left, disjoint_comm, Iff.trans
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a b : α
⊢ Disjoint (α := Set α) {a} {b} ↔ a ≠ b

Tactic:
simp
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
⊢ Disjoint (insert a s) t ↔ ¬a ∈ t ∧ Disjoint s t

Tactic:
simp only [Set.disjoint_left, Set.mem_insert_iff, forall_eq_or_imp]

Premises used: Set.disjoint_left, forall_eq_or_imp, Set.mem_insert_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
rw : Disjoint (insert a t) s ↔ ¬a ∈ s ∧ Disjoint s t
rw₁ : ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
rw₂ rw₃ : ¬a ∈ s ∧ Disjoint s t ↔ ¬a ∈ s ∧ Disjoint s t
⊢ Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t

Tactic:
rw [disjoint_comm, disjoint_insert_left, disjoint_comm]

Premises used: disjoint_comm, Set.disjoint_insert_left
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
ha : ¬a ∈ s
⊢ insert a s = insert b s ↔ a = b

Tactic:
⟨fun h => eq_of_mem_insert_of_notMem (h ▸ mem_insert a s) ha,
    congr_arg (fun x => insert x s)⟩

Premises used: Insert.insert, congr_arg, Iff.intro, Set.eq_of_mem_insert_of_notMem
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
s : Set α
h : ¬a ∈ s
⊢ insert a s \ s = {a}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
h : a ∈ s
⊢ s ∩ insert a t = insert a (s ∩ t)

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
h : a ∈ t
⊢ insert a s ∩ t = insert a (s ∩ t)

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
h : ¬a ∈ s
⊢ s ∩ insert a t = s ∩ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s t : Set α
a : α
h : ¬a ∈ t
⊢ insert a s ∩ t = s ∩ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a : α
⊢ Eq (α := Set α) {a, a} {a}

Tactic:
union_self _

Premises used: Set.insert, Set.Mem, setOf, Set.singleton, Set.union_self
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
a b : α
⊢ Eq (α := Set α) {a, b} {b, a}

Tactic:
union_comm _ _

Premises used: Set.insert, Set.Mem, setOf, Set.union_comm, Set.singleton
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x y z w : α
simp : ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
⊢ Eq (α := Set α) {x, y} {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp [subset_antisymm_iff, insert_subset_iff]

Premises used: Set.insert_subset_iff, subset_antisymm_iff
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
aesop
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
⊢ {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ {a, b} ⊆ s

Tactic:
pair_subset_iff.2 ⟨ha,hb⟩

Premises used: Iff.mpr, Set.pair_subset_iff, And.intro
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
⊢ s ⊆ {a, b} ↔ ∀ (x : α), x ∈ s → x = a ∨ x = b

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x y : α
⊢ s ⊆ {x, y} → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
x y : α
⊢ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y} → s ⊆ {x, y}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
rw : ¬s = ∅
⊢ s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Tactic:
rw [Set.subset_pair_iff_eq, or_iff_right]

Premises used: Set.subset_pair_iff_eq, or_iff_right
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅

Tactic:
hs.ne_empty

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅

Tactic:
exact hs.ne_empty

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
x y : β
hp : ∃ (a : α), p a
hn : ∃ (a : α), ¬p a
⊢ Eq (α := Set β) (range fun (a : α) ↦ if p a then x else y) {x, y}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_1
x : α
⊢ Eq (α := Set (Set α)) (𝒫 {x}) {∅, {x}}

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_3
β : Type u_4
a : α
⊢ Eq (α := Set (α × β)) (Prod.fst ⁻¹' {a}) (range fun (x : β) ↦ (a, x))

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
α : Type u_3
β : Type u_4
b : β
⊢ Eq (α := Set (α × β)) (Prod.snd ⁻¹' {b}) (range fun (x : α) ↦ (x, b))

Tactic:
grind
-- Module: Mathlib.Data.Set.Insert
Goal:
p q : Prop
⊢ Membership.mem (γ := Set Prop) {p}ᶜ q ↔ Membership.mem (γ := Set Prop) {¬p} q

Tactic:
simpa [@Iff.comm q] using not_iff

Premises used: not_iff, Iff.comm
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ GaloisConnection (image f) (preimage f)

Tactic:
fun _ _ =>
  image_subset_iff

Premises used: Set.image_subset_iff, GaloisConnection
-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ GaloisConnection (preimage f) (kernImage f)

Tactic:
fun _ _ =>
  subset_kernImage_iff.symm

Premises used: Set.subset_kernImage_iff, Iff.symm, GaloisConnection