mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ + y₂ - (x₂ + x₁) = y₁ - x₁ + (y₁ - x₁)

Tactic:
add_comm,

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₂
⊢ y₂ + y₁ - (x₂ + x₁) = y₁ - x₁ + (y₁ - x₁)
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₂

Tactic:
add_comm,

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₂
⊢ x₁ + y₂ = y₁ + x₂
Module: Mathlib.Combinatorics.Additive.Randomisation

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) = 𝔼 i, ∏ a, ((d a * a i + (starRingEnd ℂ) (d a * a i)) / 2 + ↑(c a))

Tactic:
add_comm,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) = 𝔼 i, ∏ x, (↑(c x) + (d x * x i + (starRingEnd ℂ) (d x * x i)) / 2)
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 ^ (k + 1) * n).bitIndices = map (fun x ↦ x + (k + 1)) n.bitIndices

Tactic:
add_comm,

Goal state after:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 ^ (1 + k) * n).bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
hrw : ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i)
⊢ map (fun x ↦ x + a) (1 + 2 * (map (HPow.hPow 2) L₀).sum).bitIndices = a :: map (fun x ↦ x + a + 1) L₀

Tactic:
add_comm,

Goal state after:
case cons
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
hrw : ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i)
⊢ map (fun x ↦ x + a) (2 * (map (HPow.hPow 2) L₀).sum + 1).bitIndices = a :: map (fun x ↦ x + a + 1) L₀
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a

Tactic:
refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
    fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩ <;> rintro rfl

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
hb : b ∈ s
h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ ¬s = {b}
⊢ False

case refine_2
α : Type u_1
inst✝ : PartialOrder α
a : α
h : ∀ b ∈ {a}, b < a
⊢ False
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (∃ x, x • v = w) → (crossProduct v) w = 0

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case neg.mp
F : Type u_2
inst✝ : Field F
v : Fin 3 → F
hv : ¬v = 0
a : F
⊢ (crossProduct v) (a • v) = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
a : α
ha : a ∈ s
hst : toColex s ≤ toColex s
hcard : #s ≤ #s
ht : s.Nonempty
m : α := s.min' ht
⊢ toColex (s.erase a) ≤ toColex (s.erase m)

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
· exact (erase_le_erase ha <| min'_mem _ _).2 <| min'_le _ _ <| ha

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ toColex (s.erase a) ≤ toColex (t.erase m)
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v

Tactic:
by
  induction v with | h v hv =>
  rw [cross_mk_of_cross_eq_zero]
  rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ a_1 ∈ fixedPoints ⇑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ⇑x

Tactic:
Set.mem_compl_iff,

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ fiber none = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]
  intro f hyp
  rw [RemoveNone.mem_fiber] at hyp
  rcases hyp with ⟨F, F_derangement, F_none, _⟩
  exact F_derangement none F_none

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

Goal state before:
pp: case mp.none
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : a = x
Fx : F (some x) = none
⊢ x ∈ {a}

Tactic:
eq_comm

Goal state after:
case mp.none
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : x = a
Fx : F (some x) = none
⊢ x ∈ {a}
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
⊢ ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1 = ∑ c, ∑ a ∈ {p | p ∈ c}.toFinset, pointCount P (a, c).2

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

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
⊢ ∑ c, ∑ a ∈ {p | p ∈ c}.toFinset, pointCount P (a, c).2 = ∑ c, ∑ a ∈ {l | c ∈ l}.toFinset, lineCount L (c, a).1

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
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
⊢ Bijective ⇑Digraph.mk'

Tactic:
by
    classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp

Goal state after:
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
p : P
⊢ 2 < lineCount L p

Tactic:
simpa only [lineCount_eq L p, Nat.succ_lt_succ_iff] using one_lt_order P L

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑A⁻¹ * ↑A = ↑A * ↑A⁻¹

Tactic:
eq_comm

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑A * ↑A⁻¹ = ↑A⁻¹ * ↑A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ {l₁ l₂ : ℙ K (Fin 3 → K)} → l₁ ≠ l₂ → ℙ K (Fin 3 → K)

Tactic:
intro v

Goal state after:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
v : ℙ K (Fin 3 → K)
⊢ {l₂ : ℙ K (Fin 3 → K)} → v ≠ l₂ → ℙ K (Fin 3 → K)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ {p₁ p₂ : ℙ K (Fin 3 → K)} → p₁ ≠ p₂ → ℙ K (Fin 3 → K)

Tactic:
intro v

Goal state after:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
v : ℙ K (Fin 3 → K)
⊢ {p₂ : ℙ K (Fin 3 → K)} → v ≠ p₂ → ℙ K (Fin 3 → K)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ z ∈ A * A

Tactic:
have hl : l = A := by
    rw [inter_eq_left, ← this, subset_smul_finset_iff]
    simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]
    refine smul_finset_subset_mul ?_
    simp [mul_mem_mul, ha, hb, hc]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ z ∈ A * A
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
this : ?m.115
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
by_cases hm : 0 ∈ m.toFinset

Goal state after:
case pos
m : Multiset ℕ
this : ?m.115
hm : 0 ∈ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

case neg
m : Multiset ℕ
this : ?m.115
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.take i (↑p).dropLast.tail) ≤ count U (List.take i (↑p).dropLast.tail)

Tactic:
← drop_one,

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.take i (List.drop 1 (↑p).dropLast)) ≤ count U (List.take i (List.drop 1 (↑p).dropLast))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m n : ℕ
⊢ (multinomial (replicate m n).toFinset fun k ↦ k * count k (replicate m n)) *
      ∏ k ∈ (replicate m n).toFinset.erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
rw [toFinset_replicate]

Goal state after:
m n : ℕ
⊢ (multinomial (if m = 0 then ∅ else {n}) fun k ↦ k * count k (replicate m n)) *
      ∏ k ∈ (if m = 0 then ∅ else {n}).erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 1 = ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))!

Tactic:
eq_comm

Goal state after:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))! = 1
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n = (m * n)! / (n ! ^ m * m !)

Tactic:
eq_comm

Goal state after:
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! / (n ! ^ m * m !) = m.uniformBell n
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Tactic:
by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).2]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case pos.refine_2
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
i : ℕ
⊢ (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0

Tactic:
rw [map_smul, coeff_X_pow]
      apply smul_eq_zero_of_right
      suffices g x ≠ x * (i + 1) by simp [this]
      contrapose hprod
      simp [hprod]

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

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

Tactic:
← toList_ne_nil,

Goal state after:
p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
⊢ ↑(p.take (p.firstReturn + 1) ⋯) ≠ []
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✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
obtain hxy | hxy := hxy

Goal state after:
case inl
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1
⊢ f x.1 y.1 * g x.2 y.2 = 0

case inr
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ IncidenceAlgebra.prod 1 1 = 1

Tactic:
by
  ext x y; simp [Prod.ext_iff, ← ite_and, and_comm]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ HasProd (fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)) (PowerSeries.mk fun n ↦ ↑(#(countRestricted n m)))

Tactic:
convert! hasProd_genFun (fun i c ↦ if c < m then (1 : R) else 0) using 1

Goal state after:
case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)) = fun i ↦
    1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

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 ↦ ↑(#(countRestricted n m))) = genFun fun i c ↦ if c < m then 1 else 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
⊢ expansion K S ∅ = 0

Tactic:
simp [expansion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
G H : SimpleGraph α
⊢ ℕ

Tactic:
classical
  exact Nat.findGreatest (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
    #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) ((card α).choose 3)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsLink G.IsLink E(H)

Tactic:
rintro e he

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.IsLink e = G.IsLink e
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.Inc G.Inc E(H)

Tactic:
rintro e he

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.Inc e = G.Inc e
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsLoopAt G.IsLoopAt E(H)

Tactic:
rintro e he

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.IsLoopAt e = G.IsLoopAt e
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsNonloopAt G.IsNonloopAt E(H)

Tactic:
rintro e he

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
⊢ H.IsNonloopAt e = G.IsNonloopAt e
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

Tactic:
simpa [neg_mul, abs_mul, abs_of_nonneg this] using ruzsaSzemerediNumberNat_lower_bound n

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ EqOn H.IsNonloopAt G.IsNonloopAt E(H)

Tactic:
by
  rintro e he
  ext x
  exact hHG.isNonloopAt_congr he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x z : α
e : β
G : Graph α β
hz : G.Inc e z
hxz : x ≠ z
hy : G.Inc e z
hxy : x ≠ z
hyz : z ≠ z
hx' : G.IsLink e x z
⊢ False

Tactic:
exact hyz rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
h : G.IsLoopAt e x
y z : α
hyz : x ≠ x
hy : G.IsLink e y z
⊢ False

Tactic:
exact hyz rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)

Tactic:
by
  refine (Compatible.of_le_le (G := G) (restrict_le.trans (by simp)) (by simp)).ext (by simp) ?_
  simp only [edgeSet_restrict]
  rw [← inter_assoc, inter_comm _ F₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e✝ f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
he : e ∈ edgeSet
⊢ ∀ ⦃a b : α⦄, G.IsLink e a b → G.IsLink e b a

Tactic:
exact (G.isLink_symm <| hedgeSet ▸ he).symm

Goal state after: