mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ s.bind f ↔ ∃ a, a ∈ s ∧ b ∈ f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).card = (map (card ∘ f) s).sum

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
n : ℕ
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → m.bind f = m.bind g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β β' : Type v
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ m.bind f ≍ m.bind f'

Tactic:
by

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 (m.bind n) = m.bind fun a ↦ map f (n a)

Tactic:
by

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

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

Tactic:
by

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

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
⊢ (filter p s).prod * (filter (fun a ↦ ¬p a) s).prod = s.prod

Tactic:
by

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 : α → β
⊢ ∀ (a : α) (s : Multiset α),
    ((map f s).bind n = s.bind fun a ↦ n (f a)) → (map f (a ::ₘ s)).bind n = (a ::ₘ s).bind fun a ↦ n (f a)

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₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
⊢ False

Tactic:
by

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

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.rotate j
⊢ i % l.length = j % l.length

Tactic:
by

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 γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind f).bind g = s.bind fun a ↦ (f a).bind g) → ((a ::ₘ s).bind f).bind g = (a ::ₘ s).bind fun a ↦ (f a).bind g

Tactic:
by

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

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 ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
⊢ (map f m).prod = f i ^ count i m

Tactic:
by

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 γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind fun a ↦ n.bind fun b ↦ f a b) = n.bind fun b ↦ s.bind fun a ↦ f a b) →
      ((a ::ₘ s).bind fun a ↦ n.bind fun b ↦ f a b) = n.bind fun b ↦ (a ::ₘ s).bind fun a ↦ f a b

Tactic:
by

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

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ s → a' = 1
⊢ s.prod = a ^ count a s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
⊢ ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)

Tactic:
by

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

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

Tactic:
by

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 : α → β → γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind fun a ↦ map (fun b ↦ f a b) n) = n.bind fun b ↦ map (fun a ↦ f a b) s) →
      ((a ::ₘ s).bind fun a ↦ map (fun b ↦ f a b) n) = n.bind fun b ↦ map (fun a ↦ f a b) (a ::ₘ s)

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
h : ∀ (x : M), x ∈ s → x = 1
⊢ s.prod = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset M
hs : s ≠ 0
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
⊢ (map (⇑f) s).prod = f s.prod

Tactic:
by

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
l : List M
⊢ (map ⇑f ⟦l⟧).prod = f (prod ⟦l⟧)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ Function.onFun Disjoint (fun a ↦ {x ∈ s | f x = a}) x' y'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ (filter p m).bind f = m.bind fun a ↦ if p a then f a else 0

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f : α → Multiset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (m.bind f) = m.bind fun a ↦ filter p (f a)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
x✝ : l ~r []
n : ℕ
hn : l.rotate n = []
⊢ l = []

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l = []
⊢ l ~r l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset ι
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
g : ι → M
⊢ (map (fun i ↦ f (g i)) s).prod = f (map g s).prod

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : l.rotate n = [x]
⊢ l = [x]

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
x : α
h : l = [x]
⊢ l ~r l

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
s : Multiset ι
hs : s ≠ 0
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) s).prod = f (map f₁ s).prod (map f₂ s).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : α
⊢ b ∈ t.disjiUnion (fun a ↦ {x ∈ s | f x = a}) ⋯ ↔ b ∈ {c ∈ s | f c ∈ t}

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
s : Multiset ι
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
l : List ι
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) ⟦l⟧).prod = f (map f₁ ⟦l⟧).prod (map f₂ ⟦l⟧).prod

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l.reverse ~r l'.reverse

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ (s.bind t).prod = (map (fun a ↦ (t a).prod) s).prod

Tactic:
by

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
a : ι
m : Multiset ι
ih : (map (fun a ↦ (map (fun b ↦ f a b) n).prod) m).prod = (map (fun b ↦ (map (fun a ↦ f a b) m).prod) n).prod
⊢ (map (fun a ↦ (map (fun b ↦ f a b) n).prod) (a ::ₘ m)).prod =
    (map (fun b ↦ (map (fun a ↦ f a b) (a ::ₘ m)).prod) n).prod

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

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
h : s ≤ t
⊢ s.prod ∣ t.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.disjiUnion singleton ⋯ = s

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
l : List M
a : M
h : a ∈ ⟦l⟧
⊢ a ∣ prod ⟦l⟧

Tactic:
by

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 p (s.bind f) (t.bind g)

Tactic:
by

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

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l' ↔ l ~r l'.reverse

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l'.reverse ↔ l ~r l'

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
⊢ s.disjiUnion (fun a ↦ {f a}) ⋯ = map { toFun := f, inj' := hf } s

Tactic:
by

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

Goal state before:
pp: 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 S).prod ∣ (map g2 S).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
by

Goal state after:
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 f m).prod⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n, n ≤ l.length ∧ l.rotate n = l'

Tactic:
by

Goal state after:
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 f m).prod⁻¹

Tactic:
by
  rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
hf : (↑s).PairwiseDisjoint f
t : Finset β
⊢ Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
by

Goal state after:
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
n : ℤ
⊢ (map (fun i ↦ f i ^ n) m).prod = (map f m).prod ^ n

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset β
t : Finset α
f : α → Finset β
hf : (↑t).PairwiseDisjoint f
⊢ Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a → (f a_1).Nodup) ∧
        Pairwise (Disjoint on f) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))

Tactic:
by

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

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
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
⊢ (↑s).PairwiseDisjoint fun a ↦ (f a).disjUnion (g a) ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ a :: l ~r l ++ [a]

Tactic:
by

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

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
by

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

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
by

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

Goal state before:
pp: α : Type u
L : List α
hL : L ≠ []
⊢ L.getLast hL :: L.dropLast ~r L

Tactic:
by

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

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 β
f✝ : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)

Tactic:
by

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 x ↦ f x - g x) l).sum + (map g l).sum = (map f l).sum

Tactic:
by

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

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
κ : Type u_3
G : Type u_4
M✝ : Type u_5
N : Type u_6
O : Type u_7
M : Type u_8
n : ℕ
hn : n ≠ 0
x y : Multiset M
h : (fun a ↦ n • a) x = (fun a ↦ n • a) y
x✝ : M
⊢ n * count x✝ x = n * count x✝ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
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
⊢ s.disjiUnion (fun a ↦ (f a).disjUnion (g a) ⋯) ⋯ = (s.disjiUnion f hf).disjUnion (s.disjiUnion g hg) ⋯

Tactic:
by

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

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

Tactic:
by

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 : β
⊢ b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ ↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations = (zipWith (fun x1 x2 ↦ x1 ++ x2) l.tails l.inits).dropLast

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
l : List α
⊢ (x :: l).cyclicPermutations.length = l.length + 1

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state after: