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

Goal state before:
pp: n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
l₂ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)
h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom
h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom
⊢ 2 * (2 * ↑i + 1) * ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑i.centralBinom * (2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)) * (2 * ↑i - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)

Tactic:
]

Goal state after:
n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
l₂ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)
h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom
h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom
⊢ 2 * (2 * ↑i + 1) * ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑i.centralBinom * (2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)) * (2 * ↑i - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
]

Goal state after:
case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0
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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) <
    ∑ x ∈ A⁻¹ * A,
      ↑(#({a ∈ A ×ˢ A |
            (match a with
              | (x, y) => x * y⁻¹) =
              x}))

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) <
    ∑ x ∈ A⁻¹ * A,
      ↑(#({a ∈ A ×ˢ A |
            (match a with
              | (x, y) => x * y⁻¹) =
              x}))
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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ ↑(#(A⁻¹ * A)) < 2 * ↑(#A)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ ↑(#(A⁻¹ * A)) < 2 * ↑(#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 ⊆ a •> A⁻¹ * A

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A
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
⊢ ↑(A.invMulSubgroup h) = ↑(A.invMulSubgroup h)

Tactic:
]

Goal state after:
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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> (A⁻¹ * A) <• a = a •> (A⁻¹ * A) <• a

Tactic:
]

Goal state after:
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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a

Tactic:
rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]

Goal state after:
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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ 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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * 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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A ⊆ A * A⁻¹ <• a
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: ⊢ {nil} = {nil}

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh ↦ pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
]

Goal state after:
n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh ↦ pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
]

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑(d - ↑x) + 1)) =
    ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Tactic:
]

Goal state after:
case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑(d - ↑x) + 1)) =
    ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 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⁻¹
⊢ ↑(A.invMulSubgroup h) = ↑(A.invMulSubgroup h)

Tactic:
]

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

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
i : Fin d.succ
x✝ : i ∈ univ
⊢ ↑(↑i).centralBinom / (↑↑i + 1) * ↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1) =
    ↑(↑i).centralBinom / (↑↑i + 1) * ↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)

Tactic:
]

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

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Tactic:
]

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(d + 1).centralBinom / (↑(d + 1) + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(d + 1).centralBinom / (↑d + 2) = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Tactic:
]

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(d + 1).centralBinom / (↑d + 2) = ↑(d + 1).centralBinom / (↑(d + 1) + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ antidiagonal n
⊢ catalan (i, j).1 * catalan (i, j).2 = catalan (i, j).1 * catalan (i, j).2

Tactic:
]

Goal state after:
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
⊢ (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)

Tactic:
]

Goal state after:
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
⊢ (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
]

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 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
⊢ a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))

Tactic:
]

Goal state after:
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
⊢ a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: 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)

Tactic:
]

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.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
]

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !
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⁻¹
⊢ A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)

Tactic:
]

Goal state after:
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⁻¹
⊢ A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c + x)! = (x * (c + 1))!

Tactic:
]

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c + x)! = (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)
⊢ #A = #A

Tactic:
]

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

Goal state before:
pp: m : Multiset ℕ
⊢ (∏ i ∈ m.toFinset, (i * count i m)!) *
      (((Nat.multinomial m.toFinset fun k ↦ k * count k m) *
            ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
          (map (fun j ↦ j !) m).prod *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
]

Goal state after:
m : Multiset ℕ
⊢ (∏ i ∈ m.toFinset, (i * count i m)!) *
      (((Nat.multinomial m.toFinset fun k ↦ k * count k m) *
            ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
          (map (fun j ↦ j !) m).prod *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
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
⊢ #A = #A

Tactic:
]

Goal state after:
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
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
]

Goal state after:
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
⊢ #(A⁻¹ * A) < 2 * #A
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
⊢ 0 < #(l ∩ r)

Tactic:
]

Goal state after:
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
⊢ 0 < #(l ∩ r)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) *
      (∑ k ∈ m.toFinset, k * count k m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
]

Goal state after:
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) *
      (∑ k ∈ m.toFinset, k * count k m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (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)!) * (0 * count 0 m)!

Tactic:
]

Goal state after:
case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (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)!) * (0 * count 0 m)!
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
⊢ ∃ y ∈ A, ∃ z_1 ∈ A, y * z_1 = z

Tactic:
]

Goal state after:
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
⊢ ∃ y ∈ A, ∃ z_1 ∈ A, y * z_1 = z
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
h : ↑((fun x ↦ p + x) q) = ↑((fun x ↦ p + x) r)
⊢ ↑q = ↑r

Tactic:
]

Goal state after:
p q r : DyckWord
h : ↑((fun x ↦ p + x) q) = ↑((fun x ↦ p + x) r)
⊢ ↑q = ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
h : ↑((fun x ↦ x + p) q) = ↑((fun x ↦ x + p) r)
⊢ ↑q = ↑r

Tactic:
]

Goal state after:
p q r : DyckWord
h : ↑((fun x ↦ x + p) q) = ↑((fun x ↦ x + p) r)
⊢ ↑q = ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0

Tactic:
]

Goal state after:
p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0
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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) <• a⁻¹ ⊆ A⁻¹ * A

Tactic:
]

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