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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsTrail → p.reverse.IsTrail

Tactic:
intro h
      convert! h.reverse _
      try rw [reverse_reverse]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : ∃ n, (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
⊢ False

Tactic:
obtain ⟨n, ⟨hn, hnl⟩⟩ := hv

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : (p.takeUntil w hw).getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n

Tactic:
exact (· _ this)

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

Goal state before:
pp: n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : ↑n ≤ ENat.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
by
  by_cases h : Infinite ι
  · exact not_cliqueFree_of_infinite V f
  · have : Fintype ι := fintypeOfNotInfinite h
    rw [ENat.card_eq_coe_fintype_card, Nat.cast_le] at hc
    exact not_cliqueFree_of_le_card V f hc

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ G.cliqueFinset n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t

Tactic:
eq_empty_iff_forall_notMem,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ (∀ (x : Finset α), x ∉ G.cliqueFinset n) ↔ ∀ (t : Finset α), ¬G.IsNClique n t
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ Gᶜ.cliqueNum = G.indepNum

Tactic:
by
  simp [indepNum, cliqueNum]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
⊢ Gᶜ.indepNum = G.cliqueNum

Tactic:
by
  simp [indepNum, cliqueNum]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(G.edgeDensity (G.badVertices ε s t) t) ≤ ↑(G.edgeDensity s t) - ε

Tactic:
rw [edgeDensity_def]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(↑(#(G.interedges (G.badVertices ε s t) t)) / (↑(#(G.badVertices ε s t)) * ↑(#t))) ≤ ↑(G.edgeDensity s t) - ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

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

Tactic:
pow_right_comm,

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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 3 / 4 * ε ≤
    |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
          (4 ^ #P.parts) ^ 2|
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ ↑(#A) ≤ ↑(#(A * B))

Tactic:
exact mod_cast card_le_card_mul_right hB

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / (4 ^ 2) ^ #P.parts * (9 / 4 ^ 2) * ε ^ 2

Tactic:
pow_right_comm,

Goal state after:
case h₂
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / (4 ^ #P.parts) ^ 2 * (9 / 4 ^ 2) * ε ^ 2
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s * #t ≤ Eₘ[s, t]

Tactic:
rw [← card_product]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(s ×ˢ t) ≤ Eₘ[s, t]
Module: Mathlib.Combinatorics.Additive.Energy

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

Tactic:
by
      rw [filter_eq_self.2, card_product, mul_pow]; aesop (add unsafe mul_mem_mul)

Goal state after:
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 σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
⊢ ∏ j, ↑(e a) j ^ d j = (∏ j, x₀ j ^ d ↑j) * a ^ d i

Tactic:
let e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl _

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
⊢ ∏ j, ↑(e a) j ^ d j = (∏ j, x₀ j ^ d ↑j) * a ^ d i
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: i n : ℕ
⊢ i ∈ n.bitIndices ↔ n.testBit i = true

Tactic:
induction n using Nat.binaryRec generalizing i with
  | zero => simp
  | bit b n ih => cases b <;> cases i <;> simp_all [Nat.testBit_add_one, Nat.mul_add_div]

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : w 0 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 0 • w → -w 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 : w 1 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 1 • w → -w 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 : w 2 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 2 • w → -w 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False

Tactic:
hw',

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 :
  ![w 0, w 1, w 2] 0 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 0 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 0 = 0 ∧ ![v 0, v 1, v 2] 0 = 0
h21 :
  ![w 0, w 1, w 2] 1 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 1 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 1 = 0 ∧ ![v 0, v 1, v 2] 1 = 0
h22 :
  ![w 0, w 1, w 2] 2 • ![v 0, v 1, v 2] = ![v 0, v 1, v 2] 2 • ![w 0, w 1, w 2] →
    -![w 0, w 1, w 2] 2 = 0 ∧ ![v 0, v 1, v 2] 2 = 0
⊢ False
Module: Mathlib.Combinatorics.Derangements.Basic

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

Tactic:
exact F_derangement _ x_fixed

Goal state after:
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)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
this :
  ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) + ↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) =
    ↑(#(A ∩ (c * d) •> A)) + ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ #(A ∩ ((c * d) •> A ∪ (a * b)⁻¹ •> A)) ≤ #A

Tactic:
exact card_le_card inter_subset_left

Goal state after:
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)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)

Tactic:
have h₃ : ((i : ℚ) + 1) * (i + 1).centralBinom = 2 * (2 * i + 1) * i.centralBinom :=
    mod_cast Nat.succ_mul_centralBinom_succ i

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
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i ∈ range d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i) = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons
s : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: tail✝) = count D (s :: tail✝)
nonneg : ∀ (i : ℕ), count D (take i (s :: tail✝)) ≤ count U (take i (s :: tail✝))
h : ↑{ toList := s :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := nonneg } ≠ []
f : ¬s = U
⊢ False

Tactic:
simpa [s.dichotomy.resolve_left f] using nonneg 1

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

Goal state before:
pp: m : Multiset ℕ
⊢ m.bell = m.sum ! / ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]

Goal state after:
m : Multiset ℕ
⊢ m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !

m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0
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✝¹ : Zero 𝕜
inst✝ : LE α
a b : α
f g : IncidenceAlgebra 𝕜 α
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

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✝¹ : AddGroup 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (⇑f - ⇑g) a b = 0

Tactic:
Pi.sub_apply,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ f a b - g a b = 0
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∀ (x : (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts }),
    n.choose ↑x.fst * ((↑x.snd).parts.erase (↑x.fst + 1)).bell =
      n.choose (↑(n.sigmaPartitionWithPartEquiv x).snd - 1) *
        ((n.sigmaPartitionWithPartEquiv x).fst.parts.erase ↑(n.sigmaPartitionWithPartEquiv x).snd).bell

Tactic:
simp [sigmaPartitionWithPartEquiv]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ (mu 𝕜).prod (mu 𝕜) * zeta 𝕜 = 1

Tactic:
rw [← zeta_prod_zeta, prod_mul_prod', mu_mul_zeta, mu_mul_zeta, one_prod_one]

Goal state after:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: n : ℕ
⊢ Fintype.card { p // p.semilength = n } = catalan n

Tactic:
rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]

Goal state after:
n : ℕ
⊢ Fintype.card ↥(treesOfNumNodesEq n) = (treesOfNumNodesEq n).card
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 ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0

Tactic:
suffices ∃ i ∈ s, (coeff (g i)) ((1 : R⟦X⟧) + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) = 0 by
    obtain ⟨i, hi, hi'⟩ := this
    apply prod_eq_zero hi hi'
  contrapose! hg' with hprod
  rw [Set.mem_range]
  have hgne0 (i : ℕ) : g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i := by
    refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩
    · contrapose hs0 with rfl
      exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h)
    · exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _
  refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩
  · simpa using hgne0
  · suffices ∀ i, g i ≠ 0 → i ≠ 0 by simpa [Nat.pos_iff_ne_zero]
    exact fun i h ↦ ((hgne0 i).mp h).1
  · obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg
    refine Eq.trans ?_ h1
    suffices ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x by simpa [Finsupp.sum]
    apply sum_subset_zero_on_sdiff h2 (by simp)
    exact fun x hx ↦ Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x
  · ext x
    simpa [toFinsuppAntidiag] using Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x

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

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

Tactic:
ext1 i
    rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range]
    congrm $(by simp) + ?_
    trans ∑ k ∈ range (m - 1), (if k + 1 < m then (1 : R) else 0) • X ^ ((i + 1) * (k + 1))
    · refine sum_congr rfl fun b hn ↦ ?_
      rw [add_comm 1 b]
      have : b + 1 < m := by grind
      simp [this]
    · exact (tsum_eq_sum (fun b hb ↦ smul_eq_zero_of_left (by simpa using hb) _)).symm

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

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

Tactic:
← two_mul_smallSchroder_succ (by lia)

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (2 * (n + 1 + 1).smallSchroder) +
      ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
    6 * (n + 2).smallSchroder + 4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (map f G).Inc e x ↔ ∃ v, G.Inc e v ∧ x = f v

Tactic:
simp only [Inc, map_isLink, map_apply]

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (∃ y a b, G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ v, (∃ y, G.IsLink e v y) ∧ x = f v
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
⊢ Sum.inr e = Sum.inr f

Tactic:
obtain ⟨a, b, hab⟩ := exists_pair_ne α

Goal state after:
case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ Sum.inr e = Sum.inr f
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint (M.E ∩ (X \ D)) D

Tactic:
← inter_sdiff_assoc

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * 1 ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
mul_one

Goal state after:
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head ∈ FP (Stream'.drop (s.min' hs) a)
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D

Tactic:
obtain ⟨C, D, rfl⟩ := h
  exact ⟨C ∩ M.E, (D ∩ M.E) \ C, inter_subset_right, sdiff_subset.trans inter_subset_right,
    disjoint_sdiff_right.mono_left inter_subset_left,
    by simp [delete_eq_delete_iff, inter_assoc, inter_sdiff_assoc]⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
⊢ m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)

Tactic:
apply degree_reduce_lt (hb i) hf

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
⊢ m.degree f ≠ 0
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
x✝ : ℕ
h_len : p.length = x✝
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
induction h_len : p.length generalizing a b S ha_not_in_S hb_in_S with

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case h
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
⊢ (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u, Path.nil⟩ = ⟨φ.obj u, Path.nil⟩

Tactic:
simp only [Prefunctor.mapPath_nil]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ {s ∈ 𝒜 | s.erase a ∈ 𝒜} ∨ s ∈ {s ∈ image (fun s ↦ s.erase a) 𝒜 | s ∉ 𝒜} ↔
    s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜

Tactic:
mem_filter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∈ image (fun s ↦ s.erase a) 𝒜 ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ s ⊼ tᶜˢ ↔ a✝ ∈ s \\ t

Tactic:
simp [sdiff_eq]

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ {a ∈ s | compress u v a ∈ s} ∨ a ∈ {a ∈ image (compress u v) s | a ∉ s} ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
mem_filter,

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ s ∧ compress u v a ∈ s ∨ a ∈ image (compress u v) s ∧ a ∉ s ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
exists₂_congr

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ a b, ?m.29 a b) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ ?m.29 a_1 b

α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ α → α → Prop