mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#({x | G.Adj x.1 x.2} \ {x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}))

Tactic:
cast_card_sdiff

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#{x | G.Adj x.1 x.2}) - ↑(#{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})

α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ {x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2} ⊆ {x | G.Adj x.1 x.2}
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)

Tactic:
simpa only [mul_comm] using hε

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : ∃ a b c, (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
⊢ ∃ x ∈ t, toTriangle x = s

Tactic:
obtain ⟨x, y, z, hxy, hxz, hyz, rfl⟩ := h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
⊢ ∃ x_1 ∈ t, toTriangle x_1 = {x, y, z}
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ y₁ - x₂ + (y₂ - x₁) = y₁ - x₁ + (y₁ - x₁)

Tactic:
by -- TODO: This really ought to just be `by linear_combination h`
    rw [sub_add_sub_comm, add_comm, add_sub_add_comm, add_right_cancel_iff,
      sub_eq_sub_iff_add_eq_add, add_comm, hxy, add_comm]

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ (Fintype.card α).choose r

Tactic:
rw [Fintype.card, ← card_powersetCard]

Goal state after:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ #(powersetCard r univ)
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case prime
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i

Tactic:
| prime p hp =>

Goal state after:
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case composite
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Tactic:
| composite m hm ihm n hn ihn =>

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁

Tactic:
by
  simp_rw [← sdiff_eq_empty_iff_subset]
  by_contra! h
  have ⟨⟨s, hs⟩, t, ht⟩ := h
  rw [mem_sdiff] at hs ht
  obtain hst | hst | hts := trichotomous_of (α := Colex (Finset α)) (· < ·) (toColex s) (toColex t)
  · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩
  · simp only [toColex_inj] at hst
    exact ht.2 <| hst ▸ hs.1
  · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ ⇑toColex) = #t
le : toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
⊢ t ∈ 𝒜

Tactic:
obtain p | p := le.eq_or_lt

Goal state after:
case refine_2.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ ⇑toColex) = #t
le : toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
p : toColex t = toColex (𝒜.sup' h𝒜₀ ⇑toColex)
⊢ t ∈ 𝒜

case refine_2.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
cards : #(𝒜.sup' h𝒜₀ ⇑toColex) = #t
le : toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
p : toColex t < toColex (𝒜.sup' h𝒜₀ ⇑toColex)
⊢ t ∈ 𝒜
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ∑ i ∈ Finset.range (n + 1), (↑n + 1) * ((-1) ^ i * ↑((i + 1).ascFactorial (n - i))) =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))

Tactic:
Finset.sum_congr rfl

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ (Finset.range (n + 1)).sum ?m.104 = ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))

case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ∀ x ∈ Finset.range (n + 1), (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = ?m.104 x

n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ℕ → ℤ
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z = x⁻¹ * (y * w)

Tactic:
← hzxwy,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z = x⁻¹ * (x * z)
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
⊢ ⊥.toSimpleGraphInclusive = ⊥

Tactic:
ext; exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

Goal state after:
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
⊢ ⊥.toSimpleGraphStrict = ⊥

Tactic:
ext; exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2
⊢ lineCount L p = pointCount P l

Tactic:
← Set.toFinset_compl

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
step3 : ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, lineCount L i.1 = ∑ i ∈ {i | i.1 ∈ i.2}ᶜ.toFinset, pointCount P i.2
⊢ lineCount L p = pointCount P l
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
obtain ⟨f, _, hf2⟩ := HasLines.exists_bijective_of_card_eq h
      have : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩
      have := Fintype.one_lt_card_iff_nontrivial.mp ((congr_arg _ h).mpr Fintype.one_lt_card)
      have h₁ : ∀ p : P, 0 < lineCount L p := fun p =>
        Exists.elim (exists_ne p) fun q hq =>
          (congr_arg _ Nat.card_eq_fintype_card).mpr
            (Fintype.card_pos_iff.mpr ⟨⟨mkLine hq, (mkLine_ax hq).2⟩⟩)
      have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l))
      obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁))
      by_cases hl₂ : p ∈ l₂
      · exact ⟨p, hl₁, hl₂⟩
      have key' : Fintype.card { q : P // q ∈ l₂ } = Fintype.card { l : L // p ∈ l } :=
        ((HasLines.lineCount_eq_pointCount h hl₂).trans Nat.card_eq_fintype_card).symm.trans
          Nat.card_eq_fintype_card
      have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)
      let f : { q : P // q ∈ l₂ } → { l : L // p ∈ l } := fun q =>
        ⟨mkLine (this q), (mkLine_ax (this q)).1⟩
      have hf : Function.Injective f := fun q₁ q₂ hq =>
        Subtype.ext ((eq_or_eq q₁.2 q₂.2 (mkLine_ax (this q₁)).2
            ((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mpr (mkLine_ax (this q₂)).2)).resolve_right
            fun h => (congr_arg (p ∉ ·) h).mp hl₂ (mkLine_ax (this q₁)).1)
      have key' := ((Fintype.bijective_iff_injective_and_card f).mpr ⟨hf, key'⟩).2
      obtain ⟨q, hq⟩ := key' ⟨l₁, hl₁⟩
      exact ⟨q, (congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hq)).mp (mkLine_ax (this q)).2, q.2⟩

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ lineCount L p • order P L + 1 = order P L ^ 2 + order P L + 1

Tactic:
lineCount_eq,

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ (order P L + 1) • order P L + 1 = order P L ^ 2 + order P L + 1
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h
K : Type u_3
inst✝ : Field K
c d : ℙ K (Fin 3 → K)
a : Fin 3 → K
ha : a ≠ 0
hac : (Projectivization.mk K a ha).orthogonal c
had : (Projectivization.mk K a ha).orthogonal d
b : Fin 3 → K
hb : b ≠ 0
hbc : (Projectivization.mk K b hb).orthogonal c
hbd : (Projectivization.mk K b hb).orthogonal d
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ c = d

Tactic:
induction c with

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i)

pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
· refine sum_congr rfl fun i _ => ?_
        rw [gosper_trick i.is_le, mul_div]

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
⊢ uniformBell 1 n = 1

Tactic:
by
  simp only [uniformBell_eq, Finset.range_one, Finset.prod_singleton, zero_mul,
    zero_add, choose_self]

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

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
h : ↑r ++ ↑p = ↑q
e : r' = ↑r
⊢ p ≤ q

Tactic:
replace h : r + p = q := DyckWord.ext h

Goal state after:
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ q
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ powMulProdOneSubPow k n x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) n x =
    x ^ ((k + 1) * (n + 1)) * (x ^ (2 * k + (n + 1) + 3) - 1) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 2)) -
      x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))

Tactic:
Finset.prod_range_succ,

Goal state after:
R : Type u_1
inst✝ : CommRing R
k n : ℕ
x : R
⊢ powMulProdOneSubPow k n x + x ^ (3 * k + 5) * powMulProdOneSubPow (k + 1) n x =
    x ^ ((k + 1) * (n + 1)) * (x ^ (2 * k + (n + 1) + 3) - 1) *
        ((∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))) * (1 - x ^ (k + n + 2))) -
      x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))
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

Tactic:
rw [mul_comm]

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 i * Multiset.count i p.parts = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
by
  have : (#(A ∩ B) + #(A ∪ B) : ℝ) = #A + #B := mod_cast card_inter_add_card_union A B
  have : K * #(A ∩ B) + K * #(A ∪ B) = K * #A + K * #B := by simp only [← mul_add, this]
  have : (#(A * S ∩ (B * S)) + #(A * S ∪ B * S) : ℝ) = #(A * S) + #(B * S) :=
    mod_cast card_inter_add_card_union (A * S) (B * S)
  have : (#((A ∩ B) * S) : ℝ) ≤ #(A * S ∩ (B * S)) := by grw [inter_mul_subset]
  simp_rw [expansion, union_mul]
  nlinarith

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

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

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

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
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Tactic:
have h := (multipliable_one_sub_X_pow R).hasProd

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
this✝ : TopologicalSpace R := ⊥
this : DiscreteTopology R
h : HasProd (fun n ↦ 1 - X ^ (n + 1)) (∏' (b : ℕ), (1 - X ^ (b + 1)))
⊢ ∀ᶠ (s : Finset ℕ) in atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
h : V(G) ⊆ X ∧ E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ (noEdge X β).IsLink e x y

Tactic:
simpa [h] using he.edge_mem

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
⊢ G.Inc e x

Tactic:
rw [h.2, ← show z = v from (show z ∈ {v} from hrw ▸ hzw.left_mem)]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
⊢ G.Inc e z
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u✝ v✝ : α
e f : β
X Y : Set α
G : Graph α β
u v : ↑V(G)
⊢ u ≠ v ∧ G.Adj ↑u ↑v → v ≠ u ∧ G.Adj ↑v ↑u

Tactic:
grind [adj_comm]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
inst✝ : M.RankPos
hD : M.Coindep D
⊢ (M ＼ D).RankPos

Tactic:
by
  rw [rankPos_iff, hD.delete_isBase_iff]
  simp [M.empty_not_isBase]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f = m.degree f - m.degree b + m.degree b

Tactic:
ext d

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
d : σ
⊢ (m.degree f) d = (m.degree f - m.degree b + m.degree b) d
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ _x ∈ s, x = ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := ⋯
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∀ x_1 ∈ s, x = ↑(↑l ⟨x, xs⟩ x_1)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ∑ i ∈ sᶜ, ↑(↑l ⟨x, xs⟩ i)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := ⋯
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∀ x_1 ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun x_1)).getD 0 = ↑(↑l ⟨x, xs⟩ x_1)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
m : PEmpty.{u_2 + 1} →₀ ℕ
⊢ m = 0

Tactic:
ext d

Goal state after:
case h_empty
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
m : PEmpty.{u_2 + 1} →₀ ℕ
d : PEmpty.{u_2 + 1}
⊢ m d = 0 d
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
hdep2 : (M ／ K).Dep (C' \ K)
⊢ C' \ K ⊆ C'

Tactic:
exact sdiff_subset

Goal state after: