mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s : List α
⊢ s ∈ [].tails ↔ s <:+ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s : List α
a : α
t : List α
⊢ s ∈ (a :: t).tails ↔ s <:+ a :: t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = [] :: map (fun t ↦ a :: t) l.inits

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
rw [ndinsert_of_notMem h] at ht
      subst ht
      simp [attach_cons, h]

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (a :: l) :: l.tails

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ ([] ++ []).inits = [].inits ++ map (fun l ↦ [] ++ l) [].inits.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t), t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).inits = [].inits ++ map (fun l ↦ [] ++ l) (a :: t).inits.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint (ndinsert a s) t ↔ _root_.Disjoint (a ::ₘ s) t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).inits = (a :: s).inits ++ map (fun l ↦ a :: s ++ l) t.inits.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ ([] ++ []).tails = map (fun l ↦ l ++ []) [].tails ++ [].tails.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).tails = map (fun l ↦ l ++ a :: t) [].tails ++ (a :: t).tails.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).tails = map (fun l ↦ l ++ t) (a :: s).tails ++ t.tails.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ [].inits = (map reverse [].reverse.tails).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
x✝¹ : α
x✝ : Multiset α
h : x✝.ndunion t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u
⊢ (x✝¹ ::ₘ x✝).ndunion t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).inits = (map reverse (a :: l).reverse.tails).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
⊢ [].tails = (map reverse [].reverse.inits).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ s.ndunion t = s.dedup + t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (map reverse (a :: l).reverse.inits).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndunion t = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse l.tails).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s).ndinter t = a ::ₘ s.ndinter t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s).ndinter t = s.ndinter t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse l.inits).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s ∩ t).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.inits = l.reverse.tails.reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.tails = l.reverse.inits.reverse

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.tails.length = l.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.inits.length = l.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndinter t = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
⊢ l.tails[n] = drop n l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : Fin l.tails.length
⊢ l.tails.get n = drop (↑n) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
⊢ l.inits[n] = take n l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : Fin l.inits.length
⊢ l.inits.get n = take (↑n) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).inits = map (map g) l.inits

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).tails = map (map g) l.tails

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits = take (n + 1) l.inits

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ insert a l = if a ∈ l then l else a :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ∈ s.erase b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hs : b ∈ s
hsa : ¬b ∈ s.erase a
⊢ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ⊆ t.erase a ↔ s ⊆ t ∧ ¬a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ ↑(s.erase a) = ↑s \ {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
⊢ ↑{a} = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (s.erase a).erase a = s.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
⊢ (s.erase a).erase b = (s.erase b).erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ ↑s = {a} ↔ s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
x✝ : α
⊢ ¬(x✝ ∈ s → x✝ ∉ t) ↔ x✝ ∈ s ∧ x✝ ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
⊢ s.erase x = s.erase y ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
⊢ Disjoint {a} s ↔ a ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ ↑s ⊆ {a} ↔ s ⊆ {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ {a} ⊆ ↑s ↔ {a} ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Set ι
f : ι → α
⊢ (s.PairwiseDisjoint fun i ↦ {f i}) ↔ Set.InjOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: n : ℕ
⊢ range n.succ = n ::ₘ range n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) m)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x ↦ a + x) (range b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : Unique α
s : Finset α
⊢ s.Nonempty ↔ s = {default}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ a, s = {a}) ↔ ∃! a, a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ ↑{a} ⊆ s ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ s ⊆ {a} ↔ s = ∅ ∨ s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} ⊆ {b} ↔ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ s ⊂ {a} ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
⊢ ¬∅.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_5
s t : Finset α
h : Disjoint s t
a : α
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬{a}.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
hs : s.Nontrivial
⊢ s ≠ {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
h : Disjoint s t
⊢ ∀ (x : α), x ∈ ↑(s.disjUnion t h) ↔ x ∈ ↑s ∪ ↑t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s₁ s₂ t : Finset α
h₁ : Disjoint s₁ t
h₂ : Disjoint s₂ t
⊢ s₁.disjUnion t h₁ = s₂.disjUnion t h₂ ↔ s₁ = s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t₁ t₂ : Finset α
h₁ : Disjoint s t₁
h₂ : Disjoint s t₂
⊢ s.disjUnion t₁ h₁ = s.disjUnion t₂ h₂ ↔ t₁ = t₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a b : α
s : Finset α
l : List α
h : Nodup ⟦[]⟧
⊢ ¬{ val := ⟦[]⟧, nodup := h }.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ s.disjUnion {a} h = cons a s ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a b : α
s : Finset α
l : List α
head✝ : α
h : Nodup ⟦[head✝]⟧
⊢ ¬{ val := ⟦[head✝]⟧, nodup := h }.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a✝ b✝ : α
s : Finset α
l : List α
a b : α
tail✝ : List α
h : Nodup ⟦a :: b :: tail✝⟧
⊢ a ∈ ↑{ val := ⟦a :: b :: tail✝⟧, nodup := h }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a✝ b✝ : α
s : Finset α
l : List α
a b : α
tail✝ : List α
h : Nodup ⟦a :: b :: tail✝⟧
⊢ b ∈ ↑{ val := ⟦a :: b :: tail✝⟧, nodup := h }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
m : Multiset α
hm : m.Nodup
⊢ { val := m, nodup := hm }.Nonempty ↔ m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ ↑(cons a s h) = insert a ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ⊂ t ↔ ∃ a, ∃ (h : a ∉ s), cons a s h ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ 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:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ 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✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = (a ::ₘ s.val).dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).val = a ::ₘ s.val

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ : α
s : Finset α
h : a✝ ∉ s
a : α
⊢ a ∈ cons a✝ s h ↔ a ∈ insert a✝ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ ↑(insert a s) = insert a ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
⊢ x ∈ insert y s ↔ x ∈ insert y ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
f : α → β
a : α
⊢ insert a ∅ = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ insert a s = s ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
⊢ insert a (insert b s) = insert b (insert a s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ ↑{a, b} = {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ ↑s = {a, b} ↔ s = {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ insert a (insert a s) = insert a s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ≠ insert a t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
h : s ⊆ t
⊢ insert a s ⊆ insert a t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
⊢ motive { val := s, nodup := nd }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
⊢ motive s hs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥(insert x t)
⊢ (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) ((fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : (i : α) → i ∈ insert a s → f i
⊢ prodPiInsert f (insertPiProd f x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ insertPiProd f (prodPiInsert f x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a}.toFinset = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
⊢ (replicate n a).toFinset = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset = ∅ ↔ l = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset.Nonempty ↔ l ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ filter p s ⊂ s ↔ ∃ x, x ∈ s ∧ ¬p x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.toList = [a] ↔ s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter q (filter p s) = filter (fun a ↦ p a ∧ q a) s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ (a :: s.toList).Nodup

Tactic:
by

Goal state after: