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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
⊢ snoc p x (last n) = x

Tactic:
by simp [snoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
H : l.Nodup
x : { x // x ∈ l }
⊢ (fun i ↦ ⟨l.get i, ⋯⟩) ((fun x ↦ ⟨idxOf (↑x) l, ⋯⟩) x) = x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
nd : l.Nodup
h : ∀ (x : α), x ∈ l
a : α
⊢ (fun i ↦ l.get i) ((fun a ↦ ⟨idxOf a l, ⋯⟩) a) = a

Tactic:
by simp

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
x : α✝ (last n)
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.castSucc
i : Fin n
y : α✝ i.castSucc
z : α✝ (last n)
α : Fin (n + 1) → Type u_2
f : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ (fun f ↦ (f (last n), init f)) ((fun f x ↦ snoc f.2 f.1 x) f) = f

Tactic:
by simp

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
x : α✝ (last n)
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.castSucc
i : Fin n
y : α✝ i.castSucc
z : α✝ (last n)
α : Fin (n + 1) → Type u_2
f : (i : Fin (n + 1)) → α i
⊢ (fun f x ↦ snoc f.2 f.1 x) ((fun f ↦ (f (last n), init f)) f) = f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
x✝ : ℕ
⊢ ∀ ⦃b : ℕ⦄, x✝ < b → (fun x ↦ x + 1) x✝ < (fun x ↦ x + 1) b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
a : α
inst✝ : Infinite (β a)
x✝¹ x✝ : β a
⊢ (fun x ↦ ⟨a, x⟩) x✝¹ = (fun x ↦ ⟨a, x⟩) x✝ → x✝¹ = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
h : {x | p x}.Finite
⊢ h.toFinset = {x | p x}

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ x = cons x (fun j ↦ cast ⋯ (p j)) 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ s.toFinset ∪ t.toFinset ↔ x ∈ s ∪ t

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ {a ∈ s.toFinset | p a} ↔ x ∈ {a | a ∈ s ∧ p a}

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ s.toFinset ∩ t.toFinset ↔ x ∈ s ∩ t

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
⊢ ∀ (x : α), x ∈ {a ∈ s.toFinset | a ∈ t} ↔ x ∈ s ∩ t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
duplicate_iff_two_le_count,

Goal state after:
α : Type u_1
l : List α
x : α
⊢ 2 ≤ count x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑t
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (x : α), x ∈ {a ∈ t.toFinset | a ∈ s} ↔ x ∈ s ∩ t

Tactic:
by simp [and_comm]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ x = snoc (fun j ↦ cast ⋯ (p j)) x (last n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ s.toFinset \ t.toFinset ↔ x ∈ s \ t

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ ∀ (x : α), x ∈ ∅ ↔ x ∈ ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
⊢ ∀ (x : α), x ∈ {a} ↔ x ∈ {a}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ 0 < (replicate 2 x).length

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ ∀ (x : α), x ∈ insert a s.toFinset ↔ x ∈ insert a s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ 1 < (replicate 2 x).length

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ ∀ (x : α), x ∈ { val := a ::ₘ s.toFinset.val, nodup := ⋯ } ↔ x ∈ insert a s

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
s : Set α
f : α → β
inst✝ : Fintype ↑s
⊢ ∀ (x : β), x ∈ Finset.image f s.toFinset ↔ x ∈ f '' s

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ ∀ (x : ℕ), x ∈ Finset.range n ↔ x ∈ {i | i < n}

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ ↑hs.toFinset = s

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
x✝ : Finset α
⊢ (fun s ↦ ⋯.toFinset) ((fun s ↦ ⟨↑s, ⋯⟩) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
x✝ : { s // s.Finite }
⊢ (fun s ↦ ⟨↑s, ⋯⟩) ((fun s ↦ ⋯.toFinset) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Set α
a : α
hs : (insert a s).Finite
⊢ ∀ (a_1 : α), a_1 ∈ hs.toFinset ↔ a_1 ∈ insert a ⋯.toFinset

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
⊢ p.insertNth (f p) (p.removeNth f) = f

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0

Tactic:
by simp

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : (i : Fin (n + 1)) → α i
⊢ (fun f ↦ p.insertNth f.1 f.2) ((fun f ↦ (f p, p.removeNth f)) f) = f

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
← card_fintypeInsertOfNotMem s h

Goal state after:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Fintype ↑s
f : α → β
inst✝ : Fintype ↑(f '' s)
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
this : (a : Prop) → Decidable a
⊢ ∀ (x : β), x ∈ Finset.image f s.toFinset ↔ x ∈ f '' s

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
n : ℕ
⊢ ↑(Finset.map (Embedding.subtype fun x ↦ x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) ⊆ s ∧
    (Finset.map (Embedding.subtype fun x ↦ x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))).card = n

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ ∀ ⦃i j : ℕ⦄ ⦃hi : i < (finRange n).length⦄ ⦃hj : j < (finRange n).length⦄, i < j → (finRange n)[i] < (finRange n)[j]

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
i : Fin n
⊢ i ∈ find? p ↔ p i = true ∧ ∀ (j : Fin n), j < i → ¬p j = true

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
change _ > _ ↔ _

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
change _ > _ ↔ _

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
ha : a ∈ head✝ :: tail✝
⊢ R (head✝ :: tail✝).head! a

Tactic:
· cases ha with
    | head => exact refl_of ..
    | tail => exact rel_of_pairwise_cons h (by assumption)

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

Goal state before:
pp: n m i : ℕ
H : i < (range' n m).length
⊢ (range' n m)[i] = n + i

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
exact Decidable.List.Lex.ne_iff H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length

Tactic:
induction l₁ with

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

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ [] ++ [a, b] ++ l = a :: b :: l

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
a b : α
l : List α
x✝¹ x✝ : α
h : [x✝¹, x✝] <:+: b :: l
⊢ [a] ++ b :: l ++ [] = a :: b :: l

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
⊢ IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l

Tactic:
by
  cases l <;> simp [isChain_iff_forall₂]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
head✝² head✝¹ head✝ : α
tail✝ : List α
h : IsChain R (head✝² :: head✝¹ :: head✝ :: tail✝)
hne : (head✝² :: head✝¹ :: head✝ :: tail✝).dropLast ≠ []
⊢ (head✝² :: head✝¹ :: head✝ :: tail✝).tail.dropLast ≠ []

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R ([] ++ l) ↔ IsChain R [] ∧ IsChain R l ∧ ∀ (x : α), x ∈ [].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : IsChain R (head✝² :: head✝¹ :: tail✝¹ ++ head✝ :: tail✝)
h₁ : head✝² :: head✝¹ :: tail✝¹ ≠ []
h₂ : head✝ :: tail✝ ≠ []
⊢ head✝¹ :: tail✝¹ ≠ []

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : IsChain R (head✝² :: head✝¹ :: tail✝¹ ++ head✝ :: tail✝)
h₁ : head✝² :: head✝¹ :: tail✝¹ ≠ []
h₂ : head✝ :: tail✝ ≠ []
⊢ head✝ :: tail✝ ≠ []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ [].rotate' n = []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x✝ : ℕ
⊢ ([].rotate' x✝).length = [].length

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x✝ : ∀ (m : M), m ∈ [] → IsUnit m
⊢ IsUnit [].prod

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x✝ : ¬[] ∈ []
⊢ IsChain R [].flatten ↔
    (∀ (l : List α), l ∈ [] → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≤ [].length
⊢ [].rotate' n = drop n [] ++ take n []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
h : 0 ≤ l.length
⊢ l.rotate' 0 = drop 0 l ++ take 0 l

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
x✝¹ : [].prod = 1
x✝ : ℕ
⊢ ([].rotate x✝).prod = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ 0 < (a :: l).length

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n m : ℕ
⊢ ([].rotate' n).rotate' m = [].rotate' (n + m)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate' (l.length * 0) = l

Tactic:
by simp

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

Goal state before:
pp: α : Type u
x✝ : α
n : ℕ
⊢ x✝ ∈ [].rotate n ↔ x✝ ∈ []

Tactic:
by simp

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

Goal state before:
pp: α : Type u
a : α
l : List α
x✝ : α
⊢ x✝ ∈ (a :: l).rotate 0 ↔ x✝ ∈ a :: l

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
σ : α → Type u_8
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (l₁.sigma l₂).length = (map (fun a ↦ (l₂ a).length) l₁).sum

Tactic:
induction l₁ with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ (l₁ ++ l).prod

Tactic:
prod_append

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n).head? = l[n]?

Tactic:
head?_eq_getElem?,

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n)[0]? = l[n]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
⊢ (∀ (n : ℕ), [].rotate n = []) ↔ ∃ a, [] = replicate [].length a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ a ∈ join 0 ↔ ∃ s, s ∈ 0 ∧ a ∈ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
S : Multiset (Multiset α)
⊢ (join 0).card = (map card 0).sum

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
S : Multiset (Multiset α)
⊢ ∀ (a : Multiset α) (s : Multiset (Multiset α)),
    s.join.card = (map card s).sum → (a ::ₘ s).join.card = (map card (a ::ₘ s)).sum

Tactic:
by simp

Goal state after:
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₂ t : α → Finset β
⊢ (↑∅).PairwiseDisjoint t

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < (x :: l).reverse.length

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ (bind 0 fun a ↦ f a ::ₘ g a) = map f 0 + bind 0 g

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ (map f 0).bind n = bind 0 fun a ↦ n (f a)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ (bind 0 f).bind g = bind 0 fun a ↦ (f a).bind g

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ (bind 0 fun a ↦ n.bind fun b ↦ f a b) = n.bind fun b ↦ bind 0 fun a ↦ f a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ (bind 0 fun a ↦ map (fun b ↦ f a b) n) = n.bind fun b ↦ map (fun a ↦ f a b) 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate 0 = l

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < (hd :: tl).length

Tactic:
by simp

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

Goal state before:
pp: α : Type u
hd : α
tl : List α
⊢ (hd :: tl).rotate 1 = tl ++ [hd]

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
M : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
n : Multiset κ
f : ι → κ → M
⊢ (map (fun a ↦ (map (fun b ↦ f a b) n).prod) 0).prod = (map (fun b ↦ (map (fun a ↦ f a b) 0).prod) n).prod

Tactic:
by simp

Goal state after:
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 β
s : Finset α
x✝¹ : α
x✝ : x✝¹ ∈ ↑s
⊢ ∀ ⦃y : α⦄, y ∈ ↑s → x✝¹ ≠ y → Function.onFun Disjoint singleton x✝¹ y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (map f 0).sum = (map (fun b ↦ count a (f b)) 0).sum

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ ∀ (a_1 : β) (s : Multiset β),
    count a (map f s).sum = (map (fun b ↦ count a (f b)) s).sum →
      count a (map f (a_1 ::ₘ s)).sum = (map (fun b ↦ count a (f b)) (a_1 ::ₘ s)).sum

Tactic:
by simp

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

Goal state before:
pp: M : Type u_5
s : Multiset M
⊢ (map (fun a ↦ {a}) 0).sum = 0

Tactic:
by simp

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

Goal state before:
pp: M : Type u_5
s : Multiset M
⊢ ∀ (a : M) (s : Multiset M), (map (fun a ↦ {a}) s).sum = s → (map (fun a ↦ {a}) (a ::ₘ s)).sum = a ::ₘ s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
L : List α
hL : [] ≠ []
hL' : [].head hL = [].getLast hL
⊢ [].dropLast ~r [].tail

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
L : List α
head✝ : α
hL : [head✝] ≠ []
hL' : [head✝].head hL = [head✝].getLast hL
⊢ [head✝].dropLast ~r [head✝].tail

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l : List α
p : α × ℕ → Prop
⊢ (∀ (i : ℕ) (x : i < l.length), p (l[i], 0 + i)) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], i)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
l : List α
p : α × ℕ → Prop
⊢ (∃ i x, p (l[i], 0 + i)) ↔ ∃ i x, p (l[i], i)

Tactic:
by simp

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

Goal state before:
pp: case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ (a :: l).cyclicPermutations[n] = (a :: l).rotate n

Tactic:
simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]

Goal state after:
case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
k : ℕ
⊢ l.cyclicPermutations.rotate k = (l.rotate k).cyclicPermutations

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
x✝ : 0 ≤ n + 1
⊢ 0 < (n + 1).choose 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
x✝ : 0 ≤ n + 1
⊢ (n + 1).choose 0 * 0! * (n + 1 - 0)! = (n + 1)!

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑s.offDiag
⊢ ∀ (a : α × α), a ∈ s.offDiag.toFinset ↔ a ∈ s.toFinset.offDiag

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ univ ×ˢ univ

Tactic:
by simp

Goal state after: