mathlib-initiative/mathlib-tactics huggingface dataset:
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
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) ≤ ↑(#𝒜) * ↑(#s) * ((↑m + 1) / ↑m)

Tactic:
mul_div_assoc',

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
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) ≤ ↑(#𝒜) * ↑(#s) * (↑m + 1) / ↑m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : u ∈ p.support
⊢ (match v, p, u, h with
    | .(u), nil, u_1, h => ⋯.mpr nil
    | w, cons r p, u_1, h =>
      if hx : u = u_1 then
        Eq.ndrec (motive := fun u_2 ↦ u_2 ∈ (cons r p).support → G.Walk u_2 w) (fun h ↦ cons r p) hx h
      else p.dropUntil u_1 ⋯) =
    p

Tactic:
split

Goal state after:
case h_1
V : Type u
G : SimpleGraph V
u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
h : u ∈ nil.support
⊢ ⋯.mpr nil = nil

case h_2
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
v✝ : V
r✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : u ∈ (cons r✝ p✝).support
⊢ (if hx : u = u then Eq.ndrec (motive := fun u_1 ↦ u_1 ∈ (cons r✝ p✝).support → G.Walk u_1 v) (fun h ↦ cons r✝ p✝) hx h
    else p✝.dropUntil u ⋯) =
    cons r✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
simpa using p.darts_takeUntil_prefix_darts h |>.length_le

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
this✝ : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
this : List.count (p.getVert n) ((p.takeUntil (p.getVert n) h).support.dropLast ++ [p.getVert n]) = 1
⊢ False

Tactic:
grind [List.not_mem_of_count_eq_zero]

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

Goal state before:
pp: case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : (cons h✝ p✝).length ≤ n + 1
⊢ (cons h✝ p✝).take (n + 1) = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
length_cons,

Goal state after:
case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝¹ : G.Adj u v✝
p✝ : G.Walk v✝ v
h✝ : (cons h✝¹ p✝).length ≤ n + 1
h : p✝.length + 1 ≤ n + 1
⊢ (cons h✝¹ p✝).take (n + 1) = (cons h✝¹ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
hs,

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ (completeMultipartiteGraph V).CliqueFree n

Tactic:
by
  rw [cliqueFree_iff, isEmpty_iff]
  intro f
  obtain ⟨v, w, hn, he⟩ := exists_ne_map_eq_of_card_lt (Sigma.fst ∘ f) (by simp [hc])
  rw [← top_adj, ← f.topEmbedding.map_adj_iff, comap_adj, top_adj] at hn
  exact absurd he hn

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
⊢ x ∈ t

Tactic:
by_contra hf
  have ht : (t : Set α) \ {x} = t := sdiff_eq_left.mpr <| Set.disjoint_singleton_right.mpr hf
  exact h t ⟨ht ▸ hc.1.sdiff_of_sup_edge, hc.2⟩

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 α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 ↦ (x, x_1))
          ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match x with
            | (y, z) => G.Adj y z})))

Tactic:
have hZ : #u * ε ≤ #{y ∈ u | G.Adj x y} := by
    refine le_trans ?_ hsu; gcongr; linarith

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 ↦ (x, x_1))
          ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match x with
            | (y, z) => G.Adj y z})))
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 α := 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}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#s) - 2 * ε * ↑(#s) ≤ ↑(#s - #(G.badVertices ε s t ∪ G.badVertices ε s u))

Tactic:
Nat.cast_sub (card_le_card i),

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}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#s) - 2 * ε * ↑(#s) ≤ ↑(#s) - ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u))
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * ((1 - (↑m)⁻¹) / ↑m) ≤ 1

Tactic:
mul_div_assoc',

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
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (1 - (↑m)⁻¹) / ↑m ≤ 1
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * ((↑m - 1) / ↑m) ≤ ↑m

Tactic:
mul_div_assoc',

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
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (↑m - 1) / ↑m ≤ ↑m
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:

Tactic:
_ = (#((univ ×ˢ univ).filter fun (x, y) ↦
          G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) : ℝ) := by
      rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
      · norm_cast
        rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
      · gcongr with xy _
        exact fun hxy ↦ regularityReduced_le hxy
    _ ≤ #(A ∪ B ∪ C) := by gcongr; exact unreduced_edges_subset
    _ ≤ #(A ∪ B) + #C := mod_cast (card_union_le _ _)
    _ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _
    _ < 4 * (ε / 8) * card α ^ 2 + _ + _ := by
      gcongr; exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε
    _ ≤ _ + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 := by
      gcongr
      · exact hP.card_biUnion_offDiag_le hε hP'
      · exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)
    _ = 2 * ε * (card α ^ 2 : ℕ) := by norm_cast; ring

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

Tactic:
obtain ⟨x₁, y₁, x₂, y₂, hx₁y₁, hx₁y₂, hx₂y₁, hxy, hx₁x₂⟩ :
      ∃ x₁ y₁ x₂ y₂, y₁ - x₁ ∈ A ∧ y₂ - x₁ ∈ A ∧ y₁ - x₂ ∈ A ∧ x₁ + y₂ = x₂ + y₁ ∧ x₁ ≠ x₂ := by
    simpa [IsCornerFree, isCorner_iff, B, -exists_and_left, -exists_and_right]
      using corners_theorem ε hε hG B this

Goal state after:
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₂
⊢ False
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b ↦ bif b then f₂ else f₁
this : ∑ b, (F b).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }

Tactic:
simpa only [Bool.forall_bool] using! char_dvd_card_solutions_of_fintype_sum_lt p this

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
⊢ #A + #A.subsetSum < #(insert a A).subsetSum

Tactic:
have disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum) := by
    have := nonneg_of_mem_subsetSum (fun y hy ↦ (hA y hy).le)
    simpa [disjoint_left, mem_insert, mem_vadd_finset] using
      ⟨fun x hx => (add_pos_of_pos_of_nonneg ha <| this _ hx).ne',
        fun x hx y hy ↦ (lt_add_of_lt_of_nonneg (hAa x hx) <| this _ hy).ne'⟩
  -- Both sets are subsets of `(insert a A).subsetSum`.
  have insert_subset : insert 0 A ⊆ (insert a A).subsetSum := by
    grw [insert_subset_iff, ← subset_insert]; exact ⟨zero_mem_subsetSum, subset_subsetSum⟩
  have vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum :=
    vadd_finset_subsetSum_subset_subsetSum_insert fun ha => (hAa a ha).false
  -- Count the sizes.
  calc #A + #A.subsetSum
    _ < #A + 1 + #A.subsetSum := by gcongr; exact Nat.lt_add_one _
    _ = #(insert 0 A) + #A.subsetSum := by rw [card_insert_of_notMem fun h => (hA 0 h).false]
    _ = #(insert 0 A) + #(a +ᵥ A.subsetSum) := by simp [vadd_finset_def, card_image_of_injOn]
    _ = #((insert 0 A) ∪ (a +ᵥ A.subsetSum)) := by rw [card_union_of_disjoint disjoint]
    _ ≤ #(insert a A).subsetSum := by grw [union_subset insert_subset vadd_subset]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hst : s = t
⊢ False

Tactic:
exact ht.2 <| hst ▸ hs.1

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: 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 ∈ 𝒜

Tactic:
exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ StrictMono fun s ↦ ∑ k ∈ ofColex s, n ^ k

Tactic:
intro s t hst

Goal state after:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
hst : s < t
⊢ (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) 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))
⊢ (↑n + 1) * ↑(numDerangements n) - (-1) ^ n =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x)) +
      (-1) ^ (n + 1) * ↑((n + 1 + 1).ascFactorial (n + 1 - (n + 1)))

Tactic:
hn,

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ (↑n + 1) * ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) - (-1) ^ n =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x)) +
      (-1) ^ (n + 1) * ↑((n + 1 + 1).ascFactorial (n + 1 - (n + 1)))
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
G : Digraph V
⊢ (Digraph.mk' fun v w ↦ decide (G.Adj v w)) = G

Tactic:
ext v w

Goal state after:
case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
G : Digraph V
v w : V
⊢ (Digraph.mk' fun v w ↦ decide (G.Adj v w)).Adj v w ↔ G.Adj v w
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
⊢ 1 < order P L

Tactic:
by
  obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
  cases nonempty_fintype { p : P // p ∈ l₂ }
  rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card,
    Fintype.two_lt_card_iff]
  simp_rw [Ne, Subtype.ext_iff]
  have h := mkPoint_ax (P := P) (L := L) fun h => h₂₁ ((congr_arg (p₂ ∈ ·) h).mpr h₂₂)
  exact
    ⟨⟨mkPoint _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩, ne_of_mem_of_not_mem h.1 h₂₁,
      ne_of_mem_of_not_mem h.1 h₃₁, ne_of_mem_of_not_mem h₂₃ h₃₃⟩

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

Goal state before:
pp: m : Multiset ℕ
⊢ ((Nat.multinomial m.toFinset fun k ↦ k * count k m) *
          ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        (map (fun j ↦ j !) m).prod *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    m.sum !

Tactic:
← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)

Goal state after:
m : Multiset ℕ
⊢ (∏ i ∈ m.toFinset, (i * count i m)!) *
      (((Nat.multinomial m.toFinset fun k ↦ k * count k m) *
            ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
          (map (fun j ↦ j !) m).prod *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
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 𝕝 α
⊢ 1 • f = f

Tactic:
by ext a b hab; simp [ite_smul, hab]

Goal state after:
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✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
⊢ (algebraMap 𝕜 𝕝) (c + d) • 1 = (algebraMap 𝕜 𝕝) c • 1 + (algebraMap 𝕜 𝕝) d • 1

Tactic:
by rw [map_add, add_smul]

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

Goal state before:
pp: case e'_2.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

Tactic:
simp only [toFinset_replicate]
    split_ifs with hm
    · rw [hm, factorial_zero, eq_comm]
      rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]
    · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
      simp only [Finset.prod_singleton, count_replicate_self]

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

Goal state before:
pp: case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (range (↑(p + q)).length).length

Tactic:
· rw [length_range, u, length_append]
    exact Nat.lt_add_right _ (firstReturn_lt_length h)

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ↑(p.take (p.firstReturn + 1) ⋯ + p.drop (p.firstReturn + 1) ⋯) = ↑p

Tactic:
apply take_append_drop

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

Goal state before:
pp: p : DyckWord
⊢ 0 < p ↔ p ≠ 0

Tactic:
rw [ne_comm, iff_comm, ne_iff_lt_iff_le]

Goal state after:
p : DyckWord
⊢ 0 ≤ p
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
hK : K ≤ 1
hS : S.Nonempty
hA : IsAtom K S A
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
⊢ #(A ∩ B) ≤ #A

Tactic:
grw [inter_subset_left]

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

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

Tactic:
hn,

Goal state after:
case succ
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1) * n ! + (n + 1).stirlingFirst 0 = (n + 1)!
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
by
  rw [mul_assoc]
  obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0
  · exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)
  exact
    (mul_le_mul_of_nonneg_left Behrend.roth_lower_bound hn).trans
      (rothNumberNat_le_ruzsaSzemerediNumberNat' _)

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x y : α'
f : α → α'
G : Graph α β
e : β
⊢ e ∈ E(G) ↔ ∃ x y, Relation.Map (G.IsLink e) f f x y

Tactic:
by
    refine ⟨fun h ↦ ?_, fun ⟨_, _, _, _, h, _, _⟩ ↦ h.edge_mem⟩
    obtain ⟨x, y, hxy⟩ := exists_isLink_of_mem_edgeSet h
    exact ⟨_, _, _, _, hxy, rfl, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case head'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m : M
a : Stream' M
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a

Tactic:
exact ⟨1, fun m hm => FP.cons a m hm⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ↾ M.E \ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D

Tactic:
isBasis_restrict_iff,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I X ∧ X ⊆ M.E \ D ↔ M.IsBasis I X ∧ Disjoint X D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
have mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l := by
      rintro ⟨l, c, hl⟩
      refine ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => ?_⟩
      rw [Line.horizontal_apply, ← hl, ← hl']

Goal state after:
case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ↾ M.E \ D).closure X = M.closure (X \ D) \ D

Tactic:
restrict_closure_eq',

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ (M.E \ D)) ∩ (M.E \ D) ∪ (M.E \ D) \ M.E = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ⋯.choose ∈ s

Tactic:
hs,

Goal state after:
case refine_1
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ⋯.choose ∈ {i | l.idxFun i = none}