mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ s = U

Tactic:
]

Goal state after:
case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ s = U
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A * (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False

Tactic:
]

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ ∏ x ∈ m.toFinset.erase 0,
      x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!

Tactic:
]

Goal state after:
case e_a
m : Multiset ℕ
⊢ ∏ x ∈ m.toFinset.erase 0,
      x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * ↑A = ↑A⁻¹ * ↑A

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a.a
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ (x * count x m)! = (x * count x m)!

pp: case e_a.a.hx
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
case e_a.a.hx
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ≠ 0
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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a⁻¹ •> ((A⁻¹ * 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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = ∑ m_1 ∈ m.toFinset, count m_1 m • m_1

Tactic:
]

Goal state after:
case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = ∑ m_1 ∈ m.toFinset, count m_1 m • m_1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = take 1 (↑p).dropLast ++ drop 1 (↑p).dropLast ++ [(↑p).getLast h']

Tactic:
]

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = take 1 (↑p).dropLast ++ drop 1 (↑p).dropLast ++ [(↑p).getLast h']
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A * A) ⊆ A⁻¹ * (A⁻¹ * A * A)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = [U] ++ (↑p).dropLast.tail ++ [D]

Tactic:
]

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = [U] ++ (↑p).dropLast.tail ++ [D]
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
k : ℕ
⊢ count D (List.take (min k i) ↑p) ≤ count U (List.take (min k i) ↑p)

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
k : ℕ
⊢ count D (List.take (min k i) ↑p) ≤ count U (List.take (min k i) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

pp: m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !

pp: m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0

Tactic:
]

Goal state after:
m : Multiset ℕ
⊢ m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !

m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑(A.invMulSubgroup h) = ↑(A.invMulSubgroup h)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ m.bell * (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !

Tactic:
]

Goal state after:
m : Multiset ℕ
⊢ m.bell * (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U (List.take i ↑p) + count U (List.drop i ↑p) = count D (List.take i ↑p) + count D (List.drop i ↑p)
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
this : count U (List.take i ↑p) + count U (List.drop i ↑p) = count D (List.take i ↑p) + count D (List.drop i ↑p)
⊢ count U (List.drop i ↑p) = count D (List.drop i ↑p)
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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(#(A * A)) < 3 / 2 * ↑(#A)

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(#(A * A)) < 3 / 2 * ↑(#A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take k (List.drop i ↑p)) ≤ count U (List.take k (List.drop i ↑p))

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take k (List.drop i ↑p)) ≤ count U (List.take k (List.drop i ↑p))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣
    m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
]

Goal state after:
m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣
    m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)
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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> (↑A⁻¹ * ↑A)

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> (↑A⁻¹ * ↑A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take (i + k) ↑p) ≤ count U (List.take (i + k) ↑p)

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take i (List.take (i + k) ↑p)) = count D (List.take i (List.take (i + k) ↑p))
⊢ count D (List.take (i + k) ↑p) ≤ count U (List.take (i + k) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ 0 < (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
]

Goal state after:
m : Multiset ℕ
⊢ 0 < (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ ↑H = ↑H

pp: case ha
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ x * a⁻¹ ∈ H

Tactic:
]

Goal state after:
case ha
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ x * a⁻¹ ∈ H
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case ha
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ x ∈ ↑H <• a

Tactic:
]

Goal state after:
case ha
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ x ∈ ↑H <• a
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) +
      count D (List.take (i - [U].length) ↑p) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U]) +
      count U (List.take (i - [U].length) ↑p)

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) +
      count D (List.take (i - [U].length) ↑p) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U]) +
      count U (List.take (i - [U].length) ↑p)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
⊢ Fintype.card ↥H * #Z = #(↑H).toFinset * #Z

pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
⊢ Set.InjOn (fun p ↦ p.1 * p.2) (↑(↑H).toFinset ×ˢ ↑Z)

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
⊢ Fintype.card ↥H * #Z = #(↑H).toFinset * #Z

G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
⊢ Set.InjOn (fun p ↦ p.1 * p.2) (↑(↑H).toFinset ×ˢ ↑Z)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ 1 ≤ i

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ 1 ≤ i
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ (count D (List.take (i - ([U] ++ ↑p).length) [D]) + if U = D then 1 else 0) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U [U]

Tactic:
]

Goal state after:
case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ (count D (List.take (i - ([U] ++ ↑p).length) [D]) + if U = D then 1 else 0) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U [U]
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ 0 + count D (List.take (i - ([U] ++ ↑p).length) [D]) ≤ count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U [U]

Tactic:
]

Goal state after:
case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ 0 + count D (List.take (i - ([U] ++ ↑p).length) [D]) ≤ count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U [U]
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hmem : a ∈ m.toFinset.erase 0
⊢ (count a m)! * rest = (count a m)! * ∏ x ∈ (m.toFinset.erase 0).erase a, (count x m)!

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ (↑p).length + 1

Tactic:
]

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ i ≤ (↑p).length + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ 1 ≤ i

Tactic:
]

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ 1 ≤ i
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) ≤ count U (List.take (i - 1) ↑p)

Tactic:
]

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) ≤ count U (List.take (i - 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
hn : p.IsNested
this :
  (count U (↑p).dropLast.tail + if (U == U) = true then 1 else 0) + count U [D] =
    count D (U :: (↑p).dropLast.tail ++ [D])
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail

Tactic:
]

Goal state after:
p q : DyckWord
h : p ≠ 0
hn : p.IsNested
this :
  (count U (↑p).dropLast.tail + if (U == U) = true then 1 else 0) + count U [D] =
    count D (U :: (↑p).dropLast.tail ++ [D])
⊢ count U (↑p).dropLast.tail = count D (↑p).dropLast.tail
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))

Tactic:
]

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
hc : 0 < a ! * c
hq : (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ((count a (a ::ₘ m))! * rest) = (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!

Tactic:
]

Goal state after:
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
hc : 0 < a ! * c
hq : (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ((count a (a ::ₘ m))! * rest) = (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq : count D [U] + count D (List.drop 1 (List.take j ↑p)) < count U [U] + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
]

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq : count D [U] + count D (List.drop 1 (List.take j ↑p)) < count U [U] + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m n : ℕ
⊢ (multinomial (if m = 0 then ∅ else {n}) fun k ↦ k * count k (replicate m n)) *
      ∏ k ∈ (if m = 0 then ∅ else {n}).erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
]

Goal state after:
m n : ℕ
⊢ (multinomial (if m = 0 then ∅ else {n}) fun k ↦ k * count k (replicate m n)) *
      ∏ k ∈ (if m = 0 then ∅ else {n}).erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.semilength = count U ↑p

Tactic:
]

Goal state after:
p : DyckWord
⊢ p.semilength = count U ↑p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ count D ↑p + count U ↑p = (↑p).length

Tactic:
]

Goal state after:
p : DyckWord
⊢ count D ↑p + count U ↑p = (↑p).length
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : AddCommMonoid 𝕜
inst✝ : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case e'_6
p : DyckWord
⊢ (countP fun x ↦ x == U) = countP fun a ↦ decide ¬(a == D) = true

Tactic:
]

Goal state after:
case e'_6
p : DyckWord
⊢ (countP fun x ↦ x == U) = countP fun a ↦ decide ¬(a == D) = true
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
z : G
⊢ r z⁻¹ = r z

Tactic:
simp [r, inv_inv]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddCommMonoid 𝕜
inst✝¹ : AddCommMonoid 𝕝
inst✝ : SMul 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
a b : α
h : ¬a ≤ b
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

pp: p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length

Tactic:
]

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
]

Goal state after:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (f • 0) a✝¹ b✝ = 0 a✝¹ b✝

Tactic:
exact sum_eq_zero fun x _ ↦ smul_zero _

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ↑p ≠ []

Tactic:
]

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ↑p ≠ []
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ p.firstReturn < (range (↑p).length).length

Tactic:
]

Goal state after:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ p.firstReturn < (range (↑p).length).length
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ m ! = ∏ x ∈ ∅.erase 0, (count x (replicate m n))!

Tactic:
hm,

Goal state after:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0! = ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))!