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

Goal state before:
pp: case h₁
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ a = x ↔ φ a = t

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case h₂.h₁
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
a✝ : φ a = t
⊢ b = x ↔ φ b = t

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case h₂.h₂
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
a✝¹ : φ a = t
a✝ : φ b = t
⊢ G.Adj s s ↔ False

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case h₃.h₁
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
a✝ : ¬φ a = t
⊢ b = x ↔ φ b = t

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))

Tactic:
insert_erase <| mem_erase_of_ne_of_mem hne.symm h2,

Goal state after:
case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (t.erase x)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
⊢ G.CliqueFreeOn s n

Tactic:
rintro t hts ht
  obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)
  exact hG ((coe_subset.2 hut).trans hts) ⟨ht.isClique.subset hut, hu⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∀ w ∈ p.support, w ∈ q.support → w ≠ u → w = v
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
refine ⟨u, v, p, q, p.isSubwalk_rfl, q.isSubwalk_rfl, ?_⟩
    refine hp.isCycle_append (isPath_reverse_iff q |>.mpr hq) (fun _ ↦ ?_) ?_
    · grind [dropLast_support_concat, IsPath.support_nodup, support_reverse, cons_tail_support]
    · grind [length_reverse, eq_of_length_le_one]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
he : e ∈ G.edgeSet
⊢ {b | b ∈ sᶜ ∧ b ∈ e}.Nonempty

Tactic:
obtain ⟨v, w⟩ := e

Goal state after:
case mk
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
⊢ {b | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ ∃ s, Gᶜ.IsNClique (sSup {n | ∃ s, Gᶜ.IsNClique n s}) s

Tactic:
exact exists_isNClique_cliqueNum

Goal state after:
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
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ 2 * (ε / 8) ≤ ↑(G.edgeDensity s Y)

Tactic:
by rwa [that]

Goal state after:
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
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ 2 * (ε / 8) ≤ ↑(G.edgeDensity s Z)

Tactic:
by rwa [that]

Goal state after:
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
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ 2 * (ε / 8) ≤ ↑(G.edgeDensity Y Z)

Tactic:
by rwa [that]

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hst : Disjoint s t
hsu : Disjoint s u
htu : Disjoint t u
x₁ x₂ y₁ y₂ z₁ z₂ : α
hx₁ : x₁ ∈ s
hx₂ : x₂ ∈ s
hy₁ : y₁ ∈ t
hy₂ : y₂ ∈ t
hz₁ : z₁ ∈ u
hz₂ : z₂ ∈ u
h :
  ((x₁ = x₂ ∨ x₁ = y₂ ∨ x₁ = z₂) ∧ (y₁ = x₂ ∨ y₁ = y₂ ∨ y₁ = z₂) ∧ (z₁ = x₂ ∨ z₁ = y₂ ∨ z₁ = z₂)) ∧
    (x₂ = x₁ ∨ x₂ = y₁ ∨ x₂ = z₁) ∧ (y₂ = x₁ ∨ y₂ = y₁ ∨ y₂ = z₁) ∧ (z₂ = x₁ ∨ z₂ = y₁ ∨ z₂ = z₁)
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Tactic:
grind [Finset.disjoint_left]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A

Tactic:
Set.image_image,

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ ↑A = (fun x ↦ Prod.map Fin.val Fin.val (Prod.map Nat.cast Nat.cast x)) '' ↑A
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
⊢ a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b

Tactic:
prod_erase_eq_div hat,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
⊢ a = (∏ b ∈ u, b) / ((∏ x ∈ t, x) / a)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
    (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)))
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
    (4 ^ #P.parts * 4 ^ #P.parts)
r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))
s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
t : ℝ := ↑(G.edgeDensity U V)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ ε ^ 5 / 49
hqt : |q - t| ≤ ε ^ 5 / 49
⊢ ε ^ 5 ≤ ε

Tactic:
simpa using pow_le_pow_of_le_one (by sz_positivity) hε₁ (show 1 ≤ 5 by simp)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅

Tactic:
simp [← (Nat.zero_le _).not_lt_iff_eq', imp_iff_or_not, or_comm]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ↑A = Fin.val '' Nat.cast '' ↑A

Tactic:
Set.image_image,

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ↑A = (fun x ↦ ↑↑x) '' ↑A
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ (bit b n).bitIndices.SortedLT

Tactic:
suffices List.Pairwise (fun a b ↦ a < b) n.bitIndices by
      cases b <;> simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]

Goal state after:
case bit
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ List.Pairwise (fun a b ↦ a < b) n.bitIndices
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
h✝ : (crossProduct ↑x✝⁴) ↑x✝¹ = 0
⊢ x✝⁵ ≈ x✝⁴

Tactic:
use a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // fixedPoints ⇑f = {a} } ⊕ { f // fixedPoints ⇑f = ∅ } ≃ ↑(derangements ↑{a}ᶜ) ⊕ ↑(derangements α)

Tactic:
refine
        Equiv.sumCongr ((derangements.subtypeEquiv _).trans <|
            subtypeEquivRight fun x => ?_).symm
          (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ a_1 ∈ fixedPoints ⇑x) ↔ fixedPoints ⇑x = {a}
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Tactic:
have h1 : ∀ a : Fin (n + 1), card ({a}ᶜ : Set (Fin (n + 1))) = card (Fin n) := by
    intro a
    rw [Fintype.card_compl_set]
    simp
  have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by simp only [card_fin, card_option]
  -- rewrite the LHS and substitute in our fintype-level equivalence
  simp only [card_derangements_invariant h2,
    card_congr
      (@derangementsRecursionEquiv (Fin (n + 1))
        _), -- push the cardinality through the Σ and ⊕ so that we can use `card_n`
    card_sigma,
    card_sum, card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin,
    mul_add, Nat.cast_id]

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

Goal state before:
pp: ⊢ treesOfNumNodesEq 0 = {nil}

Tactic:
by rw [treesOfNumNodesEq]

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ U :: (↑p).dropLast.tail ++ [D] = ↑p

Tactic:
have h' := toList_ne_nil.mpr h

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
⊢ U :: (↑p).dropLast.tail ++ [D] = ↑p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
⊢ f • (g + h) = f • g + f • h

Tactic:
by ext; exact Eq.trans (sum_congr rfl fun x _ ↦ smul_add _ _ _) sum_add_distrib

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

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

Tactic:
let r : DyckWord := q.take _ hc

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
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
⊢ p ≤ q
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inr.inl
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

Tactic:
exact ih.trans (hm ▸ semilength_insidePart_lt hr).le

Goal state after:
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 β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
⊢ eulerChar 𝕜 (α × β) = eulerChar 𝕜 α * eulerChar 𝕜 β

Tactic:
simp [eulerChar, ← mu_prod_mu]

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 ↦ ∑ p_1, (Multiset.toFinsupp p_1.parts).prod fun i c ↦ if p i then 1 else 0

Tactic:
Finsupp.prod,

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 ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, p i_1 then 1 else 0)) =
    PowerSeries.mk fun n ↦ ∑ p_1, ∏ x ∈ (Multiset.toFinsupp p_1.parts).support, if p x then 1 else 0
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
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ (Multiset.toFinsupp p.parts).prod f =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))

Tactic:
Finsupp.prod,

Goal state after:
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
⊢ ∏ a ∈ (Multiset.toFinsupp p.parts).support, f a ((Multiset.toFinsupp p.parts) a) =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (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 ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, Multiset.count i_1 i.parts < m then 1 else 0)) =
    PowerSeries.mk fun n ↦ ∑ p, (Multiset.toFinsupp p.parts).prod fun i c ↦ if c < m then 1 else 0

Tactic:
Finsupp.prod,

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 ↦ ↑(∑ i, if ∀ i_1 ∈ i.parts, Multiset.count i_1 i.parts < m then 1 else 0)) =
    PowerSeries.mk fun n ↦
      ∑ p, ∏ x ∈ (Multiset.toFinsupp p.parts).support, if (Multiset.toFinsupp p.parts) x < 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
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0

Tactic:
rw [tsum_eq_single (Multiset.count i p.parts - 1) ?_]

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

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
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
refine Nat.mul_left_cancel zero_lt_two ?_

Goal state after:
case succ.succ
n : ℕ
hn : 1 < n + 1 + 1
⊢ 2 * (n + 1 + 1 + 1).smallSchroder =
    2 *
      (3 * (n + 1 + 1).smallSchroder +
        2 * ∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder)
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)

Tactic:
#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. -/

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)
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
#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. -/

Goal state after:
case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
#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. -/

Goal state after:
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
hb : a * b ∈ a •> n⁻¹ •> N
⊢ a ∈ n⁻¹ •> N ∩ a •> n⁻¹ •> N

Tactic:
by
        simpa only [mem_inter] using! ⟨ha, self_mem_smul_carrier a⟩

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
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:
rw [← coe_smul_finset, mem_coe] at *
      apply smul_mem_smul_finset (a := a) at hb
      rw [smul_eq_mul] at hb
      have : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty := ⟨a, by
        simpa only [mem_inter] using! ⟨ha, self_mem_smul_carrier a⟩⟩
      simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a) this] using! hb

Goal state after:
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 α
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s

Tactic:
have := noAccidental hs
  rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]

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

Goal state before:
pp: ⊢ Nat.cast =O[atTop] fun n ↦ 3⁻¹ * ↑n

Tactic:
exact (isBigO_refl ..).const_mul_right (by simp)

Goal state after: