mathlib-initiative/mathlib-tactics huggingface dataset:
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))

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)
⊢ Summable fun n ↦ X ^ ((i + 1) * (n + 1))

Tactic:
·

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

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
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
        parts_pos := ⋯, parts_sum := ⋯ }.toFinsuppAntidiag =
    g
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:
·

Goal state after:
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))
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 ↦ ↑(#(restricted n p))) = genFun fun i c ↦ if p i then 1 else 0

Tactic:
·

Goal state after:
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 ↦ ↑(#(restricted n p))) = genFun fun i c ↦ if p i then 1 else 0
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:
·

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
⊢ (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))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ p.parts.toFinset ⊆ s

pp: case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ s \ p.parts.toFinset, (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ p.parts.toFinset,
    f x (Multiset.count x p.parts) = (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1)))

Tactic:
·

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ p.parts.toFinset ⊆ s
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 : ℕ
⊢ ∑ k ∈ range (m - 1), X ^ ((i + 1) * (1 + k)) =
    ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1))

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

Tactic:
·

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ k ∈ range (m - 1), X ^ ((i + 1) * (1 + k)) =
    ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ s \ p.parts.toFinset, (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ p.parts.toFinset,
    f x (Multiset.count x p.parts) = (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1)))

Tactic:
·

Goal state after:
case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ s \ p.parts.toFinset, (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 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 : ℕ
⊢ ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1)) =
    ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
·

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 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: 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:
·

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

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ p.parts.toFinset,
    f x (Multiset.count x p.parts) = (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1)))

Tactic:
·

Goal state after:
case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ p.parts.toFinset,
    f x (Multiset.count x p.parts) = (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1)))
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)

pp: case inr
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)

Tactic:
·

Goal state after:
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)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

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

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    if Multiset.count i p.parts * i = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0

pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ ∀ (b' : ℕ),
    b' ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b' + 1) then f i (b' + 1) else 0) = 0

Tactic:
·

Goal state after:
case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    if Multiset.count i p.parts * i = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
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
⊢ Function.Injective fun i ↦ (↑i + 1) * m - 1

pp: case refine_2
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
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1

pp: case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m

Tactic:
·

Goal state after:
case refine_1
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
⊢ Function.Injective fun i ↦ (↑i + 1) * m - 1
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case refine_1
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)
⊢ Tendsto (fun x_1 ↦ x ^ ((k + 1) * x_1)) atTop (𝓝 0)

pp: case refine_2
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)
⊢ Tendsto (fun x_1 ↦ x ^ (2 * k + x_1 + 3) - 1) atTop (𝓝 (0 - 1))

pp: case refine_3
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)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))

Tactic:
·

Goal state after:
case refine_1
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)
⊢ Tendsto (fun x_1 ↦ x ^ ((k + 1) * x_1)) atTop (𝓝 0)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case refine_2
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)
⊢ Tendsto (fun x_1 ↦ x ^ (2 * k + x_1 + 3) - 1) atTop (𝓝 (0 - 1))

pp: case refine_3
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)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))

Tactic:
·

Goal state after:
case refine_2
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)
⊢ Tendsto (fun x_1 ↦ x ^ (2 * k + x_1 + 3) - 1) atTop (𝓝 (0 - 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case refine_3
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)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))

Tactic:
·

Goal state after:
case refine_3
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)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_2
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
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1

pp: case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m

Tactic:
·

Goal state after:
case refine_2
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
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_2
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
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1

pp: case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m

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

Goal state after:
case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m

Tactic:
·

Goal state after:
case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m
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 ℕ
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
⊢ Set.MapsTo toFinsuppAntidiag ↑univ ↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d)

pp: case refine_2
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
⊢ ∀ i ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
    i ∉ toFinsuppAntidiag '' ↑univ →
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
          (coeff (i i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1))) =
        0

pp: case refine_3
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
⊢ ∀ i ∈ univ,
    (Multiset.toFinsupp i.parts).prod f =
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
        (coeff (i.toFinsuppAntidiag i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1)))

Tactic:
·

Goal state after:
case refine_1
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
⊢ Set.MapsTo toFinsuppAntidiag ↑univ ↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d)
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
⊢ 0 < κ + 1

Tactic:
linarith [connectivity_nonneg hK.le hS]

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

Goal state before:
pp: case refine_2
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
⊢ ∀ i ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
    i ∉ toFinsuppAntidiag '' ↑univ →
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
          (coeff (i i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1))) =
        0

pp: case refine_3
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
⊢ ∀ i ∈ univ,
    (Multiset.toFinsupp i.parts).prod f =
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
        (coeff (i.toFinsuppAntidiag i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1)))

Tactic:
·

Goal state after:
case refine_2
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
⊢ ∀ i ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
    i ∉ toFinsuppAntidiag '' ↑univ →
      ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
          (coeff (i i_1)) (1 + ∑' (j : ℕ), f i_1 (j + 1) • X ^ (i_1 * (j + 1))) =
        0