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

Goal state before:
pp: case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h = U

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✝ } ≠ []
⊢ (↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head
      h =
    U

Tactic:
·

Goal state after:
case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h = U
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
(dichotomy _).resolve_right f

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.DyckWord

Goal state before:
pp: case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : { toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']

pp: case cons.nil
s : DyckStep
count_U_eq_count_D✝ : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']

pp: case cons.cons
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: head✝ :: tail✝)) ≤ count U (take i (s :: head✝ :: tail✝))
h :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ } ≠
    0
h' :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
⊢ take 1
      (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h']

Tactic:
·

Goal state after:
case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : { toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons.nil
s : DyckStep
count_U_eq_count_D✝ : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']

pp: case cons.cons
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: head✝ :: tail✝)) ≤ count U (take i (s :: head✝ :: tail✝))
h :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ } ≠
    0
h' :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
⊢ take 1
      (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h']

Tactic:
·

Goal state after:
case cons.nil
s : DyckStep
count_U_eq_count_D✝ : count U [s] = count D [s]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']
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.sum

Tactic:
·

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

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

Tactic:
·

Goal state after:
case cons.cons
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: head✝ :: tail✝)) ≤ count U (take i (s :: head✝ :: tail✝))
h :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ } ≠
    0
h' :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
⊢ take 1
      (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h']
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 !
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
⊢ ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A)

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 •> ↑H

pp: case refine_3
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 •> ↑H = ↑H <• 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
⊢ ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A)
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.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 ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !
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 •> ↑H

pp: case refine_3
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 •> ↑H = ↑H <• 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 •> ↑H
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_3
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 •> ↑H = ↑H <• a

Tactic:
·

Goal state after:
case refine_3
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 •> ↑H = ↑H <• a
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)! ≠ 0

Tactic:
·

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

Goal state before:
pp: case h
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ (m.toFinset.erase 0).erase a = ((a ::ₘ m).toFinset.erase 0).erase a

pp: case a
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
j : ℕ
hj : j ∈ ((a ::ₘ m).toFinset.erase 0).erase a
⊢ (count j m)! = (count j (a ::ₘ m))!

Tactic:
·

Goal state after:
case h
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ (m.toFinset.erase 0).erase a = ((a ::ₘ m).toFinset.erase 0).erase a
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case a
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
j : ℕ
hj : j ∈ ((a ::ₘ m).toFinset.erase 0).erase a
⊢ (count j m)! = (count j (a ::ₘ m))!

Tactic:
·

Goal state after:
case a
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
j : ℕ
hj : j ∈ ((a ::ₘ m).toFinset.erase 0).erase a
⊢ (count j m)! = (count j (a ::ₘ m))!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

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

Tactic:
·

Goal state after:
case inl
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i = 0
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U])
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
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 = ∏ j ∈ m.toFinset.erase 0, (count j m)!

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

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

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
⊢ (count a m)! * rest = ∏ j ∈ m.toFinset.erase 0, (count j m)!
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case inl
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 * ↑(#∅)
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑∅ * ↑∅⁻¹

pp: case inr
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
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

Tactic:
·

Goal state after:
case inl
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 * ↑(#∅)
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑∅ * ↑∅⁻¹
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons.cons
q : DyckWord
i : ℕ
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ :
  ∀ (i : ℕ), count D (List.take i (s :: head✝ :: tail✝)) ≤ count U (List.take i (s :: head✝ :: tail✝))
hn :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
l1 :
  List.take 1
      ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
          count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h]
⊢ (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).length -
      1 =
    (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
                count_D_le_count_U := count_D_le_count_U✝ }).length -
          1 -
        1 +
      1

Tactic:
·

Goal state after:
case cons.cons
q : DyckWord
i : ℕ
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ :
  ∀ (i : ℕ), count D (List.take i (s :: head✝ :: tail✝)) ≤ count U (List.take i (s :: head✝ :: tail✝))
hn :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
l1 :
  List.take 1
      ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
          count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h]
⊢ (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).length -
      1 =
    (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
                count_D_le_count_U := count_D_le_count_U✝ }).length -
          1 -
        1 +
      1
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 (List.take (min 1 j) ↑p) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take (min 1 j) ↑p) + count U (List.drop 1 (List.take j ↑p))
⊢ 1 ≤ j

Tactic:
by lia

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

Goal state before:
pp: case pos
𝕜 : 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
⊢ f a b = g a b

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
⊢ f a b = g a b

Tactic:
·

Goal state after:
case pos
𝕜 : 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
⊢ f a b = g a b
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m n : ℕ
hm : m = 0
⊢ (multinomial ∅ fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ ∅.erase 0, ∏ 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)

pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ 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 pos
m n : ℕ
hm : m = 0
⊢ (multinomial ∅ fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ ∅.erase 0, ∏ 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: 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
⊢ f a b = g a b

Tactic:
·

Goal state after:
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
⊢ f a b = g a b
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ 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
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ 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✝¹ : AddGroup 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (⇑f - ⇑g) a b = 0

Tactic:
by simp_rw [Pi.sub_apply, apply_eq_zero_of_not_le h, sub_zero]

Goal state after: