mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 1 = f

Tactic:
by

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

Goal state before:
pp: p : DyckWord
⊢ 2 * p.semilength = (↑p).length

Tactic:
by

Goal state after:
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:
by

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✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ f * g * h = f * (g * h)

Tactic:
by

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
⊢ ∑ x ∈ Icc a b, f a x • g x b = 0

Tactic:
by

Goal state after:
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
r_inv : ∀ (z : G), r z⁻¹ = r z
⊢ ↑(#(↑H).toFinset) = ↑(Fintype.card ↥H)

Tactic:
by

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✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
⊢ (f • g) • h = f • g • h

Tactic:
by

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
⊢ 1 • f = f

Tactic:
by

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
⊢ f • 0 = 0

Tactic:
by

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
⊢ f • (g + h) = f • g + f • h

Tactic:
by

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
⊢ (f + g) • h = f • h + g • h

Tactic:
by

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
⊢ 0 • f = 0

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ m.uniformBell n = ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
by

Goal state after:
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
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ↑(#A) * ↑(#A) = ↑(#A) * ↑(#A⁻¹)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ uniformBell 0 n = 1

Tactic:
by

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

Goal state before:
pp: m : ℕ
⊢ m.uniformBell 0 = 1

Tactic:
by

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 𝕜 𝕝
⊢ (algebraMap 𝕜 𝕝) 1 • 1 = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ uniformBell 1 n = 1

Tactic:
by

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

Goal state before:
pp: m : ℕ
⊢ m.uniformBell 1 = 1

Tactic:
by

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ 0 < p.firstReturn

Tactic:
by

Goal state after:
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
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ↑(#A) * ↑(#A⁻¹) = ↑(#(A ×ˢ A⁻¹))

Tactic:
by

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 * d) • 1 = (algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1

Tactic:
by

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 𝕜 𝕝
⊢ (algebraMap 𝕜 𝕝) 0 • 1 = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ↑(#(A ×ˢ A⁻¹)) = ∑ z ∈ S, ↑(r z)

Tactic:
by

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 + d) • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1

Tactic:
by

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)

Tactic:
by

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 : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ { toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c * f =
    f * { toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c

Tactic:
by

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

Goal state before:
pp: p : DyckWord
i : ℕ
hi : i < p.firstReturn
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Tactic:
by

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 : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ c • f = { toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c * f

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n * n ! ^ m * m ! = (m * n)!

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n = (m * n)! / (n ! ^ m * m !)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).bell = ∑ i ≤ n, n.choose i * (n - i).bell

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(#(Icc a b))

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).bell = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 * ij.2.bell

Tactic:
by

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

Goal state before:
pp: ⊢ Nat.bell 0 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ Nat.bell 1 = 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a ↑x

Tactic:
by

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

Goal state before:
pp: ⊢ Nat.bell 2 = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ n.succ * p.parts.bell = (∑ a ∈ p.parts.toFinset, count a p.parts * a) * p.parts.bell

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ (∑ a ∈ p.parts.toFinset, count a p.parts * a) * p.parts.bell =
    ∑ a ∈ p.parts.toFinset, a * (count a p.parts * p.parts.bell)

Tactic:
by

Goal state after:
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
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ∑ z ∈ S, ↑(r z) = ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(r z) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), ↑(r z)

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
⊢ a ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
⊢ (p.parts.erase a).sum + a = n + 1

Tactic:
by

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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : ¬muFun 𝕜 a b = 0
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ ∑ a ∈ p.parts.toFinset, a * (count a p.parts * p.parts.bell) =
    ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (mu 𝕜) a b = if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜) a x

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) =
    n.succ * ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ p.parts.bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a : α
⊢ (mu 𝕜) a a = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts }
⊢ ↑x.fst + 1 ∈ (↑x.snd).parts.toFinset

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : (p : (n + 1).Partition) × ↥p.parts.toFinset
⊢ ↑x.snd - 1 < n.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : (p : (n + 1).Partition) × ↥p.parts.toFinset
⊢ ↑⟨↑x.snd - 1, ⋯⟩ + 1 ∈ x.fst.parts

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts }
⊢ (fun x ↦ ⟨⟨↑x.snd - 1, ⋯⟩, ⟨x.fst, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⟨↑x.fst + 1, ⋯⟩⟩) x) = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : (p : (n + 1).Partition) × ↥p.parts.toFinset
⊢ (fun x ↦ ⟨↑x.snd, ⟨↑x.fst + 1, ⋯⟩⟩) ((fun x ↦ ⟨⟨↑x.snd - 1, ⋯⟩, ⟨x.fst, ⋯⟩⟩) x) = x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = if a = b then 1 else 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b ↑x

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ i ≤ n, n.choose i * (n - i).bell = ∑ i ≤ n, ∑ q, n.choose i * q.parts.bell

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
i : ℕ
hi : i ∈ Finset.Iic n
this : i ≤ n
⊢ 1 ≤ i + 1

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
i : ℕ
hi : i ∈ Finset.Iic n
this : i ≤ n
h1 : 1 ≤ i + 1
⊢ i + 1 ≤ n + 1

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
i : ℕ
hi : i ∈ Finset.Iic n
this : i ≤ n
h1 : 1 ≤ i + 1
h2 : i + 1 ≤ n + 1
⊢ n + 1 - (i + 1) = n - i

Tactic:
by

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

Goal state before:
pp: p q : DyckWord
⊢ (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ i ≤ n, ∑ q, n.choose i * q.parts.bell = ∑ i ≤ n, ∑ p, n.choose i * ((↑p).parts.erase (i + 1)).bell

Tactic:
by

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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : ¬muFun' 𝕜 b a = 0
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (mu' 𝕜) a b = if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜) x b

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a : α
⊢ (mu' 𝕜) a a = 1

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ i ≤ n, ∑ p, n.choose i * ((↑p).parts.erase (i + 1)).bell =
    ∑ x, n.choose (↑x.snd - 1) * (x.fst.parts.erase ↑x.snd).bell

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (mu' 𝕜) a b = -∑ x ∈ Ioc a b, (mu' 𝕜) x b

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ p, ∑ a, n.choose (↑a - 1) * (p.parts.erase ↑a).bell = ∑ p, p.parts.bell

Tactic:
by

Goal state after:
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
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(r z) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), ↑(r z) ≤
    ∑ z ∈ S with (K - 1) * ↑(#A) < ↑(r z), ↑(#A) + ∑ z ∈ S with ↑(r z) ≤ (K - 1) * ↑(#A), (K - 1) * ↑(#A)

Tactic:
by

Goal state after: