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

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

Tactic:
simp

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

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

Tactic:
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:
simp

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

Goal state before:
pp: n : ℕ
α : Type u_3
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthEquiv (fun x ↦ α) (last n)) x✝¹ x✝ = (snocEquiv fun x ↦ α) x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
c : β
h : op c (op b c) = op b c
hd : Decidable (∅ = ∅)
⊢ fold op b (fun x ↦ c) ∅ = if ∅ = ∅ then b else op b c

Tactic:
simp

Goal state after:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∧ ∀ x ∈ ∅, r c (f x)

Tactic:
simp

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

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
j.succAbove_of_le_castSucc,

Goal state after:
case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g k.succ

case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∨ ∃ x ∈ ∅, r c (f x)

Tactic:
simp

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
simp

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

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ [a, b]

Tactic:
simp

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

Goal state before:
pp: case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Tactic:
simp

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

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

Goal state before:
pp: case zero
r : ℕ → ℕ → Prop
⊢ IsChain r (range 0) ↔ ∀ (m : ℕ), m < 0 - 1 → r m m.succ

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs

Tactic:
simp

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

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

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

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

Tactic:
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:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
simp

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

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

Tactic:
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:
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:
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:
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:
simp

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l

Tactic:
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:
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:
simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ drop l.length l ++ take l.length l = l

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
⊢ (map (fun x ↦ count x []) (filter p [].dedup)).sum = countP p []

Tactic:
simp

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

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

Tactic:
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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ l.rotate' 0 ~ l

Tactic:
simp

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) ~ []

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ l.rotate 0 = [] ↔ l = []

Tactic:
simp

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) = [] ↔ [] = []

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type u_1
f : α → α → β
x y : α
l : List α
⊢ zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x])

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: case nil
α : Type u_1
⊢ IsChain (fun x1 x2 ↦ x1 = x2) [] ↔ ∀ (a : α), a ∈ [].head? → [] = replicate [].length a

Tactic:
simp

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

Goal state before:
pp: case singleton
α : Type u_1
x✝ : α
⊢ IsChain (fun x1 x2 ↦ x1 = x2) [x✝] ↔ ∀ (a : α), a ∈ [x✝].head? → [x✝] = replicate [x✝].length a

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ (l.rotate 0).reverse.rotate 0 = l.reverse

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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))

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β
⊢ map f (join 0) = (map (map f) 0).join

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : CommMonoid α
⊢ (join 0).prod = (map prod 0).prod

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p (join 0) = (map (filter p) 0).join

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → Option β
⊢ filterMap f (join 0) = (map (filterMap f) 0).join

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case zero
α : Type u
β : Type u_1
f : α → β
l : List α
⊢ map f (l.rotate 0) = (map f l).rotate 0

Tactic:
simp

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)

Tactic:
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:
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:
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:
simp

Goal state after:
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 ∨ [] = []

Tactic:
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:
simp

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

Goal state before:
pp: case empty
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = bind 0 fun a ↦ if p a then {a} else 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : p a
⊢ {a}.bind f = f a

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : ¬p a
⊢ bind 0 f = 0

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → Option β
⊢ filterMap f 0 = bind 0 fun a ↦ (Option.map singleton (f a)).getD 0

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ ((Option.map singleton none).getD 0).bind g = (Option.map g none).getD 0

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
b : β
⊢ ((Option.map singleton (some b)).getD 0).bind g = (Option.map g (some b)).getD 0

Tactic:
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:
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:
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:
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:
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:
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:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
simp

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

Goal state before:
pp: case e_c
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (x ∈ s.dedup.bind f) = (x ∈ s.bind f)

Tactic:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case nil
α : Type u
n : ℕ
h : n < [].cyclicPermutations.length
⊢ [].cyclicPermutations[n] = [].rotate n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = (↑l₁).bind fun a ↦ ↑(List.map (Prod.mk a) l₂)

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
n : Fin l.cyclicPermutations.length
⊢ l.cyclicPermutations.get n = l.rotate ↑n

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
k : Fin l.cyclicPermutations.length
h : l.cyclicPermutations.get k ∈ l.cyclicPermutations
⊢ (l.cyclicPermutations.get k).length = l.length

Tactic:
simp

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

Tactic:
simp

Goal state after: