mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : LinearOrder α
⊢ #{x | x.1 < x.2} = (card α).choose 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
⊢ s ⊆ image Prod.fst s ×ˢ image Prod.snd s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : γ ↪ δ
s : Finset α
t : Finset γ
⊢ map (f.prodMap g) (s ×ˢ t) = map f s ×ˢ map g t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
by

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

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ 0 < (n - k)! * (k - s)! * s !

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
⊢ (cons m a (f a ⋯) fun a' ha' ↦ f a' ⋯) = f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = s.biUnion fun a ↦ image (fun b ↦ (a, b)) t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
⊢ Infinite ((i : ι) → π i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
⊢ (cons m a (φ b) fun a' ha' ↦ φ (f a' ha')) = fun a' ha' ↦ φ (cons m a b f a' ha')

Tactic:
by

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

Goal state before:
pp: ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
by

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

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
    n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ FactorsThrough f s.domRestrict

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ ∃ g, f = g ∘ s.domRestrict

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
b : β
⊢ DependsOn (fun x ↦ b) ∅

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
hf : DependsOn f ∅
x y : (i : ι) → α i
⊢ ∀ i ∈ ∅, x i = y i

Tactic:
by

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

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - 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 β
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | p x.1 ∧ q x.2} = filter p s ×ˢ filter q t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ s ×ˢ t | p x.1} = filter p s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose k = n ! / (k ! * (n - k)!)

Tactic:
by

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

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j = (i + j)! / (i ! * j !)

Tactic:
choose_eq_factorial_div_factorial (Nat.le_add_left j i),

Goal state after:
i j : ℕ
⊢ (i + j)! / (j ! * (i + j - j)!) = (i + j)! / (i ! * j !)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j = (i + j)! / (i ! * j !)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
⊢ ∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (cons m a b₁ f₁ a_1 ha) (cons m a b₂ f₂ a_1 ha)

Tactic:
by

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

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j * i ! * j ! = (i + j)!

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₁ a' h' = cons s a b f₁ a' this

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !

Tactic:
by

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

Goal state before:
pp: i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₁ a' this = cons s a b f₂ a' this

Tactic:
by

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

Goal state before:
pp: i j : ℕ
⊢ i ! * j ! ∣ (i + j)!

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₂ a' this = f₂ a' h'

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose (n - k) = n.choose k

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : n.choose (n - b) = n.choose b
⊢ n.choose a = n.choose b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
⊢ n.choose a = n.choose b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
by

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

Goal state before:
pp: m : ℕ
⊢ (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
a : α
⊢ {a} ×ˢ t = map { toFun := Prod.mk a, inj' := ⋯ } t

Tactic:
by

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

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

Tactic:
← Nat.add_mul,

Goal state after:
n k : ℕ
⊢ (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
b : β
⊢ s ×ˢ {b} = map { toFun := fun i ↦ (i, b), inj' := ⋯ } s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ cons s a b e₁ e ⋯ = cons s a b e₂ e ⋯

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Nodup (Quotient.map List.offDiag ⋯ s.val)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.diag.Nonempty ↔ s.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.diag = ∅ ↔ s = ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.diag = {a ∈ s ×ˢ s | a.1 = a.2}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α × α → β
s : Finset α
⊢ image f s.diag = image (fun x ↦ f (x, x)) s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.diag = #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s * #s - #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (insert a s).pi t = (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x✝¹ x✝ : Finset α
⊢ x✝¹ ⊆ x✝ → x✝¹.diag ⊆ x✝.diag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.diag ∪ s.offDiag = s ×ˢ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Disjoint s.diag s.offDiag

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s ×ˢ s \ s.diag = s.offDiag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s ×ˢ s \ s.offDiag = s.diag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (s ∩ t).diag = s.diag ∩ t.diag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ ↑(s ∩ t).offDiag = ↑(s.offDiag ∩ t.offDiag)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (s ∪ t).diag = s.diag ∪ t.diag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(s.piDiag ι) = #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ ↑(s ∪ t).offDiag = ↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.offDiag = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.diag = {(a, a)}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
⊢ (insert a s).diag = insert (a, a) s.diag

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
has : a ∉ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
⊢ {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
t : (i : ↥s) → Set (π ↑i)
⊢ s.restrict ⁻¹' Set.univ.pi t = (↑s).pi fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
⊢ Disjoint u v

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝¹ : DecidableEq ι
I : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ I
s : Finset ↑I
u : (i : ↑I) → Set (π ↑i)
⊢ I.domRestrict ⁻¹' (↑s).pi u = (↑(image Subtype.val s)).pi fun i ↦ if h : i ∈ I then u ⟨i, h⟩ else Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
⊢ u.disjUnion v disj = s.offDiag

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
s t : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
hst : s ⊆ t
u : (i : ↥s) → Set (π ↑i)
⊢ restrict₂ hst ⁻¹' Set.univ.pi u = Set.univ.pi fun j ↦ if h : ↑j ∈ s then u ⟨↑j, h⟩ else Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
⊢ ∀ (i : α × α), i ∈ u ↔ (Equiv.prodComm α α) i ∈ v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
⊢ #({x ∈ s ×ˢ s | x.1 < x.2}) = (#s).choose 2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
s : (a : α) → Finset (γ a)
t : (a : α) → Finset (δ a)
x✝¹ x✝ : (a : α) → a ∈ univ → δ a
⊢ (fun f a ↦ f a ⋯) x✝¹ = (fun f a ↦ f a ⋯) x✝ → x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.univ.pi fun a ↦ ↑(t a)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ piFinset s = ∅ ↔ ∃ i, s i = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : Nonempty α
⊢ (piFinset fun x ↦ ∅) = ∅

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ (piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
inst✝ : IsEmpty α
s : (a : α) → Finset (γ a)
x✝ : (a : α) → γ a
⊢ x✝ ∈ piFinset s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
f x✝ : (a : α) → δ a
⊢ (x✝ ∈ piFinset fun i ↦ {f i}) ↔ x✝ ∈ {f}

Tactic:
by

Goal state after: