mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
a : α
⊢ (insert a s).biUnion t = t a ∪ s.biUnion t

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations.length = l.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
⊢ s₁.biUnion t₁ = s₂.biUnion t₂

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
h : (a :: l).cyclicPermutations = []
⊢ False

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' : Finset β
⊢ s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Finset β
inst✝ : DecidableEq β
a : α
⊢ {a}.biUnion t = t a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g

Tactic:
by

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

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ (a :: l).length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
s : Multiset α
t : α → Multiset β
x : β
⊢ x ∈ (s.bind t).toFinset ↔ x ∈ s.toFinset.biUnion fun a ↦ (t a).toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst✝ : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
⊢ s₁.biUnion t ⊆ s₂.biUnion t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
u : α → Finset β
x : α
xs : x ∈ s
⊢ u x ⊆ s.biUnion u

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → Finset β
⊢ s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.biUnion singleton = s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (s.biUnion f) = s.biUnion fun a ↦ filter p (f a)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
⊢ s ×ˢ 0 = 0

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
b : β
s : Multiset α
t : Multiset β
⊢ s ×ˢ (b ::ₘ t) = map (fun a ↦ (a, b)) s + s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Finset β
s : Finset α
b : β
⊢ (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.cyclicPermutations.head ⋯ = l

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).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.cyclicPermutations.head? = some l

Tactic:
by

Goal state after:
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 β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
by

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

Goal state before:
pp: α : Type u
l l' : List α
h : l.cyclicPermutations = l'.cyclicPermutations
⊢ l = l'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ (s ×ˢ t).card = s.card * t.card

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b).1 ∈ s ∧ (a, b).2 ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup ⟦l₁⟧
d₂ : Nodup ⟦l₂⟧
⊢ (⟦l₁⟧ ×ˢ ⟦l₂⟧).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
⊢ (map f (s ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s).prod

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (a ::ₘ s).sigma t = map (Sigma.mk a) (t a) + s.sigma t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ (s + t).sigma u = s.sigma u + t.sigma u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

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 : α → Finset β
⊢ Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
f : α → β
s✝ : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : (image f s).biUnion t = s.biUnion fun a ↦ t (f a)
⊢ (image f (insert a s)).biUnion t = (insert a s).biUnion fun a ↦ t (f a)

Tactic:
by

Goal state after:
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)
⊢ ((a ::ₘ s).sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (s.sigma t).card = (map (fun a ↦ (t a).card) s).sum

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s✝ : Finset α
t : α → Finset β
f : β → γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : image f (s.biUnion t) = s.biUnion fun a ↦ image f (t a)
⊢ image f ((insert a s).biUnion t) = (insert a s).biUnion fun a ↦ image f (t a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ s.sigma t ↔ ⟨a, b⟩.fst ∈ s ∧ ⟨a, b⟩.snd ∈ t ⟨a, b⟩.fst

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
⊢ (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion fun x ↦ t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → β
⊢ (s.biUnion fun a ↦ {f a}) = image f s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → Finset β
⊢ (s.attach.biUnion fun x ↦ f ↑x) = s.biUnion f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : ↥s → Finset β
⊢ s.attach.biUnion f = s.biUnion fun a ↦ if h : a ∈ s then f ⟨a, h⟩ else ∅

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
hn : l.Nodup
⊢ l.cyclicPermutations.Nodup

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.choose 0 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ map (fun x ↦ (x.fst, a)) l.zipIdx = map (fun x ↦ (x, a)) l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).offDiag ~ map (fun x ↦ (a, x)) l ++ map (fun x ↦ (x, a)) l ++ l.offDiag

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.offDiag.length = l.length * (l.length - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.offDiag.length = l.length ^ 2 - l.length

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
x : α × α
⊢ x ∈ l.offDiag ↔ ∃ i x_1 j x_2, i ≠ j ∧ l[i] = x.fst ∧ l[j] = x.snd

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ Function.Injective fun x_1 ↦ (x, x_1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : 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 : α
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.choose n = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.choose 1 = n

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ Function.Injective fun x ↦ (x, y)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : 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 : α
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n k : ℕ
⊢ ¬n.choose k ≠ 0 ↔ ¬k ≤ n

Tactic:
by

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

Goal state before:
pp: ⊢ (0 + 1) * choose 0 0 = (0 + 1).choose (0 + 1) * (0 + 1)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ choose 0 x✝ * x✝! * (0 - x✝)! = 0!

Tactic:
by

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

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

Tactic:
by

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 !

Tactic:
by

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
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k)! = (n - k) * (n - k.succ)!

Tactic:
by

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
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
⊢ count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁.offDiag ~ l₂.offDiag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ l.offDiag.Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
this✝ : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
this : 1 + List.count a l < List.count a l * List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 1 + List.count a l < List.count a l + List.count a l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ List.count a l + List.count a l ≤ List.count a l * List.count a l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.offDiag.Nodup
⊢ l.Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x : α × α
⊢ x ∈ l.offDiag ↔ x.fst ∈ l ∧ x.snd ∈ l ∧ x.fst ≠ x.snd

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map (Prod.map f f) l.offDiag = (map f l).offDiag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
⊢ (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
← Nat.add_mul,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + (1 + n) * n ! - k * n ! = (n + 1) * n !
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
⊢ image Prod.fst (s ×ˢ t) = s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
⊢ image Prod.snd (s ×ˢ t) = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
s : Finset α
t : Finset β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ (a'' ∈ a ::ₘ a' ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) ≍ cons (a ::ₘ m) a' b' (cons m a b f)

Tactic:
by

Goal state after: