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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
n k : ℕ
⊢ ((replicate n a).rotate k).length = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
by

Goal state after:
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
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as)
        (match false 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:
simp only

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
by

Goal state after:
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
x✝¹ : α
h : x✝¹ ≠ a
x✝ : x✝¹ ∈ filter p (a :: as).dedup
⊢ (if a = x✝¹ then 1 else 0) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state after:
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
⊢ 0 = if p a = true then 1 else 0

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
as m : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
hm : IsChain (fun x1 x2 ↦ x1 > x2) m
hmas : m ≤ as
⊢ IsChain (fun x1 x2 ↦ x1 > x2) (a :: m)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
⊢ (map (fun x ↦ count x l) l.dedup).sum = l.length

Tactic:
by

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

Goal state before:
pp: α : Type u_3
R : α → α → Prop
l : List α
v : α
hl : IsChain R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ IsChain R (v :: l)

Tactic:
by

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

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

Goal state before:
pp: a : ℕ
l : List ℕ
⊢ (a :: l).ranges.flatten = range (a :: l).sum

Tactic:
by

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

Goal state before:
pp: l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l.ranges.flatten

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
⊢ a ∈ s

Tactic:
by

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

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum

Tactic:
by

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

Goal state before:
pp: α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ i < l.length

Tactic:
by

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

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ take i (map length L) = take i (map length (take (i + 1) L))

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)

Tactic:
by

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

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

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Tactic:
by

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

Goal state before:
pp: l : List ℤ
h : l.prod = -1
⊢ -1 ≠ 1

Tactic:
by

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

Goal state before:
pp: l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 * -1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ a ∈ n • s ↔ a ∈ s

Tactic:
by

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

Goal state before:
pp: l : List ℤ
h : l.prod = -1
⊢ -1 ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • (a ::ₘ s) = n • {a} + n • s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ n • {a} = replicate n a

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ l.prod

Tactic:
by

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₁.prod ∣ l₂.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
hi : i < l.length
⊢ f^[i] l[0] = l[i]

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
n : ℕ
a : α
h : r a a
⊢ IsChain r (replicate n a)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m - l.length < l.length

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ IsChain (fun x1 x2 ↦ x1 = x2) (a :: l) ↔ l = replicate l.length a

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s

Tactic:
by

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
⊢ List.Pairwise rᶜ l.reverse

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ countP p (n • s) = n * countP p s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
⊢ (n • s).dedup = s.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
by

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length

Tactic:
rw [mul_comm, ← div_eq_mul_inv, div_zpow]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (l.rotate n)[m]? = l[(m + n) % l.length]?

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ s.card • t ↔ s ⊆ t

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
⊢ ∀ (l : List M), op l.prod = (map op l).reverse.prod

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
k : Fin (l.rotate n).length
⊢ (l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f = g

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop l.prod = (map unop l).reverse.prod

Tactic:
by

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

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ MulOpposite.unop (f l.prod) = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l)[n] = (replicate (a :: l).length a)[n]

Tactic:
by

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

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ (a :: l).rotate n = a :: l

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate n.succ = l

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ (drop (n % l.length) l).length = (drop (n % l'.length) l').length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.IsChain (flip r) (a :: l)
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ Injective fun l ↦ l.rotate n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ l = ↑l'

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ l = [x]

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = l.rotate n ↔ [x] = l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))

Tactic:
rw [← length_reverse]

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
l : List α
L : List (List α)
⊢ (↑(List.map ofList (l :: L))).join = ↑(l :: L).flatten

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ ∀ (a_1 : Multiset α) (s : Multiset (Multiset α)),
    (a ∈ s.join ↔ ∃ s_1, s_1 ∈ s ∧ a ∈ s_1) → (a ∈ (a_1 ::ₘ s).join ↔ ∃ s_1, s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a
⊢ Acc (List.lex_chains r) l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
⊢ map f S.join = (map (map f) S).join

Tactic:
by

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * (s.erase a).prod = s.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
S : Multiset (Multiset α)
⊢ S.join.prod = (map prod S).prod

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
b : β
h : (↑s).PairwiseDisjoint t
⊢ b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f (m.erase a)).prod = (map f m).prod

Tactic:
by

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

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s t : Multiset M
l₁ l₂ : List M
⊢ (⟦l₁⟧ + ⟦l₂⟧).prod = prod ⟦l₁⟧ * prod ⟦l₂⟧

Tactic:
by

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 < n % (x :: l).reverse.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = ↑(List.flatMap f l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
a : α
s : Multiset α
f : α → Multiset β
⊢ (a ::ₘ s).bind f = f a + s.bind f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
a : α
f : α → Multiset β
⊢ {a}.bind f = f a

Tactic:
by

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ (0 • m).prod = m.prod ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s t : Multiset α
f : α → Multiset β
⊢ (s + t).bind f = s.bind f + t.bind f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
⊢ (s.bind fun x ↦ 0) = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (bind 0 fun x ↦ {f x}) = map f 0

Tactic:
by

Goal state after: