mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ a ∈ fixedPoints ⇑f ∧ fixedPoints ⇑f ⊆ {a} ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ a ∈ fixedPoints ⇑f ∧ fixedPoints ⇑f ⊆ {a} ↔ a ∈ fixedPoints ⇑f ∧ ∀ x ∈ fixedPoints ⇑f, x = a
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
a : G
ha : a ∈ A
⊢ A * A = A * A

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ ∀ (x : α), x ∉ fixedPoints ⇑f

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ ∀ (x : α), x ∉ fixedPoints ⇑f
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ a_1 ∈ fixedPoints ⇑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ⇑x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ a_1 ∈ fixedPoints ⇑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ⇑x
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ = 0

Tactic:
]

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ = 0
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), x ∉ fiber none

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), x ∉ fiber none
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
x a : G
ha : a ∈ A
⊢ a * x ∈ A ↔ a * x ∈ A

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F ∈ derangements (Option α), F none = none ∧ removeNone F = f
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F ∈ derangements (Option α), F none = none ∧ removeNone F = f
⊢ False
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : s = univ
⊢ s.biUnion t = univ

Tactic:
]

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : s = univ
⊢ s.biUnion t = univ
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : s = univ
⊢ univ.biUnion t = univ

Tactic:
]

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : s = univ
⊢ univ.biUnion t = univ
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : ∀ (x : L), x ∈ s
⊢ ∀ (x : P), x ∈ univ.biUnion t

Tactic:
]

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : ∀ (x : L), x ∈ s
⊢ ∀ (x : P), x ∈ univ.biUnion t
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ (∃ F ∈ derangements (Option α), F none = some a ∧ removeNone F = f) → f ∈ {f | fixedPoints ⇑f ⊆ {a}}

Tactic:
]

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ (∃ F ∈ derangements (Option α), F none = some a ∧ removeNone F = f) → f ∈ {f | fixedPoints ⇑f ⊆ {a}}
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : (removeNone F) x = x
⊢ x ∈ {a}

Tactic:
]

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : (removeNone F) x = x
⊢ x ∈ {a}
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
⊢ a * x ∈ ↑A ↔ x ∈ ↑H

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
⊢ a * x ∈ ↑A ↔ x ∈ ↑H
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp.none
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : x = a
Fx : F (some x) = none
⊢ x ∈ {a}

Tactic:
]

Goal state after:
case mp.none
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : x = a
Fx : F (some x) = none
⊢ x ∈ {a}
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp.some
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : F (some x) = some x
y : α
Fx : F (some x) = some y
⊢ False

Tactic:
]

Goal state after:
case mp.some
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : F (some x) = some x
y : α
Fx : F (some x) = some y
⊢ False
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ card (Fin (n + 1)) - card ↑{a} = card (Fin n)

Tactic:
]

Goal state after:
n : ℕ
a : Fin (n + 1)
⊢ card (Fin (n + 1)) - card ↑{a} = card (Fin n)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }

Tactic:
]

Goal state after:
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ a ∈ A

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : x ∈ ↑H
⊢ a ∈ A
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ (n + 1) * numDerangements n + (n + 1) * numDerangements (n + 1) =
    (n + 1) * numDerangements n + (n + 1) * numDerangements (n + 1)

pp: case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n + 1 < n + 1 + 1

pp: case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 1

Tactic:
]

Goal state after:
case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n + 1 < n + 1 + 1

case ind.succ.succ.a
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ n < n + 1 + 1
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ x, lineCount L ({ toFun := f, inj' := hf₁ } x)

Tactic:
]

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ l, lineCount L (f l) = ∑ x, lineCount L ({ toFun := f, inj' := hf₁ } x)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f a) ≠ none

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f a) ≠ none
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case refine_2
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ a, f a = p
⊢ Nonempty { l // p ∈ l }

Tactic:
]

Goal state after:
case refine_2
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ a, f a = p
⊢ Nonempty { l // p ∈ l }
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ f x ≠ x

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ f x ≠ x
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ (some a, f) = (some a, f)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ∀ (a : ↑∅), False

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ∀ (a : ↑∅), False
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ (Finset.range (n + 1)).sum ?m.104 = ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))

pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ∀ x ∈ Finset.range (n + 1), (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = ?m.104 x

pp: n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ℕ → ℤ

Tactic:
]

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ∀ x ∈ Finset.range (n + 1),
    (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ ↑A = ↑A

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (-1) ^ x * ((↑n + 1) * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ((↑n + 1) * ↑((x + 1).ascFactorial (n - x)))

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ y, ∑ x, lineCount L (x, y).1 = ∑ x, ∑ y, pointCount P (x, y).2

Tactic:
]

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ y, ∑ x, lineCount L (x, y).1 = ∑ x, ∑ y, pointCount P (x, y).2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a⁻¹ •> (↑A <• a) = ↑A

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ a⁻¹ •> (↑A <• a) = ↑A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
inv_smul_A : ∀ {a : G}, a ∈ A → a⁻¹ •> ↑A = ↑H
⊢ A = A

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ a •> A ⊆ B * A ∧ b •> A ⊆ B * A

Tactic:
]

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ a •> A ⊆ B * A ∧ b •> A ⊆ B * A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
this : #(a •> A ∪ b •> A) ≤ #(B * A)
⊢ 2 * #A ≤ #(a •> A) + #(b •> A)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
this : #(a •> A ∪ b •> A) ≤ #(B * A)
⊢ 2 * #A ≤ #(a •> A) + #(b •> A)
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial) atTop (𝓝 (Real.exp (-1)))
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ i ∈ s, pointCount P i.2

pp: case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Tactic:
]

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ i ∈ s, pointCount P i.2

case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i ↦ (-1) ^ i / ↑i.factorial) (exp (-1))

Tactic:
]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ HasSum (fun i ↦ (-1) ^ i / ↑i.factorial) (exp (-1))
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 1)

Tactic:
]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 1)
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑((i + 1).ascFactorial (n - i)) / ↑n.factorial = s (n + 1)

Tactic:
]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑((i + 1).ascFactorial (n - i)) / ↑n.factorial = s (n + 1)
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial