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

Goal state before:
pp: case succ
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_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∑ 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) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ x_1 ∈ Finset.range (n + 1), (-1) ^ x_1 * (x ^ (x_1 * (3 * x_1 + 1) / 2) - x ^ ((x_1 + 1) * (3 * x_1 + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1 + 1) * (3 * (n + 1) + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
]

Goal state after:
case succ
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_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∑ 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) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ x_1 ∈ Finset.range (n + 1), (-1) ^ x_1 * (x ^ (x_1 * (3 * x_1 + 1) / 2) - x ^ ((x_1 + 1) * (3 * x_1 + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1 + 1) * (3 * (n + 1) + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x
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 : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = ((n + 1) * (3 * n + 4) + 2 * (2 * n + 3)) / 2

Tactic:
]

Goal state after:
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 : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = ((n + 1) * (3 * n + 4) + 2 * (2 * n + 3)) / 2
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

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

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

Tactic:
]

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

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0

Tactic:
]

Goal state after:
case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0
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
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb : b ∈ n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N

Tactic:
]

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
a b : G
ha : a ∈ n⁻¹ •> N
hb : b ∈ n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
]

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (2 * (n + 1 + 1).smallSchroder) +
      ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
    6 * (n + 2).smallSchroder + 4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder
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
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N

Tactic:
]

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
a b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
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 : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = ((n + 1) * (3 * n + 4) + 2 * (3 * n + 5)) / 2

Tactic:
]

Goal state after:
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 : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = ((n + 1) * (3 * n + 4) + 2 * (3 * n + 5)) / 2
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
⊢ ↑n < ↑((k + 1) * m) + (∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < ↑((k + 1) * m) + (∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order
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
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha : a ∈ n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N

Tactic:
]

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
a : G
ha : a ∈ n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
⊢ 0 + 0 = 0

Tactic:
]

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

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ n + 1 + (n + 1).choose 2 = n + 1 + (n + 1).choose (succ 1)

Tactic:
]

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

Goal state before:
pp: case succ
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1) * n ! + 0 = (n + 1)!

Tactic:
]

Goal state after:
case succ
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1) * n ! + 0 = (n + 1)!
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
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha✝ : a ∈ n⁻¹ •> N
ha : 1 ∈ a⁻¹ •> n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N

Tactic:
]

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
a : G
ha✝ : a ∈ n⁻¹ •> N
ha : 1 ∈ a⁻¹ •> n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) (pentagonalSeries R)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
⊢ (0 + 1) * 1 + 0 = 1

Tactic:
]

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

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ n + 1 + (n + 1).choose 2 = n + 1 + (n + 1).choose (succ 1)

Tactic:
]

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)
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)

Tactic:
]

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)
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
G H : SimpleGraph α
⊢ ℕ

Tactic:
exact Nat.findGreatest (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
    #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) ((card α).choose 3)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #((SimpleGraph.map (⇑f) G).cliqueFinset 3) = #((SimpleGraph.map (⇑f) G).cliqueFinset 3)

pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ 3 ≠ 1

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ 3 ≠ 1
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ n.choose 3 = n.choose 3

Tactic:
]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) (X ^ i)) atTop (𝓝 ((coeff d) 0))

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) (X ^ i)) atTop (𝓝 ((coeff d) 0))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Multipliable fun n ↦ 1 - X ^ (n + k + 1)

pp: case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)

Tactic:
· exact Pentagonal.multipliable_one_sub_X_pow R

Goal state after:
case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (d : ℕ),
    Tendsto
      (fun i ↦
        (coeff d)
          ((-1) ^ (i + 1) * X ^ ((i + 1) * (3 * i + 4) / 2) *
            ∑' (n : ℕ), X ^ ((i + 1) * n) * ∏ i_1 ∈ Finset.range (n + 1), (1 - X ^ (i + i_1 + 1))))
      atTop (𝓝 ((coeff d) 0))

Tactic:
]

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (d : ℕ),
    Tendsto
      (fun i ↦
        (coeff d)
          ((-1) ^ (i + 1) * X ^ ((i + 1) * (3 * i + 4) / 2) *
            ∑' (n : ℕ), X ^ ((i + 1) * n) * ∏ i_1 ∈ Finset.range (n + 1), (1 - X ^ (i + i_1 + 1))))
      atTop (𝓝 ((coeff d) 0))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))) =
    0

Tactic:
]

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))) =
    0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-1) ^ (k + 1)).order + (X ^ ((k + 1) * (3 * k + 4) / 2)).order +
      (∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order

Tactic:
]

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n <
    ((-1) ^ (k + 1)).order + (X ^ ((k + 1) * (3 * k + 4) / 2)).order +
      (∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))).order
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (n + 1) * 2 ≤ (k + 1) * (3 * k + 4)

Tactic:
]

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (n + 1) * 2 ≤ (k + 1) * (3 * k + 4)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : CommRing α
s : Finset α
x : α × α × α
inst✝ : Fact (IsUnit 2)
⊢ ∀ ⦃a b c c' : α⦄, (a, b, c) ∈ triangleIndices s → (a, b, c') ∈ triangleIndices s → c = c'

Tactic:
simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
    rintro _ _ _ _ x a ha rfl rfl rfl y b hb rfl h rfl
    simpa [(Fact.out (p := IsUnit (2 : α))).mul_right_inj, eq_comm] using h

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 n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * (x ^ pentagonal (-↑i) - x ^ pentagonal (↑i + 1)))
    (map (fun a ↦ a + 1) atTop) (𝓝 (∏' (n : ℕ), (1 - x ^ (n + 1))))

Tactic:
]

Goal state after:
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 n ↦ x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
hlhs : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hrhs : Summable fun k ↦ (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
htail :
  Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
    atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    ∏' (n : ℕ), (1 - x ^ (n + 1)) -
        (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
      ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * (x ^ pentagonal (-↑i) - x ^ pentagonal (↑i + 1)))
    (map (fun a ↦ a + 1) atTop) (𝓝 (∏' (n : ℕ), (1 - x ^ (n + 1))))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : CommRing α
s : Finset α
inst✝¹ : Fact (IsUnit 2)
hs : ThreeAPFree ↑s
inst✝ : DecidableEq α
this : NoAccidental (triangleIndices s)
⊢ 3 * (Fintype.card α * #s) = 3 * (Fintype.card α * #s)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h :
  ∀ (d : ℕ),
    Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 - X ^ (b + 1)))) (SummationFilter.unconditional ℕ).filter
      (𝓝 ((coeff d) (pentagonalSeries R)))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h :
  ∀ (d : ℕ),
    Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 - X ^ (b + 1)))) (SummationFilter.unconditional ℕ).filter
      (𝓝 ((coeff d) (pentagonalSeries R)))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)