awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a b : α
⊢ Eq (α := Finset α) {a} {b} ↔ a = b

Tactic:
singleton_injective.eq_iff

Premises used: Function.Injective.eq_iff, Finset.singleton_injective
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
⊢ Finset.Nonempty (α := α) {a}

Tactic:
⟨a, mem_singleton_self a⟩

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

Tactic:
(singleton_nonempty a).ne_empty

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

Tactic:
(singleton_ne_empty a).symm

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

Tactic:
(singleton_nonempty _).empty_ssubset

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

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ (↑s : Set α) = {a} ↔ s = {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ (↑s : Set α) ⊆ {a} ↔ s ⊆ {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ {a} ⊆ (↑s : Set α) ↔ {a} ⊆ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

Tactic:
grind [singleton_nonempty]

Premises used: Finset.singleton_nonempty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : Unique α
s : Finset α
⊢ s.Nonempty ↔ s = {default}

Tactic:
simp [eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton]

Premises used: Finset.eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
⊢ (∃ (a : α), s = {a}) ↔ ∃! a : α, a ∈ s

Tactic:
simp only [eq_singleton_iff_unique_mem, ExistsUnique]

Premises used: Finset.eq_singleton_iff_unique_mem, ExistsUnique
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Set α
a : α
⊢ (↑{a} : Set α) ⊆ s ↔ a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ {a} ⊆ s ↔ a ∈ s

Tactic:
singleton_subset_set_iff

Premises used: Finset.singleton_subset_set_iff, Set.Subset
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ s ⊆ {a} ↔ s = ∅ ∨ s = {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a b : α
⊢ Subset (α := Finset α) {a} {b} ↔ a = b

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

Tactic:
subset_singleton_iff.trans <| or_iff_right h.ne_empty

Premises used: Finset.Nonempty.ne_empty, Finset.subset_singleton_iff, or_iff_right, Iff.trans
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ s ⊆ {a} ↔ ∀ b ∈ s, b = a

Tactic:
forall₂_congr fun _ _ => mem_singleton

Premises used: Finset.mem_singleton, forall₂_congr
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
⊢ s ⊂ {a} ↔ s = ∅

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
x : α
hs : s ⊂ {x}
⊢ s = ∅

Tactic:
ssubset_singleton_iff.1 hs

Premises used: Finset.ssubset_singleton_iff, Iff.mp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
⊢ s.Nontrivial ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Nontrivial
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ s.Nonempty

Tactic:
hs.nonempty

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

Tactic:
simp [Finset.Nontrivial]

Premises used: Finset.Nontrivial
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
⊢ ¬Finset.Nontrivial (α := α) {a}

Tactic:
simp [Finset.Nontrivial]

Premises used: Finset.Nontrivial
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
hs : Finset.Nontrivial (α := α) {a}
⊢ False

Tactic:
not_nontrivial_singleton hs

Premises used: Finset.not_nontrivial_singleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
hs : Finset.Nontrivial (α := α) {a}
⊢ False

Tactic:
exact not_nontrivial_singleton hs

Premises used: Finset.not_nontrivial_singleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
hs : s.Nontrivial
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
hs.exists_ne _

Premises used: Set.Nontrivial.exists_ne
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
rw : (↑s : Set α) = {a} ∨ s.Nontrivial
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← coe_eq_singleton]

Premises used: Finset.coe_eq_singleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ (↑s : Set α) = {a} ∨ s.Nontrivial

Tactic:
Set.eq_singleton_or_nontrivial ha

Premises used: Set.eq_singleton_or_nontrivial
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ (↑s : Set α) = {a} ∨ s.Nontrivial

Tactic:
exact Set.eq_singleton_or_nontrivial ha

Premises used: Set.eq_singleton_or_nontrivial
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s.Nontrivial ↔ s ≠ {a}

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

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

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

Premises used: _private.0.Finset.Nonempty.exists_eq_singleton_or_nontrivial.match_1, Or.imp_left, Exists, Finset.eq_singleton_or_nontrivial, Finset.Nontrivial, Exists.intro, Or, Singleton.singleton, Eq
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α).Nontrivial ↔ s.Nontrivial

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s : Finset α
a b : α
inst : Nonempty α
⊢ Nontrivial.{u_1} (Finset α)

Tactic:
‹Nonempty α›.elim fun a => ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩

Premises used: Nonempty.elim, Nontrivial.mk, Exists.intro, Finset.singleton_ne_empty, EmptyCollection.emptyCollection, Singleton.singleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
i : α
⊢ (↑default : α) = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 : Finset α
a b : α
s : Finset α
l : List α
h : Nodup ⟦[]⟧
⊢ ¬{ val := ⟦[]⟧, nodup := h : Finset α }.Nontrivial

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 : Finset α
a b : α
s : Finset α
l : List α
head : α
h : Nodup ⟦[head]⟧
⊢ ¬{ val := ⟦[head]⟧, nodup := h : Finset α }.Nontrivial

Tactic:
simp [SetLike.coe]

Premises used: SetLike.coe
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 : Finset α
a_1 b_1 : α
s : Finset α
l : List α
a b : α
tail : List α
h : Nodup ⟦a :: b :: tail⟧
⊢ a ∈ (↑{ val := ⟦a :: b :: tail⟧, nodup := h : Finset α } : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 : Finset α
a_1 b_1 : α
s : Finset α
l : List α
a b : α
tail : List α
h : Nodup ⟦a :: b :: tail⟧
⊢ b ∈ (↑{ val := ⟦a :: b :: tail⟧, nodup := h : Finset α } : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a b : α
h : a ∉ s
⊢ b ∈ cons a s h ↔ b = a ∨ b ∈ s

Tactic:
Multiset.mem_cons

Premises used: Set.Mem, setOf, Multiset.cons, Multiset.Mem, Multiset.mem_cons
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a b : α
s : Finset α
hb : b ∉ s
ha : a ∈ s
⊢ a ∈ cons b s hb

Tactic:
Multiset.mem_cons_of_mem ha

Premises used: Set.Mem, setOf, Multiset.mem_cons_of_mem, Multiset.cons, Multiset.Mem
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ a ∈ cons a s h

Tactic:
Multiset.mem_cons_self _ _

Premises used: Set.Mem, setOf, Multiset.cons, Multiset.Mem, Multiset.mem_cons_self
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).val = a ::ₘ s.val

Tactic:
rfl

Premises used: Multiset.cons, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a b : α
has : a ∉ s
h : b ∈ cons a s has
hb : b ∉ s
⊢ b = a

Tactic:
(mem_cons.1 h).resolve_right hb

Premises used: Iff.mp, Or.resolve_right, Finset.mem_cons
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
has : a ∉ s
i : α
hi : i ∈ cons a s has
hia : i ≠ a
⊢ i ∈ s

Tactic:
(mem_cons.1 hi).resolve_left hia

Premises used: Or.resolve_left, Iff.mp, Finset.mem_cons
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
p : α → Prop
⊢ (∀ x ∈ cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
p : α → Prop
h_1 : a ∉ s
H : ∀ x ∈ cons a s h_1, p x
x : α
h : x ∈ s
⊢ p x

Tactic:
H _ <| mem_cons.2 <| Or.inr h

Premises used: Iff.mpr, Finset.mem_cons, Or.inr
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Multiset α
h : (a ::ₘ s).Nodup
⊢ { val := a ::ₘ s, nodup := h : Finset α } = cons a { val := s, nodup := ⋯ } ⋯

Tactic:
rfl

Premises used: Finset.cons, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
⊢ cons a ∅ ⋯ = {a}

Tactic:
rfl

Premises used: Finset.cons, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).Nonempty

Tactic:
⟨a, mem_cons.2 <| Or.inl rfl⟩

Premises used: Iff.mpr, Exists.intro, Finset.Nonempty, Or.inl, Finset.mem_cons, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
⊢ cons a s h ≠ ∅

Tactic:
(cons_nonempty _).ne_empty

Premises used: Finset.cons_nonempty, Finset.Nonempty.ne_empty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
m : Multiset α
hm : m.Nodup
empty :
  ∀ {hm : Nodup.{u_1} (α := α) 0}, { val := 0, nodup := hm : Finset α }.Nonempty ↔ Ne.{u_1 + 1} (α := Multiset α) 0 0
cons :
  ∀ (a : α) (s : Multiset α),
    (∀ {hm : s.Nodup}, { val := s, nodup := hm : Finset α }.Nonempty ↔ s ≠ 0) →
      ∀ {hm : (a ::ₘ s).Nodup}, { val := a ::ₘ s, nodup := hm : Finset α }.Nonempty ↔ a ::ₘ s ≠ 0
⊢ { val := m, nodup := hm : Finset α }.Nonempty ↔ m ≠ 0

Tactic:
induction m using Multiset.induction_on
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
hm : Nodup.{u_1} (α := α) 0
⊢ { val := 0, nodup := hm : Finset α }.Nonempty ↔ Ne.{u_1 + 1} (α := Multiset α) 0 0

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Multiset α
h : ∀ {hm : s.Nodup}, { val := s, nodup := hm : Finset α }.Nonempty ↔ s ≠ 0
hm : (a ::ₘ s).Nodup
⊢ { val := a ::ₘ s, nodup := hm : Finset α }.Nonempty ↔ a ::ₘ s ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
h₁ : ∀ (x : α), x ∈ (↑(cons a s h) : Set α) ↔ x ∈ insert a (↑s : Set α)
⊢ (↑(cons a s h) : Set α) = insert a (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
x : α
⊢ x ∈ (↑(cons a s h) : Set α) ↔ x ∈ insert a (↑s : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
⊢ s ⊆ cons a s h

Tactic:
Multiset.subset_cons _ _

Premises used: Set.Mem, setOf, Multiset.cons, Multiset.Mem, Multiset.subset_cons, Multiset.Subset
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a : α
h : a ∉ s
⊢ s ⊂ cons a s h

Tactic:
Multiset.ssubset_cons h

Premises used: Set.Mem, setOf, Multiset.cons, Multiset.ssubset_cons, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s t : Finset α
a : α
h : a ∉ s
⊢ cons a s h ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
Multiset.cons_subset

Premises used: Multiset.cons_subset, Set.Mem, setOf, Multiset.cons, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₁ : insert a (↑s : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₂ : insert a (↑s : Set α) ⊆ insert a (↑t : Set α) ↔ s ⊆ t
rwa₃ : (↑s : Set α) ⊆ (↑t : Set α) ↔ s ⊆ t
rwa₄ : a ∉ (↑s : Set α)
rwa₅ : s ⊆ t ↔ s ⊆ t
rwa₆ : a ∉ (↑s : Set α)
rwa₇ : s ⊆ t ↔ s ⊆ t
rwa₈ rwa₉ rwa₁₀ : a ∉ (↑s : Set α)
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t

Tactic:
rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]

Premises used: Set.insert_subset_insert_iff, Finset.coe_cons, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s t : Finset α
⊢ s ⊂ t ↔ ∃ (a : α) (h : a ∉ s), cons a s h ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
s : Finset α
a b : α
hb : b ∉ s
ha : a ∉ cons b s hb
⊢ cons a (cons b s hb) ha = cons b (cons a s ⋯) ⋯

Tactic:
eq_of_veq <| Multiset.cons_swap a b s.val

Premises used: Multiset.cons_swap, Finset.eq_of_veq, Finset.val
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b : α
inst : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : (i : α) → i ∈ cons a s has → f i
⊢ prodPiCons f has (consPiProd f has x) = x

Tactic:
grind [prodPiCons, consPiProd]

Premises used: Finset.prodPiCons, Finset.consPiProd
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b : α
inst : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
fst : (consPiProd f has (prodPiCons f has x)).1 = x.1
snd : ∀ (x_1 : α) (hi : x_1 ∈ s), (consPiProd f has (prodPiCons f has x)).2 x_1 hi = x.2 x_1 hi
⊢ consPiProd f has (prodPiCons f has x) = x

Tactic:
ext _ hi
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b : α
inst : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
⊢ (consPiProd f has (prodPiCons f has x)).1 = x.1

Tactic:
grind [prodPiCons, consPiProd]

Premises used: Finset.prodPiCons, Finset.consPiProd
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b : α
inst : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x : f a × ((i : α) → i ∈ s → f i)
x_1 : α
hi : x_1 ∈ s
⊢ (consPiProd f has (prodPiCons f has x)).2 x_1 hi = x.2 x_1 hi

Tactic:
grind [prodPiCons, consPiProd]

Premises used: Finset.prodPiCons, Finset.consPiProd
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ insert a s = { val := ndinsert a s.val, nodup := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val

Tactic:
rfl

Premises used: Multiset.ndinsert, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
rw : (insert a s).val = ndinsert a s.val
⊢ (insert a s).val = (a ::ₘ s.val).dedup

Tactic:
rw [dedup_cons, dedup_eq_self]

Premises used: Multiset.dedup_cons, Finset.dedup_eq_self
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
rw : ndinsert a s.val = a ::ₘ s.val
rw₁ rw₂ : a ::ₘ s.val = a ::ₘ s.val
⊢ (insert a s).val = a ::ₘ s.val

Tactic:
rw [insert_val, ndinsert_of_notMem h]

Premises used: Finset.insert_val, Multiset.ndinsert_of_notMem
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
⊢ a ∈ insert b s ↔ a = b ∨ a ∈ s

Tactic:
mem_ndinsert

Premises used: Set.Mem, setOf, Multiset.mem_ndinsert, Multiset.Mem, Multiset.ndinsert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ a ∈ insert a s

Tactic:
mem_ndinsert_self a s.1

Premises used: Set.Mem, setOf, Finset.val, Multiset.Mem, Multiset.ndinsert, Multiset.mem_ndinsert_self
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
h : a ∈ s
⊢ a ∈ insert b s

Tactic:
mem_ndinsert_of_mem h

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_ndinsert_of_mem, Multiset.ndinsert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
h : b ∈ insert a s
⊢ b ≠ a → b ∈ s

Tactic:
(mem_insert.1 h).resolve_left

Premises used: Or.resolve_left, Finset.mem_insert, Iff.mp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
ha : b ∈ insert a s
hb : b ∉ s
⊢ b = a

Tactic:
(mem_insert.1 ha).resolve_right hb

Premises used: Finset.mem_insert, Iff.mp, Or.resolve_right
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Finset α) (insert a ∅) {a}

Tactic:
rfl

Premises used: Multiset.cons, Multiset.ofList, Multiset.ndinsert, rfl, ite
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a_1 : α
s : Finset α
h : a_1 ∉ s
a : α
⊢ a ∈ cons a_1 s h ↔ a ∈ insert a_1 s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ (↑(insert a s) : Set α) = insert a (↑s : Set α)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x y : α
⊢ x ∈ insert y s ↔ x ∈ insert y (↑s : Set α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s t : Finset α
a_1 b : α
f : α → β
a : α
⊢ Eq (α := Finset α) (insert a ∅) {a}

Tactic:
simp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : a ∈ s
⊢ insert a s = s

Tactic:
eq_of_veq <| ndinsert_of_mem h

Premises used: Finset.eq_of_veq, Multiset.ndinsert_of_mem
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ insert a s = s ↔ a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ insert a s ≠ s ↔ a ∉ s

Tactic:
insert_eq_self.not

Premises used: Finset.insert_eq_self, Iff.not
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Finset α) {a, a} {a}

Tactic:
insert_eq_of_mem <| mem_singleton_self _

Premises used: Finset.mem_singleton_self, Finset.insert_eq_of_mem
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Finset α
⊢ insert a (insert b s) = insert b (insert a s)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
⊢ (↑{a, b} : Set α) = {a, b}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
rw : (↑s : Set α) = (↑{a, b} : Set α) ↔ s = {a, b}
rw₁ rw₂ : s = {a, b} ↔ s = {a, b}
⊢ (↑s : Set α) = {a, b} ↔ s = {a, b}

Tactic:
rw [← coe_pair, coe_inj]

Premises used: Finset.coe_pair, Finset.coe_inj
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
⊢ Eq (α := Finset α) {a, b} {b, a}

Tactic:
insert_comm a b ∅

Premises used: Multiset.cons, Multiset.ofList, EmptyCollection.emptyCollection, Multiset.ndinsert, Finset.insert_comm, ite
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ insert a (insert a s) = insert a s

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

Tactic:
⟨a, mem_insert_self a s⟩

Premises used: Finset.mem_insert_self, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ insert a s ≠ ∅

Tactic:
(insert_nonempty a s).ne_empty

Premises used: Finset.Nonempty.ne_empty, Finset.insert_nonempty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
s_1 t : Finset α
a b : α
f : α → β
i : α
s : Finset α
⊢ Nonempty.{u_1 + 1} (↑(↑(insert i s) : Set α) : Type u_1)

Tactic:
(Finset.coe_nonempty.mpr (s.insert_nonempty i)).to_subtype

Premises used: Iff.mpr, Finset.coe_nonempty, Set.Nonempty.to_subtype, Finset.insert_nonempty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
contrapose : ∀ (h : s = insert a t), a ∈ s
⊢ s ≠ insert a t

Tactic:
contrapose h
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

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

Tactic:
insert_subset_iff.mpr ⟨ha,hs⟩

Premises used: Iff.mpr, Finset.insert_subset_iff, And.intro
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ s ⊆ insert a s

Tactic:
fun _b => mem_insert_of_mem

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
h : s ⊆ t
⊢ insert a s ⊆ insert a t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ (↑(insert a s) : Set α) ⊆ (↑(insert a t) : Set α) ↔ (↑s : Set α) ⊆ (↑t : Set α)

Tactic:
simp [ha]
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
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_self _ _) ha, congr_arg (insert · s)⟩

Premises used: Insert.insert, Finset.eq_of_mem_insert_of_notMem, congr_arg, Iff.intro
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ Set.InjOn (β := Finset α) (fun (a : α) ↦ insert a s) (↑s : Set α)ᶜ

Tactic:
fun _ h _ _ =>
  (insert_inj h).1

Premises used: Iff.mp, Finset.insert_inj, Set.InjOn
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t

Tactic:
mod_cast @Set.ssubset_iff_insert α s t

Premises used: Finset.coe_insert._simp_1, SetLike.coe_subset_coe._simp_1, congrArg, cast, Exists, HasSubset.Subset, Set.Subset, Finset.mem_coe._simp_1, funext, And, SetLike.coe_ssubset_coe._simp_1, Iff, SetLike.coe, congr, congrFun', Not, Eq.trans, Set.ssubset_iff_insert
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : a ∉ s
⊢ s ⊂ insert a s

Tactic:
ssubset_iff.mpr ⟨a, h, Subset.rfl⟩

Premises used: Iff.mpr, Finset.Subset.rfl, Finset.ssubset_iff, And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
nd : Nodup.{u_3} (α := α) 0
⊢ motive { val := 0, nodup := nd }

Tactic:
empty

Premises used: Finset.empty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
nd : Nodup.{u_3} (α := α) 0
⊢ motive { val := 0, nodup := nd }

Tactic:
exact empty
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
cons₁ : motive (Finset.cons a { val := s, nodup := ⋯ } ⋯)
⊢ motive { val := a ::ₘ s, nodup := nd }

Tactic:
rw [mk_cons nd]

Premises used: Finset.mk_cons