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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (∑ x ∈ P.parts.offDiag with ¬G.IsUniform ε x.1 x.2, ε ^ 4 / 3 - ↑(#P.parts.offDiag) * (ε ^ 5 / 25))

Tactic:
sum_const,

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (#({x ∈ P.parts.offDiag | ¬G.IsUniform ε x.1 x.2}) • (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25))
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ ∑ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m ≤
    2 ^ (#P.parts - 1) * m

Tactic:
sum_const,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ #({B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}) • m ≤
    2 ^ (#P.parts - 1) * m
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ 2 ^ (#P.parts - 1) * m

Tactic:
by
  have hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U :=
    nonuniformWitness_mem_nonuniformWitnesses h₂ hV hUV
  have q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
      {B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts |
        B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
        fun B => B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id := by
    intro x hx
    rw [← biUnion_filter_atomise hX (G.nonuniformWitness_subset h₂), star, mem_sdiff,
      mem_biUnion] at hx
    simp only [not_exists, mem_biUnion, and_imp, mem_filter,
      not_and, mem_sdiff, id, mem_sdiff] at hx ⊢
    obtain ⟨⟨B, hB₁, hB₂⟩, hx⟩ := hx
    exact ⟨B, hB₁, hB₂, fun A hA AB => hx A hA <| AB.trans hB₁.2.1⟩
  apply (card_le_card q).trans (card_biUnion_le.trans _)
  trans ∑ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts with
    B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m
  · suffices ∀ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts,
        #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m by
      gcongr with B hB
      exact this B <| filter_subset _ _ hB
    intro B hB
    unfold chunk
    split_ifs with h₁
    · convert! card_parts_equitabilise_subset_le _ (card_aux₁ h₁) hB
    · convert! card_parts_equitabilise_subset_le _ (card_aux₂ hP hU h₁) hB
  grw [sum_const, smul_eq_mul, card_filter_atomise_le_two_pow (s := U) hX,
    Finpartition.card_nonuniformWitnesses_le, filter_subset] <;> simp

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.degree v = 0

Tactic:
rw [← G'.coe_degree ⟨v, hv⟩]

Goal state after:
case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.coe.degree ⟨v, hv⟩ = 0
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
hv : v ≠ t
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj v w ↔ G.Adj v w

Tactic:
by simp [replaceVertex, hv, hw]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk u w
⊢ (p.reverseAux q).length = p.length + q.length

Tactic:
by
  induction p with
  | nil => simp!
  | cons _ _ ih => simp [ih, Nat.succ_add, add_assoc]

Goal state after:
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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
| (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
SimpleGraph.edgeDensity_def,

Goal state after:
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
| (1 - ε ^ 5 / 50) * ↑(↑(#(G.interedges (A.biUnion id) (B.biUnion id))) / (↑(#(A.biUnion id)) * ↑(#(B.biUnion id))))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ (nil.drop 0).getVert m = nil.getVert (0 + m)

Tactic:
simp [*, drop, add_right_comm]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).getVert m = nil.getVert (n✝ + 1 + m)

Tactic:
simp [*, drop, add_right_comm]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
⊢ ((cons h✝ p✝).drop 0).getVert m = (cons h✝ p✝).getVert (0 + m)

Tactic:
simp [*, drop, add_right_comm]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (n✝ + 1 + m)

Tactic:
simp [*, drop, add_right_comm]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.take 0 = nil.copy ⋯ ⋯

Tactic:
cases p <;> simp [take]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case zero
V : Type u
G : SimpleGraph V
v u : V
p : G.Walk u v
h : p.length ≤ 0
⊢ p.take 0 = p.copy ⋯ ⋯

Tactic:
cases p <;> simp [take] at h ⊢

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ∈ {i | i ≤ (cons h p).length}
m : ℕ
hm : m ∈ {i | i ≤ (cons h p).length}
hnm : (cons h p).getVert n = (cons h p).getVert m
⊢ n = m

Tactic:
| @cons v w u h p ihp =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i - 1 ∈ {i | i ≤ p.length - 1}

Tactic:
simp only [Set.mem_ofPred_eq, Nat.sub_le_iff_le_add]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
x✝ : p.tail.IsPath ∧ 3 ≤ p.length
h₁ : p.tail.IsPath
h₂ : 3 ≤ p.length
⊢ p.IsCycle

Tactic:
cases p with
  | nil => simp_all
  | cons h' p =>
    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
    have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
    have := p.isPath_iff_injective_get_support.mp h₁ this
    lia

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ G.CliqueFree n

Tactic:
rw [cliqueFree_iff]

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ IsEmpty ((completeGraph (Fin n)).Copy G)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : 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
⊢ ∃ s, x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)

Tactic:
use (t.erase x).erase y, erase_right_comm (a := x) ▸ (notMem_erase _ _), notMem_erase _ _

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
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s

Tactic:
rw [isNClique_iff]

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsClique ↑s ∧ #s = n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : Gᶜ.IsMaximumClique s
⊢ Maximal Gᶜ.IsClique ↑s

Tactic:
exact IsMaximumClique.isMaximalClique s M

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

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∩ t)) = ↑(#s) + ↑(#t) - ↑(#(s ∪ t))

Tactic:
by
  rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := ⋯
this :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ #X' • (ε ^ 3 * ↑(#t) * ↑(#u))

Tactic:
nsmul_eq_mul

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#X') * (ε ^ 3 * ↑(#t) * ↑(#u))
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:
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.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case composite.succ.refine_1
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
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this✝ : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
this : t₀ ∉ 𝒜
⊢ (↑(cons t₀ 𝒜 this)).Pairwise Disjoint

Tactic:
simp only [cons_eq_insert, coe_insert, Set.pairwise_insert_of_symm, mem_coe, ne_eq]
      exact ⟨h𝒜disj, fun t ht _ ↦ sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id ht⟩

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w] ↔ 0 = 0

Tactic:
eq_self,

Goal state after:
case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w] ↔ True
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s t : Finset α
hf : StrictMono f
⊢ toColex (image f s) ≤ toColex (image f t) ↔ toColex s ≤ toColex t

Tactic:
by
  simp [toColex_le_toColex, hf.le_iff_le, hf.injective.eq_iff]

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
l : L
x✝ : l ∈ univ
⊢ ∑ x ∈ {p | p ∈ l}.toFinset, lineCount L (f l) = ∑ x ∈ {l_1 | f l ∈ l_1}.toFinset, lineCount L (f l)

Tactic:
sum_const,

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
l : L
x✝ : l ∈ univ
⊢ #{p | p ∈ l}.toFinset • lineCount L (f l) = #{l_1 | f l ∈ l_1}.toFinset • lineCount L (f l)
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
a b c d x✝ y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
⊢ ∀ (x_1 : G), x_1⁻¹ ∈ A → ∀ x_2 ∈ A, x_1 * x_2 = x → ∃ x_3, x_3⁻¹ ∈ A ∧ ∃ y ∈ A, x_3 * y = x⁻¹

Tactic:
rintro a ha b hb rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ ∃ x, x⁻¹ ∈ A ∧ ∃ y ∈ A, x * y = (a * b)⁻¹
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Tactic:
have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self

Goal state after:
case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
nth_rw 2 [← p.toList.dropLast_append_getLast h', ← p.toList.dropLast.take_append_drop 1]

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = take 1 (↑p).dropLast ++ drop 1 (↑p).dropLast ++ [(↑p).getLast h']
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)

Tactic:
count_take_firstReturn_add_one h

Goal state after:
case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count D (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)
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 : ℕ
hx : x ∈ s \ p.parts.toFinset
⊢ (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

Tactic:
rw [mem_sdiff, Multiset.mem_toFinset] at hx

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 : ℕ
hx : x ∈ s ∧ x ∉ p.parts
⊢ (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
⊢ n * n.stirlingFirst (k + 1) + 0 = 0

Tactic:
stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk),

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
⊢ n * 0 + 0 = 0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

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

Tactic:
neg_neg,

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

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ IsUnit 2

Tactic:
simpa
    using! (ZMod.unitOfCoprime 2 this).isUnit

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))
h1 : ∀ (k : ℕ), pentagonal (↑k + 1) = (k + 1) * (3 * k + 2) / 2
h2 : ∀ (k : ℕ), pentagonal (-↑k) = k * (3 * k + 1) / 2
⊢ Tendsto
    (fun x_1 ↦
      ∏' (n : ℕ), (1 - x ^ (n + 1)) -
          (-1) ^ (x_1 + 1) * x ^ ((x_1 + 1) * (3 * x_1 + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow x_1 n x -
        ∏' (n : ℕ), (1 - x ^ (n + 1)))
    atTop (𝓝 0)

Tactic:
simpa [powMulProdOneSubPow] using htail.neg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
h : V(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ ⊥.IsLink e x y

Tactic:
simpa [h] using he.left_mem

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

Goal state before:
pp: α : Type u_1
e e' : Set α
H : Hypergraph α
he : e ∈ E(H)
he' : e' ∈ E(H)
⊢ e = e' ↔ ∀ x ∈ V(H), x ∈ e ↔ x ∈ e'

Tactic:
by
  grind [he.subset_vertexSet, he'.subset_vertexSet]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
      rintro (_ | ⟨a⟩)
      · rfl
      · exact (h ⟨a⟩).elim

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ (M ＼ D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D

Tactic:
rw [delete_eq_restrict, restrict_isCircuit_iff, and_congr_right_iff, subset_sdiff,
    and_iff_right_iff_imp]

Goal state after:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → Disjoint C D → C ⊆ M.E