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

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

pp: α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length

Tactic:
]

Goal state after:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

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

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ a = a

Tactic:
]

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

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

Tactic:
]

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
⊢ (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
]

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[((l.length - n % l.length + k) % l.length + n) % l.length]

Tactic:
]

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = l[((l.length - n % l.length + k) % l.length + n) % l.length]
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = k

pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length

Tactic:
]

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length
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
⊢ some a = some a

Tactic:
]

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
⊢ replicate (a :: l).length b = replicate (a :: l).length b

Tactic:
]

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 1 = l

Tactic:
]

Goal state after:
α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate 1 = l
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : 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⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
apply Acc.intro; rintro ⟨_⟩ ⟨_⟩

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 = l'.rotate n
hle : l.length = l'.length
⊢ l = l'

Tactic:
rotate_eq_drop_append_take_mod

Goal state after:
α : 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
⊢ l = l'
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
⊢ l = l'

Tactic:
]

Goal state after:
α : 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
⊢ l = l'
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
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l' = l'

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = [] ↔ l.rotate n = []

Tactic:
]

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

Goal state before:
pp: case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'

pp: case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length

Tactic:
]

Goal state after:
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro
α : 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'
⊢ ∀ (hl : List.IsChain (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩

Tactic:
]

Goal state after:
case cons.intro
α : 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'
⊢ ∀ (hl : List.IsChain (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩
Module: Mathlib.Data.List.Rotate

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse.rotate n = l.reverse
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:
]

Goal state after:
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
Module: Mathlib.Data.List.Rotate

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

Tactic:
]

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

Goal state before:
pp: case cons.intro.intro.nil.nil
α : 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' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
hm : List.IsChain (flip r) []
⊢ Acc (List.lex_chains r) ⟨[], hm⟩

Tactic:
apply Acc.intro; rintro ⟨_⟩ ⟨_⟩

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

Goal state before:
pp: α : 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))

Tactic:
]

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.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
⊢ s.toList.prod = s.toList.prod

Tactic:
]

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

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

pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).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.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Tactic:
]

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

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
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
⊢ (List.map f m.toList).prod = (List.map f m.toList).prod

Tactic:
]

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.map (ofList ∘ f) l)).join

Tactic:
]

Goal state after:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ prod 0 = 1

Tactic:
]

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ prod 0 = 1
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ m.prod ^ n * m.prod = m.prod ^ n * m.prod

Tactic:
]

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
p : M → Prop
inst✝ : DecidablePred p
⊢ s.prod = s.prod

Tactic:
]

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length

Tactic:
]

Goal state after:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate (i % l.length) = l.rotate (j % l.length)
⊢ i % l.length = j % l.length
Module: Mathlib.Data.List.Rotate

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ hd :: tl = hd :: tl

pp: case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n

Tactic:
]

Goal state after:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n
Module: Mathlib.Data.List.Rotate

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

Tactic:
]

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

Goal state before:
pp: α : Type u
l : List α
⊢ [] = l ↔ [] = l

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b ↦ Rel p (f a) (g b)) s t

Tactic:
]

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b ↦ Rel p (f a) (g b)) s t
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (f x) + m'.sum

Tactic:
]

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (f x) + m'.sum
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ (map (fun i ↦ (f i)⁻¹) m).prod = (map (fun x ↦ (f x)⁻¹) m).prod

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).rotate n

Tactic:
]

Goal state after:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).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
⊢ ∀ i ∈ s, Disjoint (f i) (s.disjiUnion g hg)

Tactic:
disjoint_disjiUnion_right

Goal state after:
α : 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
⊢ ∀ i ∈ s, ∀ i_1 ∈ s, Disjoint (f i) (g i_1)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op b₀ 0 = fold op b₀ 0

Tactic:
]

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ (map (fun i ↦ f i - g i + g i) l).sum = (map f l).sum

Tactic:
]

Goal state after:
ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ (map (fun i ↦ f i - g i + g i) l).sum = (map f l).sum
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha))

Tactic:
]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) s)

Tactic:
induction s using Multiset.induction_on with
  | empty => rw [zero_bind, map_zero, map_zero, fold_zero]
  | cons a ha ih => rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]

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
⊢ drop n (a :: l) ++ take n (a :: l) = drop n (a :: l) ++ take n (a :: l)

Tactic:
]

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

Goal state after:
α : 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₂)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
]

Goal state after:
α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l = l

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ b a, b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ b a, b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ some l = some l

Tactic:
]

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

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

pp: case cons.h
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate k ≠ []

Tactic:
]

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

case cons.h
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate k ≠ []
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a ↦ ↑(List.map (Sigma.mk a) (l₂ a))

Tactic:
]

Goal state after:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a ↦ ↑(List.map (Sigma.mk a) (l₂ a))
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
]

Goal state after:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
Module: Mathlib.Data.List.Rotate

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

Tactic:
]

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations

Tactic:
]

Goal state after:
case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ Injective l.cyclicPermutations.get

Tactic:
]

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

Goal state before:
pp: case pos
α : 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
x y z : α
h : z = x
⊢ count y l = count y l

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ (n - 1).choose l + (n - 1).choose (l + 1) = (n - 1).choose l + (n - 1).choose (l + 1)

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ 0 + 0 = 0

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
]

Goal state after:
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : 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
x y z : α
h : z = y
⊢ count x l = count x l

Tactic:
]

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

Goal state before:
pp: case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
]

Goal state after:
case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0

Tactic:
]

Goal state after:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1) * (n + 1).choose (k + 1)

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
⊢ n.choose k * k.succ ! * (n - k)! = (k + 1) * (n.choose k * k ! * (n - k)!)

Tactic:
]

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
⊢ n.choose k * k.succ ! * (n - k)! = (k + 1) * (n.choose k * k ! * (n - k)!)