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

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (U :: ↑p ++ [D]).length ≤ (↑p).length + 1 + 1

Tactic:
simp

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

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ ∀ 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:
intro j

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
⊢ j < (↑p).length + 1 →
    decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ 0 = 0 + ∑' (i : ℕ), 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y z : α
hz : z ∈ Ici y
⊢ f z = (zeta 𝕜) y z * f z

Tactic:
zeta_apply,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y z : α
hz : z ∈ Ici y
⊢ f z = (if y ≤ z then 1 else 0) * f z
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ (mu 𝕜 * zeta 𝕜).prod (mu 𝕜 * zeta 𝕜) = 1

pp: case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)

Tactic:
mu_mul_zeta,

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ IncidenceAlgebra.prod 1 (mu 𝕜 * zeta 𝕜) = 1

case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ IncidenceAlgebra.prod 1 (mu 𝕜 * zeta 𝕜) = 1

pp: case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)

Tactic:
mu_mul_zeta,

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ IncidenceAlgebra.prod 1 1 = 1

case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
x✝⁵ x✝⁴ x✝³ : α
x✝² x✝¹ x✝ : β
⊢ (mu 𝕜) x✝² x✝¹ * (zeta 𝕜) x✝⁴ x✝³ = (zeta 𝕜) x✝⁴ x✝³ * (mu 𝕜) x✝² x✝¹

Tactic:
simp

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

Goal state before:
pp: case refine_3
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
h1 : s.sum ⇑g = d
h2 : g.support ⊆ s
⊢ (Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ }).sum = s.sum ⇑g

Tactic:
suffices ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x by simpa [Finsupp.sum]

Goal state after:
case refine_3
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
h1 : s.sum ⇑g = d
h2 : g.support ⊆ s
⊢ ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x
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
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
h1 : s.sum ⇑g = d
h2 : g.support ⊆ s
⊢ ∀ x ∈ s \ g.support, g x = 0

Tactic:
simp

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
n : ℕ
⊢ ∀ (a : DyckWord), a.semilength = n ↔ equivTree a ∈ treesOfNumNodesEq n

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ X ^ ((i + 1) * 0) + ∑' (b : ℕ), X ^ ((i + 1) * (b + 1)) = 1 + ∑' (j : ℕ), 1 • X ^ ((i + 1) * (j + 1))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ constantCoeff (X ^ i * X ^ 1) = 0

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : ¬p (i + 1)
⊢ 1 = 1 + ∑' (j : ℕ), 0 • X ^ ((i + 1) * (j + 1))

Tactic:
simp

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

Goal state before:
pp: case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, p i_1 then 1 else 0)) =
    PowerSeries.mk fun n ↦ ∑ x, if ∀ i ∈ (Multiset.toFinsupp x.parts).support, p i then 1 else 0

Tactic:
simp

Goal state after:
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 : ℕ
⊢ X ^ ((i + 1) * 0) = 1

Tactic:
simp

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

Goal state before:
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 ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, Multiset.count i_1 i.parts < m then 1 else 0)) =
    PowerSeries.mk fun n ↦
      ∑ x, if ∀ i ∈ (Multiset.toFinsupp x.parts).support, (Multiset.toFinsupp x.parts) i < m then 1 else 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
| fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), (X ^ (b + 1)) ^ j) * (1 - X ^ (b + 1))

Tactic:
ext b

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
b : ℕ
| if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), (X ^ (b + 1)) ^ j) * (1 - X ^ (b + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
b : ℕ
⊢ constantCoeff (X ^ (b + 1)) = 0

Tactic:
simp

Goal state after:
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
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ 𝓝 0 = 𝓝 (0 * (0 - 1) * ∏' (i : ℕ), (1 - x ^ (k + i + 2)))

Tactic:
simp

Goal state after:
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
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ 0 < k + 1

Tactic:
simp

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 ℕ
hs : s ⊇ range d
⊢ ∏ 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)))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) * ∏' (i : ℕ), (1 - X ^ (i + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))

Tactic:
by
  nontriviality R
  rw [← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
    (multipliable_one_sub_X_pow _)]
  simp_rw [ite_not, ite_mul, pow_mul]
  conv in fun b ↦ _ =>
    ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]
  refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 1) ?_ ?_ ?_
  · intro a b h
    rw [tsub_left_inj (by nlinarith) (by nlinarith), mul_left_inj' (hm.ne.symm), add_left_inj] at h
    exact SetCoe.ext h
  · suffices ∀ (i : ℕ), m ∣ i + 1 → ∃ j ≠ 0, j * m - 1 = i by simpa
    intro i hi
    obtain ⟨j, hj⟩ := dvd_def.mp hi
    refine ⟨j, by grind, Nat.sub_eq_of_eq_add ?_⟩
    rw [hj, mul_comm m j]
  · intro i
    have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind
    simp [this, pow_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) =
    PowerSeries.mk fun n ↦ ↑(#(countRestricted n m))

Tactic:
rw [powerSeriesMk_card_countRestricted_eq_tprod R hm]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) = ∏' (i : ℕ), ∑ j ∈ range m, X ^ ((i + 1) * j)
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
r : ℝ
⊢ {1}.Nonempty

Tactic:
simp

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 ℕ
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
⊢ 0 ∉ Finset.map (addRightEmbedding 1) s

Tactic:
simp

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 ℕ
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
p : d.Partition
x✝ : p ∈ univ
⊢ 0 ∉ Finset.map (addRightEmbedding 1) s

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 : ℝ
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)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ #(A * S) ≤ t * #S

Tactic:
grw [card_mul_le, hAt]

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

Goal state before:
pp: x✝ : 1 ≠ 0
⊢ Even (largeSchroder 1)

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 : ℝ
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)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G}, A.Nonempty → #A ≤ t → ex A ∈ M
⊢ (M ∪ {κ + 1}).Nonempty

Tactic:
simp

Goal state after:
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
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n✝ : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n✝ + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n✝ + 1) * x ^ ((n✝ + 1) * (3 * n✝ + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow n✝ n x
n : ℕ
⊢ 0 < 2

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 : ℝ
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)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G}, A.Nonempty → #A ≤ t → ex A ∈ M
this✝ : (M ∪ {κ + 1}).Nonempty
k : ℝ := (M ∪ {κ + 1}).min' this✝
this : κ < k
A : Finset G
hA : A.Nonempty
hAk : expansion K S A < k
⊢ κ + 1 ∈ M ∪ {κ + 1}

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        ⊥.largeSchroder * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

Tactic:
simp

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo 0 (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder + (n + 1).largeSchroder +
        (n + 1).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ x ∈ Ioo 0 (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0

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 S : Finset G
hK : K < 1
hS : S.Nonempty
hA : IsFragment K S A
⊢ A.Nonempty

Tactic:
by
  by_contra! rfl
  simp [*, not_isFragment_empty hK hS] at hA

Goal state after:
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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
⊢ ∃ H x, IsAtom K S (↑H).toFinset

Tactic:
have self_mem_smul_carrier (x : G) : x ∈ x • n⁻¹ • N := by
    apply smul_mem_smul_finset (a := x) at one_mem_carrier
    simpa only [smul_eq_mul, mul_one] using! one_mem_carrier

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
⊢ ∃ H x, IsAtom K S (↑H).toFinset
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
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h✝ : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n✝ : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n✝ + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n✝ + 1) * x ^ ((n✝ + 1) * (3 * n✝ + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow n✝ n x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
n : ℕ
⊢ 0 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ 0 ≤ (∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (n + 1).smallSchroder = 3 * n.smallSchroder + 2 * ∑ i ∈ Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder

Tactic:
obtain _ | _ | n := n
  · simp at hn
  · simp at hn
  refine Nat.mul_left_cancel zero_lt_two ?_
  calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;>
      · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
        we need to re-enable model-based theory combination in `lia` for this to go through. -/
        lia +mbtc
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
this : HasSum ((fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) ∘ pentagonal) (pentagonalSeries R)
x✝ : ℤ
⊢ ↑↑x✝.negOnePow * X ^ pentagonal x✝ = ((fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) ∘ pentagonal) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)
x : ℤ
hx : x ∉ Set.range Neg.neg
⊢ - -x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ #(⊥.cliqueFinset 3) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) (pentagonalSeries R)
k : ℕ
⊢ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1)) =
    ↑↑(-↑k).negOnePow * X ^ pentagonal (-↑k) + ↑↑((↑k).negOnePow * Int.negOnePow 1) * X ^ pentagonal (↑k + 1)

Tactic:
simp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
h : HasSum ((fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) ∘ Neg.neg) (pentagonalSeries R)
k : ℕ
⊢ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1)) =
    (-1) ^ k * X ^ pentagonal (-↑k) + -((-1) ^ k * X ^ pentagonal (↑k + 1))