mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
this : h.choose < n ∧ p h.choose
⊢ p h.choose

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
this : h.choose < n ∧ p h.choose
⊢ ∀ (n_1 : ℕ), n_1 ≤ h.choose → (p n_1 ↔ ∃ h, p ↑⟨n_1, h⟩)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedLE ↔ l.SortedGE

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedGE ↔ l.SortedLE

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedLT ↔ l.SortedGT

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ Fin.find p h < i → ∃ m, m < i ∧ p m

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.reverse.SortedGT ↔ l.SortedLT

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ Fin.find p h ≤ i → ∃ m, m ≤ i ∧ p m

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
⊢ l ≠ []

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
hl' : l.head ⋯ ≠ []
⊢ l ≠ []

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
hl' : l.getLast ⋯ ≠ []
⊢ l ≠ []

Tactic:
by grind

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
R✝ : α✝ → α✝ → Prop
l✝ : List α✝
a : α✝
α : Type u_3
l : List α
R : α → α → Prop
l' : List α
h : 1 < l'.length
⊢ l' ≠ []

Tactic:
by grind

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

Goal state before:
pp: case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ
⊢ IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
| succ n =>

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ a ∈ l ∧ b ∈ l ∧ R a b)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ a ∈ l ∧ b ∈ l.tail ∧ R a b)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
hl₁ : IsChain R l
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a b : α), a ∈ l → b ∈ l → R a b → ∃ ha hb, S (f a ha) (f b hb)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
hl₂ : IsChain S (pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ ha hb, S (f a ha) (f b hb)) → R a b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
l : List β
hl : ∀ (b : β), b ∈ l → p b
a : β
ha : p a
⊢ ∀ (a_1 : β), a_1 ∈ a :: l → p a_1

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
l : List α
a : α
ha : p a
hl₁ : IsChain R (a :: l)
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ ∀ (a_1 b : α), a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → ∃ ha hb, S (f a_1 ha) (f b hb)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : IsChain S (f a ha :: pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ ∀ ⦃a b : α⦄, (∃ ha hb, S (f a ha) (f b hb)) → R a b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
l : List α
h : IsChain R l
hne : l.dropLast ≠ []
⊢ l ≠ []

Tactic:
by grind

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length

Tactic:
List.rotate',

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
⊢ ((l ++ [a]).rotate' n).length = (a :: l).length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as)
        (match p a with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum

Tactic:
match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only

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

Goal state before:
pp: case nil
α : Type u
l' : List α
⊢ ([] ++ l').rotate' [].length = l' ++ []

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝

Tactic:
· simp

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)
⊢ n = 0

Tactic:
by grind

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

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ [].rotate' (n + 1) ~ []

pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
· simp

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
⊢ [].rotate (n + 1) = [] ↔ [] = []

pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
· simp

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
getElem?_append_right hm,

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ (take (n % l.length) l)[m - (drop (n % l.length) l).length]? = l[(m + n) % l.length]?
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
⊢ [].reverse.alternatingProd = [].alternatingProd ^ (-1) ^ ([].length + 1)

Tactic:
by simp only [alternatingProd_nil, one_zpow, reverse_nil]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
l' : List α
hne : 1 < l'.length
hsub : l' <:+: l.reverse
⊢ l'.reverse ≠ []

Tactic:
by grind

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

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
⊢ ([].rotate (n + 1)).reverse.rotate (n + 1) = [].reverse

pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse

Tactic:
· simp

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % [].reverse.length
hk' : k = k' + 1
⊢ [].reverse =
    [].reverse.rotate
      ([].reverse.length - ([].reverse.length - n % [].reverse.length) % [].reverse.length +
        ([].reverse.length - n % [].reverse.length))

pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
· simp

Goal state after:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
h : (↑s).PairwiseDisjoint t
⊢ ↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)

Tactic:
simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion]

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

Goal state before:
pp: case succ.nil
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
⊢ map f ([].rotate (n + 1)) = (map f []).rotate (n + 1)

pp: case succ.cons
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)

Tactic:
· simp

Goal state after:
case succ.cons
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
hd : α
tl : List α
⊢ map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
i j : ℕ
hl : [].Nodup
⊢ [].rotate i = [].rotate j ↔ i % [].length = j % [].length ∨ [] = []

pp: case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
· simp

Goal state after:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
h : (↑s).PairwiseDisjoint f
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (s.disjiUnion f h) = s.disjiUnion (fun a ↦ filter p (f a)) ⋯

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h₁
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ (map g1 0).prod ∣ (map g2 0).prod

pp: case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : M} {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod

Tactic:
· simp

Goal state after:
case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : M} {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
n : ℕ
⊢ ∃ n_1, n_1 ≤ [].length ∧ [].rotate n_1 = [].rotate n

pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Tactic:
· simp

Goal state after:
case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)

Tactic:
by
        simp_rw [disjoint_disjiUnion_left, disjoint_disjiUnion_right]
        intros i hi j hj
        specialize hfg' hi hj
        grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
s' : Finset β
⊢ s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Finset β
inst✝ : DecidableEq β
a : α
⊢ {a}.biUnion t = t a

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst✝ : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
⊢ s₁.biUnion t ⊆ s₂.biUnion t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
u : α → Finset β
x : α
xs : x ∈ s
⊢ u x ⊆ s.biUnion u

Tactic:
by grind

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → Finset β
⊢ s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (s.biUnion f) = s.biUnion fun a ↦ filter p (f a)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ (t.biUnion fun a ↦ {c ∈ s | f c = a}) = s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b : β
⊢ (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b

Tactic:
by grind

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (∅.biUnion f) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)

Tactic:
· simp

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
k : ℕ
⊢ ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length

pp: case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

Tactic:
· simp

Goal state after:
case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion fun x ↦ t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → β
⊢ (s.biUnion fun a ↦ {f a}) = image f s

Tactic:
by grind

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

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'

Tactic:
mem_iff_get,

Goal state after:
case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.cyclicPermutations.get n = l) → l ~r l'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
hn : [].Nodup
⊢ [].cyclicPermutations.Nodup

pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup

Tactic:
· simp

Goal state after:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0

Tactic:
have H₁ {x y z : α} : count (x, y) (map (z, ·) l) = if z = x then count y l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
⊢ s ⊆ image Prod.fst s ×ˢ image Prod.snd s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = s.biUnion fun a ↦ image (fun b ↦ (a, b)) t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ (s ×ˢ t).biUnion f = s.biUnion fun a ↦ t.biUnion fun b ↦ f (a, b)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | p x.1 ∧ q x.2} = filter p s ×ˢ filter q t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s ×ˢ s \ s.diag = s.offDiag

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (s.pi fun a ↦ {f a}) = {fun a x ↦ f a}

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s ×ˢ s \ s.offDiag = s.diag

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.diag = {(a, a)}

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
⊢ ∀ (i : α × α), i ∈ u ↔ (Equiv.prodComm α α) i ∈ v

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
f x✝ : (a : α) → δ a
⊢ (x✝ ∈ piFinset fun i ↦ {f i}) ↔ x✝ ∈ {f}

Tactic:
by grind

Goal state after: