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

Goal state before:
pp: case case4
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
l₁✝ l₂✝ : List α
x✝ : l₂✝ = [] → False
h✝ : ¬elem a✝ l₂✝ = true
ih1✝ : a ∈ l₁✝.bagInter l₂✝ ↔ a ∈ l₁✝ ∧ a ∈ l₂✝
⊢ a ∈ l₁✝.bagInter l₂✝ ↔ a ∈ a✝ :: l₁✝ ∧ a ∈ l₂✝

Tactic:
grind

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

Goal state before:
pp: case case1
α : Type u_1
inst✝ : DecidableEq α
a : α
x✝ : List α
⊢ count a [] = min (count a []) (count a x✝)

Tactic:
grind

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

Goal state before:
pp: case case2
α : Type u_1
inst✝ : DecidableEq α
a : α
t✝ : List α
x✝ : t✝ = [] → False
⊢ count a [] = min (count a t✝) (count a [])

Tactic:
grind

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

Goal state before:
pp: case case3
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
l₁✝ l₂✝ : List α
x✝ : l₂✝ = [] → False
h✝ : elem a✝ l₂✝ = true
ih1✝ : count a (l₁✝.bagInter (l₂✝.erase a✝)) = min (count a l₁✝) (count a (l₂✝.erase a✝))
⊢ count a (a✝ :: l₁✝.bagInter (l₂✝.erase a✝)) = min (count a (a✝ :: l₁✝)) (count a l₂✝)

Tactic:
grind

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

Goal state before:
pp: case case4
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
l₁✝ l₂✝ : List α
x✝ : l₂✝ = [] → False
h✝ : ¬elem a✝ l₂✝ = true
ih1✝ : count a (l₁✝.bagInter l₂✝) = min (count a l₁✝) (count a l₂✝)
⊢ count a (l₁✝.bagInter l₂✝) = min (count a (a✝ :: l₁✝)) (count a l₂✝)

Tactic:
grind

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

Goal state before:
pp: case case1
α : Type u_1
inst✝ : DecidableEq α
x✝ : List α
⊢ [] <+ []

Tactic:
grind

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

Goal state before:
pp: case case2
α : Type u_1
inst✝ : DecidableEq α
t✝ : List α
x✝ : t✝ = [] → False
⊢ [] <+ t✝

Tactic:
grind

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

Goal state before:
pp: case case3
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
l₁✝ l₂✝ : List α
x✝ : l₂✝ = [] → False
h✝ : elem a✝ l₂✝ = true
ih1✝ : l₁✝.bagInter (l₂✝.erase a✝) <+ l₁✝
⊢ a✝ :: l₁✝.bagInter (l₂✝.erase a✝) <+ a✝ :: l₁✝

Tactic:
grind

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

Goal state before:
pp: case case4
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
l₁✝ l₂✝ : List α
x✝ : l₂✝ = [] → False
h✝ : ¬elem a✝ l₂✝ = true
ih1✝ : l₁✝.bagInter l₂✝ <+ l₁✝
⊢ l₁✝.bagInter l₂✝ <+ a✝ :: l₁✝

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [a].bagInter l₁ = if a ∈ l₁ then [a] else []

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [].bagInter [a] = if a ∈ [] then [a] else []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.bagInter [a] = if a ∈ tail✝ then [a] else []
⊢ (head✝ :: tail✝).bagInter [a] = if a ∈ head✝ :: tail✝ then [a] else []

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (l₂.erase a) = [].bagInter l₂

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬a ∈ tail✝ → tail✝.bagInter (l₂.erase a) = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (head✝ :: tail✝).bagInter (l₂.erase a) = (head✝ :: tail✝).bagInter l₂

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₂
⊢ ([].erase a).bagInter l₂ = [].bagInter l₂

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬a ∈ l₂ → (tail✝.erase a).bagInter l₂ = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ l₂
⊢ ((head✝ :: tail✝).erase a).bagInter l₂ = (head✝ :: tail✝).bagInter l₂

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t : List α
⊢ [].bagInter t ~ [].bagInter t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : ∀ (t : List α), l₁✝.bagInter t ~ l₂✝.bagInter t
t : List α
⊢ (x✝ :: l₁✝).bagInter t ~ (x✝ :: l₂✝).bagInter t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case swap
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x✝ y✝ : α
l✝ t : List α
⊢ (y✝ :: x✝ :: l✝).bagInter t ~ (x✝ :: y✝ :: l✝).bagInter t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case trans
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : ∀ (t : List α), l₁✝.bagInter t ~ l₂✝.bagInter t
a_ih✝ : ∀ (t : List α), l₂✝.bagInter t ~ l₃✝.bagInter t
t : List α
⊢ l₁✝.bagInter t ~ l₃✝.bagInter t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b ↦ decide (p b)) ∘ f) l) ~ List.map f (List.filter (fun b ↦ decide (p (f b))) l)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ Set.SurjOn toFinset {l | l.Nodup} Set.univ

Tactic:
rintro ⟨⟨l⟩, hl⟩ _
  exact ⟨l, hl, (toFinset_eq hl).symm⟩

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

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

Tactic:
← subset_zero

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ _root_.Disjoint s t
Module: Mathlib.Data.Finset.Empty

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), ¬x ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ¬s ⊂ ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
⊢ ↑∅ = ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑s = ∅ ↔ s = ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ (∃ x, x ∈ ∅ ∧ p x) ↔ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a : α
l : List α
b : α
⊢ bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
    cons_append a l b (bidirectionalRec nil singleton cons_append l)

Tactic:
by
  grind [bidirectionalRec, cases List]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ (∀ (x : α), x ∈ ∅ → p x) ↔ True

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]

pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length

Tactic:
rfl

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

Goal state before:
pp: case cons.nil
α : Type u_1
head✝ : α
tail✝ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝ → tail✝ = l₁ ++ drop l₁.length tail✝
h : [] <+: head✝ :: tail✝
⊢ head✝ :: tail✝ = [] ++ drop [].length (head✝ :: tail✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ [x] <:+: xs ↔ x ∈ xs

Tactic:
rw [List.mem_iff_append, List.IsInfix]

Goal state after:
α : Type u_1
x : α
xs : List α
⊢ (∃ s t, s ++ [x] ++ t = xs) ↔ ∃ s t, xs = s ++ x :: t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mpr
α : Type u_1
x : α
⊢ [x] <:+: [x]

Tactic:
rfl

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

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

Tactic:
simp [← map_reverse]

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

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

Tactic:
simp [← map_reverse]

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

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

Tactic:
simp [← map_reverse]

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:
← subset_zero

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t
Module: Mathlib.Data.List.Infix

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

Tactic:
simp [← map_reverse]

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

Goal state before:
pp: case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ), i < min n l.length + 1 → min i (min n l.length) = min i l.length

Tactic:
grind

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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:
grind

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:
grind

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:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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:
grind

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:
grind

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

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

Tactic:
rfl

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:
rw [insert_val, ndinsert_of_notMem h]

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:
grind

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:
grind

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:
grind

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

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

Tactic:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ ((↑s).Pairwise (r on f) ∧ ∀ b ∈ ↑s, a ≠ b → (r on f) a b ∧ (r on f) b a) ↔
    (↑s).Pairwise (r on f) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
grind

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 p (filter q s)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = insert n (range n)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ n ∉ range n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ n ∈ range (n + 1)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
⊢ range n ⊆ s ↔ ∀ x < n, x ∈ s

Tactic:
grind

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

Goal state before:
pp: s : Finset ℕ
n : ℕ
⊢ s ⊆ range n ↔ ∀ x ∈ s, x < n

Tactic:
grind

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

Goal state before:
pp: n m : ℕ
⊢ range n ⊆ range m ↔ n ≤ m

Tactic:
grind

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

Goal state before:
pp: a b : ℕ
⊢ a ∈ range b.succ ↔ a ≤ b

Tactic:
grind

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

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ x ≤ n

Tactic:
grind

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

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ n - x ≠ 0

Tactic:
grind

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

Goal state before:
pp: n : ℕ
x✝ : (range n).Nonempty
k : ℕ
hk : k ∈ range n
⊢ n ≠ 0

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ 0 ∈ range n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ 0 ∈ Set.Iio n

Tactic:
grind

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

Goal state before:
pp: s : Finset ℕ
a : ℕ
x✝² : Finset ℕ
x✝¹ : a ∉ x✝²
x✝ : ∃ n, x✝² ⊆ range n
n : ℕ
hn : x✝² ⊆ range n
⊢ insert a x✝² ⊆ range (max (a + 1) n)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
⊢ Function.LeftInverse (fun j ↦ ⟨j + k, ⋯⟩) fun i ↦ ↑i - k

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
⊢ Function.RightInverse (fun j ↦ ⟨j + k, ⋯⟩) fun i ↦ ↑i - k

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidablePred fun x ↦ x ∈ s
hst : s ⊆ t
⊢ filter (fun x ↦ x ∈ s) t = s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ (s₂ \ s₁) = ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ ∀ (a b : Finset α), a ⊓ b ⊔ a \ b = a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ ∀ (a b : Finset α), a ⊓ b ⊓ a \ b = ⊥

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ s ∪ t \ s = t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ s₂ \ s₁ ∪ s₁ = s₂

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u v : Finset α
hst : s ⊆ t
hvu : v ⊆ u
⊢ s \ u ⊆ t \ v

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
h : x ∉ t
⊢ insert x s \ t = insert x (s \ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t s : Finset α
x : α
h : x ∈ t
⊢ insert x s \ t = s \ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∉ s
⊢ insert a s \ s = {a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
hb : b ∉ s
⊢ cons a s ha \ cons b s hb = {a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
⊢ s \ insert x t = s \ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : t ⊆ s
ht : t.Nonempty
⊢ s \ t ⊂ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ (s \ {c}).Nonempty

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

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

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ u : Finset α
⊢ s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t) ∩ s = s

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t) ∩ t = t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ ∩ s₂ = s₂ ∩ s₁

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finset α
⊢ s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ s.disjUnion t h = s ∪ t

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
ha : a ∉ s
hb : a ≠ b
⊢ (cons a s ha).erase b = cons a (s.erase b) ⋯

Tactic:
grind

Goal state after: