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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s (φ b) else G.Adj (φ a) (if b = x then s else φ b)) ↔
    (completeGraph (Fin n)).Adj a b

Tactic:
apply_ite (G.Adj _ ·)

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s (φ b) else if b = x then G.Adj (φ a) s else G.Adj (φ a) (φ b)) ↔
    (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
⊢ (cons h✝ p✝).bypass.support <+ (cons h✝ p✝).support

Tactic:
dsimp! only

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.support <+ p✝.support
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).support <+ u✝ :: p✝.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
⊢ (cons h✝ p✝).bypass.darts <+ (cons h✝ p✝).darts

Tactic:
dsimp! only

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
⊢ (if hs : u✝ ∈ p✝.bypass.support then p✝.bypass.dropUntil u✝ hs else cons h✝ p✝.bypass).darts <+
    { fst := u✝, snd := v✝, adj := h✝ } :: p✝.darts
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
n : ℕ
ε : ℝ
A : Finset (G × G)
⊢ Injective fun x ↦
    match x with
    | (a, b) => (a, b, a + b)

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨⟩

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
A✝ : Finset (G × G)
a b c : G
n : ℕ
ε : ℝ
A : Finset (G × G)
x₁ x₂ : G
⊢ (x₁, x₂) = (x₁, x₂)
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
n : ℕ
ε : ℝ
A : Finset (G × G)
⊢ Injective fun x ↦
    match x with
    | (a, b) => (a, b, a + b)

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨⟩; rfl

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 : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#(triangleIndices A))
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 ≤ 1 * ↑(Fintype.card G) ^ 2

Tactic:
card_triangleIndices

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
h₁ : triangleRemovalBound (ε / 9) * ↑(Fintype.card (G ⊕ G ⊕ G)) ^ 3 ≤ ↑(#A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 ≤ 1 * ↑(Fintype.card G) ^ 2
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Goal state after:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] ≤ ↑(#B)

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ σₘ[A, B] ≤ ↑(#B)
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Goal state after:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] ≤ ↑(#B)

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ δₘ[A, B] ≤ ↑(#B)
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

Tactic:
exact mod_cast card_div_le

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A] ≤ σₘ[A] ^ 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Goal state after:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ δₘ[∅] ≤ σₘ[∅] ^ 2

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] ≤ σₘ[A] ^ 2
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
⊢ σₘ[A] ≤ δₘ[A] ^ 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Goal state after:
case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
⊢ σₘ[∅] ≤ δₘ[∅] ^ 2

case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] ≤ δₘ[A] ^ 2
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∈ S
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = 1

pp: case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∉ S
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = 0

Tactic:
· apply Finset.prod_eq_one
      intro i hi
      rw [hS] at hx
      rw [hx i hi, zero_pow hq.ne', sub_zero]

Goal state after:
case neg
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : x ∉ S
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = 0
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case h₁
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₁ s a).totalDegree ≤ p - 1

Tactic:
apply totalDegree_finsetSum_le

Goal state after:
case h₁
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ ∀ i ∈ univ, (X i ^ (p - 1)).totalDegree ≤ p - 1
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ (f₂ s a).totalDegree ≤ p - 1

Tactic:
apply totalDegree_finsetSum_le

Goal state after:
case h₂
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ ∀ i ∈ univ, (a ↑i • X i ^ (p - 1)).totalDegree ≤ p - 1
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)
⊢ (2 ^ a + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x ↦ x + a + 1) L₀

Tactic:
nth_rw 1 [← mul_one (a := 2 ^ a)]

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)
⊢ (2 ^ a * 1 + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x ↦ x + a + 1) L₀
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
B : Finset (Finset α)
i : Finset α
hi : i ∈ B
⊢ ∃ t, i ⊆ t ∧ ∀ x ∈ i, g (B.biUnion id) x = g t x

Tactic:
exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩

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
v : ℙ K V
| v.submodule

Tactic:
← v.mk_rep

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| (mk K v.rep ⋯).submodule
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
v : ℙ K V
⊢ FiniteDimensional K ↥v.submodule

Tactic:
← v.mk_rep

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K ↥(mk K v.rep ⋯).submodule
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
t₁ t₂ : Finset α
ht₁ : #s = #t₁ ∧ toColex t₁ ≤ toColex s
ht₂ : toColex t₂ < toColex t₁ ∧ #t₂ = #s
⊢ toColex t₂ ≤ toColex s

Tactic:
exact ht₂.1.le.trans ht₁.2

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

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

Tactic:
rw [cross_mk, dif_neg h]

Goal state after:
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))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) =
    (-1) ^ x * ↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x))

Tactic:
add_tsub_cancel_of_le h_le,

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((n + 1) * (x + 1).ascFactorial (n - x))
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
⊢ ↑(#(b •> A ∩ a⁻¹ •> A)) ≤ ↑(#(A ∩ (a * b)⁻¹ •> A))

Tactic:
← card_smul_finset b⁻¹

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
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
⊢ ↑(#(b⁻¹ •> (b •> A ∩ a⁻¹ •> A))) ≤ ↑(#(A ∩ (a * b)⁻¹ •> A))
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)

Tactic:
simp only [gosperCatalan, tsub_self, Nat.centralBinom_zero, Nat.cast_one, mul_one, Nat.cast_add,
    Nat.sub_zero, one_mul, Nat.cast_zero, mul_zero, zero_sub, neg_add_rev]
  field

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 _]
  · rw [← mul_assoc]
    exact bell_mul_eq m
  · rw [← bell_mul_eq, mul_assoc]
    apply Nat.dvd_mul_left
  · rw [← Nat.pos_iff_ne_zero]
    exact Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity)

Goal state after:
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
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take 1 ↑p) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take 1 ↑p) + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
l1,

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
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D [(↑p).head h] + count D (List.drop 1 (List.take j ↑p)) <
    count U [(↑p).head h] + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ 2 * p.semilength = (↑p).length

Tactic:
by
  nth_rw 1 [two_mul, semilength, p.count_U_eq_count_D, semilength]
  convert! (p.toList.length_eq_countP_add_countP (· == D)).symm
  rw [count]; congr!; rename_i s; cases s <;> tauto

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

Goal state before:
pp: n : ℕ
⊢ uniformBell 0 n = 1

Tactic:
by
  simp [uniformBell_eq]

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

Goal state before:
pp: m : ℕ
⊢ m.uniformBell 0 = 1

Tactic:
by
  simp [uniformBell_eq]

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

Goal state before:
pp: case pos
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 : ℕ
hprod : (coeff (g x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) ≠ 0
hx : x ∈ s
⊢ x ∣ g x

Tactic:
contrapose hprod

Goal state after:
case pos
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
⊢ (coeff (g x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case pos.refine_1
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
⊢ g x ≠ 0

Tactic:
contrapose hprod

Goal state after:
case pos.refine_1
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
hx0 : x ≠ 0
hprod : g x = 0
⊢ x ∣ g x
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 : ℕ
⊢ g x ≠ x * (i + 1)

Tactic:
contrapose hprod

Goal state after:
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
hx0 : x ≠ 0
i : ℕ
hprod : g x = x * (i + 1)
⊢ x ∣ g x
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (p + q).insidePart = p.insidePart

Tactic:
simp_rw [insidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
    DyckWord.ext_iff, take]
  congr 3
  exact take_append_of_le_length (firstReturn_lt_length h)

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, ∑ z ≥ y, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z

Tactic:
sum_sigma' (Ici x) fun y ↦ Ici y

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ x_1 ∈ (Ici x).sigma fun y ↦ Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ IsTopologicallyNilpotent X

Tactic:
rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto]

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) (X ^ i)) atTop (𝓝 ((coeff d) 0))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasProd (fun n ↦ 1 - X ^ (n + 1)) (pentagonalSeries R)

Tactic:
rw [HasProd, tendsto_iff_coeff_tendsto]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ ∀ (d : ℕ),
    Tendsto (fun i ↦ (coeff d) (∏ b ∈ i, (1 - X ^ (b + 1)))) (SummationFilter.unconditional ℕ).filter
      (𝓝 ((coeff d) (pentagonalSeries R)))
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
⊢ E(H) ⊆ E(G)

Tactic:
intro e he
  obtain ⟨x, y, h'⟩ := exists_isLink_of_mem_edgeSet he
  exact (h'.mono h).edge_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 : Graph α β
f : α → α'
f' : α' → α''
⊢ map f' (map f G) = map (f' ∘ f) G

Tactic:
ext a b c <;> simp [map_apply]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case htn
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)}
n : ℕ
⊢ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}.Nonempty

Tactic:
exact ⟨pure _, mem_pure.mpr <| FP.head _⟩

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
d : σ
⊢ (m.degree f) d = (m.degree f - m.degree b + m.degree b) d

Tactic:
rw [tsub_add_cancel_of_le hbf]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}

Tactic:
exact h.of_contract

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

Goal state before:
pp: case h.right.left
σ : 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
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ (i_1 : ι),
    m.toSyn
        (m.degree
          (b i_1 *
            (g' + Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) i_1)) ≤
      m.toSyn (m.degree f)

pp: case h.right.right
σ : 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
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
· rintro j
      simp only [Finsupp.coe_add, Pi.add_apply]
      rw [mul_add]
      apply le_trans degree_add_le
      simp only [sup_le_iff]
      constructor
      · exact le_trans (H'.2.1 _) (le_of_lt deg_reduce)
      · classical
        rw [Finsupp.single_apply]
        split_ifs with hc
        · subst j
          grw [degree_mul_le, map_add, degree_monomial_le, ← map_add, add_tsub_cancel_of_le hf]
        · simp only [mul_zero, degree_zero, map_zero]
          exact bot_le

Goal state after:
case h.right.right
σ : 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
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c