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

Goal state before:
pp: a b : Finset (BinaryTree Unit)
x✝¹ x✝ : BinaryTree Unit × BinaryTree Unit
x₁ x₂ y₁ y₂ : BinaryTree Unit
h : (fun x ↦ node () x.1 x.2) (x₁, x₂) = (fun x ↦ node () x.1 x.2) (y₁, y₂)
⊢ (x₁, x₂) = (y₁, y₂)

Tactic:
simpa using

Goal state after:
a b : Finset (BinaryTree Unit)
x✝¹ x✝ : BinaryTree Unit × BinaryTree Unit
x₁ x₂ y₁ y₂ : BinaryTree Unit
h : (fun x ↦ node () x.1 x.2) (x₁, x₂) = (fun x ↦ node () x.1 x.2) (y₁, y₂)
⊢ x₁ = y₁ ∧ x₂ = y₂
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
⊢ ∀ (i : ℕ), count D (take i (↑p ++ ↑q)) ≤ count U (take i (↑p ++ ↑q))

Tactic:
simp only [take_append, count_append]
    exact fun _ ↦ add_le_add (p.count_D_le_count_U _) (q.count_D_le_count_U _)

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

Goal state before:
pp: case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
nonneg : ∀ (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 := nonneg } ≠ []
f : ¬s = U
⊢ False

Tactic:
simpa using

Goal state after:
case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
nonneg : ∀ (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 := nonneg } ≠ []
f : ¬s = U
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
rw [← mul_assoc, bell_mul_eq_lemma]

Goal state after:
case e_a.a.hx
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ≠ 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: 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:
refine subset_antisymm ?_ ?_
  · rw [subset_smul_finset_iff, ← op_inv]
    calc
      a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
      _ ⊆ A * (A⁻¹ * A) * A⁻¹ := by grw [smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        simp_rw [← coe_inj, coe_mul]
        rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
  · rw [subset_smul_finset_iff]
    calc
      a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * (A⁻¹ * A) <• a := smul_finset_subset_mul (by simpa)
      _ ⊆ A⁻¹ * ((A⁻¹ * A) * A) := by grw [op_smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
        simp_rw [← coe_inj, coe_mul]
        rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe]

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

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 •> (A⁻¹ * A) = (A⁻¹ * A) <• a
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
A Z : Finset G
hZA : ↑Z ⊆ ↑A
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
hHZA : (fun x ↦ ↑H <• x) '' ↑Z = (fun x ↦ ↑H <• x) '' ↑A
⊢ ↑H * ↑Z = ↑H * ↑A

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
A Z : Finset G
hZA : ↑Z ⊆ ↑A
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
hHZA : (fun x ↦ ↑H <• x) '' ↑Z = (fun x ↦ ↑H <• x) '' ↑A
⊢ ↑H * ↑Z = ↑H * ↑A
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
count_singleton'

Goal state after:
case inr
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ (count D (List.take (i - ([U] ++ ↑p).length) [D]) + if U = D then 1 else 0) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U [U]
Module: Mathlib.Combinatorics.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
h₁ z₁ h₂ z₂ : G
h : h₁ * z₁ = h₂ * z₂
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
hz₂ : z₂ ∈ Z
⊢ z₂ * z₁⁻¹ ∈ H

Tactic:
simpa using

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
h₁ z₁ h₂ z₂ : G
h : h₁ * z₁ = h₂ * z₂
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
hz₂ : z₂ ∈ Z
⊢ h₂⁻¹ * h₁ ∈ H
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
apply findIdx_lt_length_of_exists

Goal state after:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x ∈ range (↑p).length, decide (count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)) = true
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
apply Nat.div_eq_of_eq_mul_left

Goal state after:
case H1
m n : ℕ
hn : n ≠ 0
⊢ 0 < n ! ^ m * m !

case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
simpa using

Goal state after:
n : ℕ
p : (n + 1).Partition
⊢ n + 1 = ∑ a ∈ p.parts.toFinset, count a p.parts * a
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:
simpa using

Goal state after:
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
⊢ a + (p.parts.erase a).sum = n + 1
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:
simpa using

Goal state after:
n : ℕ
x : (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts }
⊢ ↑x.fst + 1 ∈ (↑x.snd).parts
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 : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) ↑p) = count D (List.take (j + 1) ↑p)) = false

Tactic:
simpa using

Goal state after:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ ¬count U (List.take (j + 1) ↑p) = count D (List.take (j + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
← Fintype.sum_sigma'

Goal state after:
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ x, n.choose ↑x.fst * ((↑x.snd).parts.erase (↑x.fst + 1)).bell =
    ∑ x, n.choose (↑x.snd - 1) * (x.fst.parts.erase ↑x.snd).bell
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: (↑p ++ [D]))) = count D (List.take (j + 1) (U :: (↑p ++ [D])))) = false

Tactic:
take_succ_cons,

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (U :: List.take j (↑p ++ [D])) = count D (U :: List.take j (↑p ++ [D]))) = false
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := ⋯
mud : IncidenceAlgebra 𝕜 αᵒᵈ := ⋯
this : mud * zeta 𝕜 * mu 𝕜 = mu 𝕜 * zeta 𝕜 * mu 𝕜
⊢ mud = mu 𝕜

Tactic:
simpa using

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := ⋯
mud : IncidenceAlgebra 𝕜 αᵒᵈ := ⋯
this : mud * zeta 𝕜 * mu 𝕜 = mu 𝕜 * zeta 𝕜 * mu 𝕜
⊢ mud = mu 𝕜
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ↑{ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } ≠ []

Tactic:
simpa using

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ¬↑p = []
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
hx : g x ≠ 0
⊢ x ∈ g.support

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
hx : g x ≠ 0
⊢ ¬g x = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

Tactic:
rw [← congrArg semilength (nest_insidePart_add_outsidePart h), semilength_add, semilength_nest,
    add_right_comm]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
h : g 0 ≠ 0
⊢ 0 ∈ g.support

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
h : g 0 ≠ 0
⊢ ¬g 0 = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ ∀ (a : ℕ), a ∈ g.support ↔ g a / a ≠ 0

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ ∀ (a : ℕ), ¬g a = 0 ↔ ¬a = 0 ∧ a ≤ g a
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
x : ℕ
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
          parts_pos := ⋯, parts_sum := ⋯ }.toFinsuppAntidiag
      x =
    g x

Tactic:
simpa using

Goal state after:
case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
x : ℕ
⊢ g x / x * x = g x
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
        parts_pos := ⋯, parts_sum := ⋯ }.toFinsuppAntidiag =
    g

Tactic:
ext x
    simpa [toFinsuppAntidiag] using Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x

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

Goal state before:
pp: case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ j ∈ range m, X ^ ((i + 1) * j) = 1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
sum_range_eq_add_Ico _ hm,

Goal state after:
case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ X ^ ((i + 1) * 0) + ∑ x ∈ Ico 1 m, X ^ ((i + 1) * x) =
    1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hb : b ∉ range (m - 1)
⊢ (if b + 1 < m then 1 else 0) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hb : b ∉ range (m - 1)
⊢ m ≤ b + 1
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)) = fun i ↦
    1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

pp: case e'_6
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (PowerSeries.mk fun n ↦ ↑(#(countRestricted n m))) = genFun fun i c ↦ if c < m then 1 else 0

Tactic:
· ext1 i
    rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range]
    congrm $(by simp) + ?_
    trans ∑ k ∈ range (m - 1), (if k + 1 < m then (1 : R) else 0) • X ^ ((i + 1) * (k + 1))
    · refine sum_congr rfl fun b hn ↦ ?_
      rw [add_comm 1 b]
      have : b + 1 < m := by grind
      simp [this]
    · exact (tsum_eq_sum (fun b hb ↦ smul_eq_zero_of_left (by simpa using hb) _)).symm

Goal state after:
case e'_6
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (PowerSeries.mk fun n ↦ ↑(#(countRestricted n m))) = genFun fun i c ↦ if c < m then 1 else 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case inl
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
⊢ Multipliable fun i ↦ ∑ j ∈ range 0, X ^ ((i + 1) * j)

Tactic:
simpa using

Goal state after:
case inl
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
⊢ Multipliable fun i ↦ 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ (1 - K) * ↑(#A) ≤ expansion K S A

Tactic:
one_sub_mul,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ ↑(#A) - K * ↑(#A) ≤ expansion K S A
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ Summable fun i ↦ x ^ (i + 1) * ∏ j < i, (1 - x ^ (j + 1))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ Summable fun i ↦ x ^ (i + 1) * ∏ x_1 ∈ Finset.range i, (1 - x ^ (x_1 + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ Multipliable fun x_1 ↦ 1 - x ^ (x_1 + 1)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ Multipliable fun x_1 ↦ 1 - x ^ (x_1 + 1)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: n m : ℕ
hm : 0 < m
⊢ #(restricted n fun x ↦ ¬m ∣ x) = #(countRestricted n m)

Tactic:
simpa using

Goal state after:
n m : ℕ
hm : 0 < m
⊢ #(restricted n fun x ↦ ¬m ∣ x) = #(countRestricted n m)
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
g : ℕ →₀ ℕ
hg : g ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d
hg' : g ∉ toFinsuppAntidiag '' ↑univ
⊢ g ∉ Set.range toFinsuppAntidiag

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
g : ℕ →₀ ℕ
hg : g ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d
hg' : g ∉ toFinsuppAntidiag '' ↑univ
⊢ ∀ (x : d.Partition), ¬x.toFinsuppAntidiag = g
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ (1 - K) * (↑t + 1) ≤ (1 - K) * ↑(#A)

Tactic:
by norm_cast; gcongr

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

Goal state before:
pp: case zero
n : ℕ
x✝ : n + 2 ≠ 0
hk : 0 ∈ Iic (n + 1)
⊢ Even (largeSchroder 0 * (n + 1 - 0).largeSchroder)

Tactic:
simpa using

Goal state after:
case zero
n : ℕ
x✝ : n + 2 ≠ 0
hk : 0 ∈ Iic (n + 1)
⊢ Even (n + 1).largeSchroder
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
k : ℕ
⊢ Multipliable fun n ↦ 1 - X ^ (n + k + 1)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
k : ℕ
⊢ Multipliable fun n ↦ 1 + -X ^ (n + k + 1)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
h : n ∉ Set.range pentagonal
⊢ ¬∃ k, pentagonal k = (Finsupp.single () n) ()

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
h : n ∉ Set.range pentagonal
⊢ ∀ (x : ℤ), ¬pentagonal x = n