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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
⊢ G.IsClique (Set.range ⇑f)

Tactic:
by
  intro _ ⟨_, h⟩ _ ⟨_, h'⟩ nh
  rw [← h, ← Copy.topEmbedding_apply, ← h', ← Copy.topEmbedding_apply] at nh ⊢
  rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh

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
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ p.tail.getVert (n - 1) = p.tail.getVert (m - 1)

Tactic:
simp_all

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

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

Tactic:
simp_all

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:
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: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → ∀ ⦃t : Finset α⦄, ↑t ⊆ s → G.IsClique ↑t → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}

Tactic:
rintro h t hst ht a b hab rfl

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
hst : ↑{a, b} ⊆ s
ht : G.IsClique ↑{a, b}
⊢ False
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 : α
hx :
  x ∈ s ∧ x ∉ s ∨
    x ∈ s ∧
      (↑(G.edgeDensity s t) - ε) * ↑(#t) ≤ ↑(#({y ∈ t | G.Adj x y})) ∧
        (↑(G.edgeDensity s u) - ε) * ↑(#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})))

Tactic:
simp only [false_or, and_not_self, mul_comm (_ - _)] at hx

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 : α
hx :
  x ∈ s ∧
    ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y})) ∧
      ↑(#u) * (↑(G.edgeDensity s 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.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
⊢ (a, b, c) ∈ triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b

Tactic:
simp only [triangleIndices, Prod.ext_iff, mem_map, Prod.exists, eq_comm]
  refine ⟨?_, fun h ↦ ⟨_, _, h.1, rfl, rfl, h.2⟩⟩
  rintro ⟨_, _, h₁, rfl, rfl, h₂⟩
  exact ⟨h₁, h₂⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#A) * σₘ[A, B] = ↑(#(A * B))

Tactic:
by
  rw [mul_comm, mulConst_mul_card]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}) ^ 2 ≤ #u * Eₘ[s, t]

Tactic:
by
  calc
    _ = (∑ c ∈ u, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 := by
        rw [← sum_card_fiberwise_eq_card_filter]
    _ ≤ #u * ∑ c ∈ u, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c} ^ 2 := by
        simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _
    _ ≤ #u * ∑ c ∈ s * t, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c} ^ 2 := by
        refine mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _
        aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)
    _ = #u * Eₘ[s, t] := by rw [mulEnergy_eq_sum_sq']

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit
b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
⊢ List.Pairwise (fun a b ↦ a < b) n.bitIndices

Tactic:
exact List.Pairwise.imp (by simp) hs.pairwise

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
x y : ℕ
hx : x ∈ L
x✝ : y ∈ L
⊢ x - (a + 1) < y - (a + 1) ↔ x < y

Tactic:
rw [tsub_lt_tsub_iff_right (haL _ hx)]

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g ↑t ⋯ x
s : Set α
hs : s.Finite
t : Finset α
ht : hs.toFinset ⊆ t
ht' : ∀ x ∈ hs.toFinset, χ x = g ↑t ⋯ x
⊢ ∃ (ht : (↑t).Finite), s ⊆ ↑t ∧ ∀ x ∈ s, χ x = g (↑t) ht x

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : (s : Set α) → s.Finite → (a : ↑s) → β ↑a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g ↑t ⋯ (inclusion hst x)
s : Set α
hs : s.Finite
t : Finset α
ht✝ : hs.toFinset ⊆ t
hst : ∀ (x : ↥hs.toFinset), χ ↑x = g ↑t ⋯ (inclusion ht✝ x)
ht : s ⊆ ↑t
⊢ ∃ (ht : (↑t).Finite) (hst : s ⊆ ↑t), ∀ (x : ↑s), χ ↑x = g (↑t) ht (inclusion hst x)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∉ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
exact ⟨b, hbu, hbs, hab⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
⊢ H ∈ Set.range Projectivization.submodule

Tactic:
rcases finrank_eq_one_iff'.1 h with ⟨v : H, hv₀, hv : ∀ w : H, _⟩

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ H ∈ Set.range Projectivization.submodule
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ (mk K ↑v ⋯).submodule = H

Tactic:
rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K ↥((Equiv.refl (Submodule K V)) H) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ c, c • v = w
⊢ (Set.range fun x ↦ x • ↑v) = ↑H
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ ((mk F v hv).cross (mk F w hw)).orthogonal (mk F v hv)

Tactic:
rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ = (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
le_antisymm_iff,

Goal state after:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h :
  (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝ ≤ (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ ∧
    (fun s ↦ ∑ i ∈ s, n ^ i) a₂✝ ≤ (fun s ↦ ∑ i ∈ s, n ^ i) a₁✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
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
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset

Tactic:
s,

Goal state after:
case h
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
⊢ ∀ (p : P × L), p ∈ {i | i.1 ∈ i.2}.toFinset ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
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
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Tactic:
s,

Goal state after:
case h
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
⊢ ∀ (p : P × L), p ∈ {i | i.1 ∈ i.2}.toFinset ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
l₂ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)
h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom
h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom
⊢ (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1) * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑i.centralBinom * ↑(n - i + 1).centralBinom * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)

Tactic:
h₂,

Goal state after:
n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
l₂ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)
h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom
h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom
⊢ (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1) * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑i.centralBinom * ((↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)) * (2 * ↑i - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1) by
    have h := Nat.succ_dvd_centralBinom n
    exact mod_cast this

Goal state after:
n : ℕ
⊢ ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
H : Subgroup G
inst✝ : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
h₁ z₁ h₂ : G
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
h : h₁ * z₁ = h₂ * z₁
hz₂ : z₁ ∈ Z
⊢ (h₁, z₁) = (h₂, z₁)

Tactic:
simp_all

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

Goal state before:
pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b

Tactic:
rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le 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✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ f * g * h = f * (g * h)

Tactic:
ext a b
    simp only [mul_apply, sum_mul, mul_sum, sum_sigma']
    apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
      aesop (add simp mul_assoc) (add unsafe le_trans)

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

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
· rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
      simp [count_replicate]

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

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
z : G
hz : z ∈ {z ∈ S | ↑(r z) ≤ (K - 1) * ↑(#A)}
⊢ ↑(r z) ≤ (K - 1) * ↑(#A)

Tactic:
simp_all

Goal state after:
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
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hg' : g ∉ Set.range toFinsuppAntidiag
i : ℕ
hi : i ∈ s
hi' : (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0
⊢ ∏ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0

Tactic:
apply prod_eq_zero hi hi'

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

Goal state before:
pp: p : DyckWord
⊢ (p.nest.take (p.nest.firstReturn + 1) ⋯).denest ⋯ = p

Tactic:
firstReturn_nest

Goal state after:
p : DyckWord
⊢ (p.nest.take ((↑p).length + 1 + 1) ⋯).denest ⋯ = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.drop (p.nest.firstReturn + 1) ⋯ = 0

Tactic:
firstReturn_nest

Goal state after:
p : DyckWord
⊢ p.nest.drop ((↑p).length + 1 + 1) ⋯ = 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
⊢ Filter.Tendsto (fun s ↦ ∏ b ∈ s, (1 + ∑' (j : ℕ), f (b + 1) (j + 1) • X ^ ((b + 1) * (j + 1))))
    (SummationFilter.unconditional ℕ).filter (nhds (genFun f))

Tactic:
WithPiTopology.tendsto_iff_coeff_tendsto

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
⊢ ∀ (d : ℕ),
    Filter.Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 + ∑' (j : ℕ), f (b + 1) (j + 1) • X ^ ((b + 1) * (j + 1)))))
      (SummationFilter.unconditional ℕ).filter (nhds ((coeff d) (genFun f)))
Module: Mathlib.Combinatorics.Enumerative.Stirling

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

Tactic:
by rw [stirlingSecond]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
d' c : α
hc : c ∈ s
h₂ : d' + c = d + a
hb : a ∈ s
h₁ : d' + 2 * a = d + 2 * a
this : a + c = a + a
⊢ d' = d ∨ d + a = d' + a ∨ d + 2 * a = d' + 2 * c

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G < H
⊢ V(G) ⊂ V(H) ∨ E(G) ⊂ E(H)

Tactic:
by
  rw [lt_iff_le_and_ne] at hGH
  simp only [ssubset_iff_subset_ne, hGH.1.vertexSet_mono, ne_eq, true_and, hGH.1.edgeSet_mono]
  by_contra! heq
  exact hGH.2 <| hGH.1.compatible.ext heq.1 heq.2

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

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

Tactic:
exact fun h ↦ by simpa [he] using h.left_mem

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 : β
x y : α
h : G.IsLink e x y
⊢ f x ∈ f '' V(G)

Tactic:
exact Set.mem_image_of_mem _ h.left_mem

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
by
  cases h : l.idxFun ie.1 <;> simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ S.Nonempty

pp: case refine_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S

pp: case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S

Tactic:
· apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
    · intro n U hU
      filter_upwards [hU]
      rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
      exact FP.tail _
    · intro n
      exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
    · exact (ultrafilter_isClosed_basic _).isCompact
    · intro n
      apply ultrafilter_isClosed_basic

Goal state after:
case refine_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S

case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Finite α
κ : Type v
inst✝ : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift.{u, v} κ), ∃ l, IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift.{u, v} κ
hc : ∀ (x : α), (ULift.up ∘ C) (↑l x) = c
x : α
⊢ C (↑l x) = c.down

Tactic:
← hc x,

Goal state after:
α : Type u
inst✝¹ : Finite α
κ : Type v
inst✝ : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift.{u, v} κ), ∃ l, IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift.{u, v} κ
hc : ∀ (x : α), (ULift.up ∘ C) (↑l x) = c
x : α
⊢ C (↑l x) = ((ULift.up ∘ C) (↑l x)).down
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ Sigma.mk j ⁻¹' {⟨i, e⟩} ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})

Tactic:
obtain (rfl | hne) := eq_or_ne i j

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
⊢ (M i).IsBase (Sigma.mk i ⁻¹' B₁ \ Sigma.mk i ⁻¹' {⟨i, e⟩} ∪ Sigma.mk i ⁻¹' {⟨i, f⟩})

case inr
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ Sigma.mk j ⁻¹' {⟨i, e⟩} ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsSStronglyConnected V
⊢ IsStronglyConnected V

Tactic:
intro i j; obtain ⟨p, _⟩ := h i j; exact ⟨p⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
⊢ p'.length = n

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h₁ : p.vertices.getLast ⋯ = b
h₂ : p.vertices.getLast ⋯ ∈ p.vertices
⊢ b ∈ p.vertices

Tactic:
simpa [h₁] using h₂

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

Tactic:
le_antisymm_iff,

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ schnirelmannDensity A ≤ 1 ∧ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} ↔ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : A = B
⊢ ∀ n > 0, n ∈ A ↔ n ∈ B

Tactic:
simp_all

Goal state after: