mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) / ↑((4 * 4) ^ #P.parts)) ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ ∀ {a b : ℕ}, a < b → a < b

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * 0 - 1 ≤ #s
⊢ ∅ ⊆ s ∧ #∅ = 0 ∧ ↑0 ∣ ∑ i ∈ ∅, a i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
n : ℕ
⊢ (2 ^ 0 * n).bitIndices = map (fun x ↦ x + 0) n.bitIndices

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: k : ℕ
⊢ map (fun x ↦ x + k) (bitIndices 1) = [k]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
⊢ (map (fun i ↦ 2 ^ i) (bitIndices 0)).sum = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case zero
i : ℕ
⊢ i ∈ bitIndices 0 ↔ testBit 0 i = true

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case nil
hL : [].SortedLT
⊢ (map (fun i ↦ 2 ^ i) []).sum.bitIndices = []

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
i : Finset α
hi : i ∈ B
⊢ ∀ x ∈ i, g (B.biUnion id) x = g (B.biUnion id) x

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Finset α) → (a : ↥s) → β ↑a
a : α
⊢ a ∈ {a}

Tactic:
simp

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

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
hk : 0 ≤ 2 * m - 1
⊢ #∅ = 0 ∧ (↑∅).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ ∅ → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ v ⬝ᵥ (crossProduct v) w = 0

Tactic:
rw [cross_apply, vec3_dotProduct]
  dsimp only [Matrix.cons_val]
  ring

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
ha hb : a ∉ s
⊢ toColex (cons a s ha) ≤ toColex (cons a s hb) ↔ a ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a : α
inst✝ : DecidableEq α
ha hb : a ∈ s
⊢ toColex (s.erase a) ≤ toColex (s.erase a) ↔ a ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ u : Finset α
a b : α
r : ℕ
t : Colex (Finset α)
⊢ t ≤ t ∨ t ≤ t

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
rw [← not_le, toColex_le_toColex, not_forall]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ x, ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
rw [← not_le, toColex_le_toColex, not_forall]
  simp only [not_forall, not_exists, not_and, not_le, exists_prop]

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

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ (Multiset.map Prod.fst t.val).card = n ∧ ↑n ∣ (Multiset.map Prod.fst t.val).sum

Tactic:
simpa using ht

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

Goal state before:
pp: n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ (Multiset.map Prod.fst t.val).card = n ∧ (Multiset.map Prod.fst t.val).sum = 0

Tactic:
simpa using ht

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
⊢ s ∈ initSeg s

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: s : Finset ℕ
n a : ℕ
hn : 2 ≤ n
hi : a ∈ s
⊢ ∀ i ∈ s, 0 ≤ n ^ i

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: s : Finset ℕ
⊢ (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s

Tactic:
by
  simp [← (geomSum_injective rfl.le).eq_iff, List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one,
      cons_val_zero, Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one,
      cons_val_zero, Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun i ↦ i) ⟨2, ⋯⟩) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one,
      cons_val_zero, Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

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

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

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ (Equiv.swap none (some a)) ((⇑(Equiv.swap none (some a)) ∘ ⇑(optionCongr f)) none) ≠ (Equiv.swap none (some a)) none

Tactic:
simp

Goal state after:
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 x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
x_vs_a,

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) ≠ (Equiv.swap none (some a)) (some a)
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
⊢ ∀ (i : L), i ∈ univ ↔ f i ∈ univ

Tactic:
simp

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

Goal state before:
pp: case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
G : Digraph V
v w : V
⊢ (Digraph.mk' fun v w ↦ decide (G.Adj v w)).Adj v w ↔ G.Adj v w

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst✝ : Nonempty V
v : V
⊢ ⊥.Adj v v ≠ ⊤.Adj v v

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ b⁻¹ * a⁻¹ = (a * b)⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: case zero
⊢ ↑(catalan 0) = ↑(Nat.centralBinom 0) / (↑0 + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
a✝ : BinaryTree Unit
⊢ (a✝ ∈
      (antidiagonal n).attach.biUnion fun ijh ↦
        pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) ↔
    a✝ ∈ (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
⊢ ∀ (x : BinaryTree Unit), x ∈ ↑(treesOfNumNodesEq n) ↔ x ∈ {x | x.numNodes = n}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hz
⊢ #(treesOfNumNodesEq 0) = catalan 0

Tactic:
simp

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
⊢ x ! ^ 0 * 0! * ∏ j ∈ Finset.range 0, (j * x + x - 1).choose (x - 1) = (x * 0)!

Tactic:
simp

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)

Tactic:
rw [Finset.prod_range_succ]

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! * (c + 1) * x ! ^ c * c ! *
      ((∏ x_1 ∈ Finset.range c, (x_1 * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1)) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝² : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝¹ : #l = #A
this✝ : #r = #A
this : #(l ∪ r) < 2 * #A
t : G
ht : t ∈ A ∧ t⁻¹ * z ∈ A
⊢ t * (t⁻¹ * z) = z

Tactic:
simp

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

Goal state before:
pp: ⊢ count U [] = count D []

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])

Tactic:
simp

Goal state after:
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:
exact p.count_D_le_count_U _

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case neg
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 = ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
have hcount : m.count a = 0 := by grind [Multiset.count_eq_zero_of_notMem]

Goal state after:
case neg
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
hcount : count a m = 0
⊢ (count a m)! * rest = ∏ j ∈ m.toFinset.erase 0, (count j m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : ↑(#(∅⁻¹ * ∅)) ≤ K * ↑(#∅)
hA₂ : ↑(#(∅ * ∅⁻¹)) ≤ K * ↑(#∅)
⊢ ↑(#∅) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑⊥ * ↑∅ = ↑∅ * ↑∅⁻¹

Tactic:
simp

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : ↑(#(∅⁻¹ * ∅)) ≤ K * ↑(#∅)
hA₂ : ↑(#(∅ * ∅⁻¹)) ≤ K * ↑(#∅)
⊢ 0 ≤ (2 - K) * K / ((φ - K) * (K - ψ))
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:
exact p.count_D_le_count_U _

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

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

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

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

Tactic:
simp

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

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

Goal state before:
pp: case inl
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 : 𝕜
a : α
a✝ : a ≤ a
⊢ ((algebraMap 𝕜 𝕝) (c * d) • 1) a a = ((algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1) a a

Tactic:
simp only [one_apply, smul_eq_mul, mul_apply, constSMul_apply, map_mul,
            eq_comm, Icc_self]

Goal state after:
case inl
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 : 𝕜
a : α
a✝ : a ≤ a
⊢ ((algebraMap 𝕜 𝕝) c * (algebraMap 𝕜 𝕝) d * if True then 1 else 0) =
    ∑ x ∈ {a}, ((algebraMap 𝕜 𝕝) c * if a = x then 1 else 0) * ((algebraMap 𝕜 𝕝) d * if a = x then 1 else 0)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case inl
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 : 𝕜
a : α
a✝ : a ≤ a
⊢ ((algebraMap 𝕜 𝕝) c * (algebraMap 𝕜 𝕝) d * if True then 1 else 0) =
    ∑ x ∈ {a}, ((algebraMap 𝕜 𝕝) c * if a = x then 1 else 0) * ((algebraMap 𝕜 𝕝) d * if a = x then 1 else 0)

Tactic:
simp

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:
convert! bell_mul_eq (replicate m n)

Goal state after:
case e'_2.e'_5.e'_6
m n : ℕ
hn : n ≠ 0
⊢ n ! ^ m = (map (fun j ↦ j !) (replicate m n)).prod

case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

case e'_3
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e'_3
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum

Tactic:
simp

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 x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Tactic:
mem_Icc

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ ∀ j < p.firstReturn, decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
intro j

Goal state after:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
⊢ j < p.firstReturn → decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false
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:
simp

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

Goal state before:
pp: case zero
n : ℕ
ih : ∀ m < 0, m.bell = ∑ p, p.parts.bell
⊢ Nat.bell 0 = ∑ p, p.parts.bell

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ 0 ≤ (C (f (i + 1) (m + 1))).order

Tactic:
simp

Goal state after: