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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle

Tactic:
refine ⟨by grind [isPath_iff_isSubwalk_imp_nil, IsCycle.not_nil], fun h ↦ ?_⟩

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
⊢ p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
h : G.Adj u v
⊢ (Walk.cons h Walk.nil).IsPath

Tactic:
by simp [h.ne]

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) ≤ (#univ).choose n

Tactic:
← card_powersetCard

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ #(powersetCard n univ)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv'✝ : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv'✝ w).IsCircuit
hvv' : s(v, v') ∈ w.bypass.edges
⊢ False

Tactic:
simp only [isCircuit_def, isTrail_cons, ne_eq, reduceCtorEq, not_false_eq_true,
        and_true] at hw
      exact hw.2 <| edges_bypass_subset_edges _ hvv'

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
⊢ ↑(G.edgeDensity Y Z) ≤ 1

Tactic:
by exact mod_cast G.edgeDensity_le_one _ _

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 ≤ ↑(#((graph (triangleIndices A)).cliqueFinset 3))
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 ≤ 1 * ↑(Fintype.card G) ^ 2

Tactic:
rw [card_triangles, card_triangleIndices] at h₁

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.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
⊢ Prod.map Nat.cast Nat.cast '' ↑A ⊆ Set.Iio ↑n ×ˢ Set.Iio ↑n

Tactic:
refine Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
hA : IsCornerFree (Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A)
this✝ : ↑A = Prod.map Fin.val Fin.val '' Prod.map Nat.cast Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ × ℕ
hx : x ∈ ↑(range n) ×ˢ ↑(range n)
⊢ x ∈ Prod.map Nat.cast Nat.cast ⁻¹' Set.Iio ↑n ×ˢ Set.Iio ↑n
Module: Mathlib.Combinatorics.Additive.Energy

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

Tactic:
aesop (add simp [filter_eq_empty_iff, mul_mem_mul])

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ (#univ).choose r

Tactic:
← card_powersetCard

Goal state after:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ #(powersetCard r univ)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ ofColex (toColex t)
hbc : b ≤ c
⊢ b ≤ a

Tactic:
exact hbc.trans <| ht _ hct

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

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : map f hf (mk K u hu) = map f hf (mk K v hv)
⊢ mk K u hu = mk K v hv

Tactic:
simp only [map_mk, mk_eq_mk_iff'] at h ⊢
  rcases h with ⟨a, ha⟩
  refine ⟨τ a, hf ?_⟩
  rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]

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
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A

Tactic:
let H := stabilizer G A

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
hA : #(A * A) ≤ #A
ha : a ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
⊢ a •> ↑(stabilizer G A) = ↑A ∧ ↑(stabilizer G A) <• a = ↑A
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)

Tactic:
apply_symm_apply

Goal state after:
case h.right
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ (some a, f) = (some a, f)
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 : ℕ
⊢ x ∈ Finset.range (n + 1) →
    (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))

Tactic:
hx

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)
⊢ (↑n + 1) * ((-1) ^ x * ↑((x + 1).ascFactorial (n - x))) = (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x))
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
i : Fin d.succ
x✝ : i ∈ univ
⊢ ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i

Tactic:
rw [gosper_trick i.is_le, mul_div]

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 : 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
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝ : #l = #A
this : #r = #A
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
exact weak_invMulSubgroup_bound h

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

Goal state before:
pp: p : DyckWord
⊢ ↑p = [] ↔ p = 0

Tactic:
rw [DyckWord.ext_iff]

Goal state after:
p : DyckWord
⊢ ↑p = [] ↔ ↑p = ↑0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
k : ℕ
⊢ count D (List.take k (List.drop i ↑p)) ≤ count U (List.take k (List.drop i ↑p))

Tactic:
show i = min i (i + k) by omega,

Goal state after:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi : count U (List.take (min i (i + k)) ↑p) = count D (List.take (min i (i + k)) ↑p)
⊢ count D (List.take k (List.drop i ↑p)) ≤ count U (List.take k (List.drop i ↑p))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
rw [DyckWord.ext_iff]

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

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

Tactic:
rw [DyckWord.ext_iff]

Goal state after:
p : DyckWord
⊢ ↑(p.nest.drop ((↑p).length + 1 + 1) ⋯) = ↑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 β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
⊢ f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

Tactic:
ext x y

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
x y : α × β
a✝ : x ≤ y
⊢ (f₁.prod g₁ * f₂.prod g₂) x y = ((f₁ * f₂).prod (g₁ * g₂)) x y
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:
ext x y

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x y : α × β
a✝ : x ≤ y
⊢ (IncidenceAlgebra.prod 1 1) x y = 1 x y
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_4
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
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
x : ℕ
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
          parts_pos := ⋯, parts_sum := ⋯ }.toFinsuppAntidiag
      x =
    g x

Tactic:
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.GenFun

Goal state before:
pp: case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
⊢ x ∈ s \ p.parts.toFinset → (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

Tactic:
hx

Goal state after:
case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s \ p.parts.toFinset
⊢ (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ ∏' (b : ℕ), (if ¬m ∣ b + 1 then ∑' (j : ℕ), X ^ ((b + 1) * j) else 1) * (1 - X ^ (b + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))

Tactic:
simp_rw [ite_not, ite_mul, pow_mul]

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (∏' (b : ℕ), if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else (∑' (j : ℕ), (X ^ (b + 1)) ^ j) * (1 - X ^ (b + 1))) =
    ∏' (i : ℕ), (1 - (X ^ (i + 1)) ^ m)
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))) =
    (coeff n) 0

Tactic:
map_zero

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (coeff n)
      ((-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))) =
    0
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

pp: case inr
n : ℕ
hn : 0 ≤ ↑n / 3 - 2
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
· exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)

Goal state after:
case inr
n : ℕ
hn : 0 ≤ ↑n / 3 - 2
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)
Module: Mathlib.Combinatorics.Graph.Subgraph

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

Tactic:
ext x y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
⊢ K ≤ H

Tactic:
refine (Compatible.of_le_le h' h.le).le_iff.mpr ⟨hsu, fun e he ↦ ?_⟩
  obtain ⟨u, v, huv⟩ := K.exists_isLink_of_mem_edgeSet he
  exact h.2 (huv.mono h') (hsu huv.left_mem) (hsu huv.right_mem) |>.edge_mem

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
⊢ G₁.IsLink e = G₂.IsLink f

Tactic:
ext x y

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
h : G₁.Inc e = G₂.Inc f
x y : α
⊢ G₁.IsLink e x y ↔ G₂.IsLink f x y
Module: Mathlib.Combinatorics.Hypergraph.Basic

Goal state before:
pp: α : Type u_1
H : Hypergraph α
⊢ V(H) = ∅ ∧ E(H) = ∅ ∨ V(H).Nonempty ∨ E(H).Nonempty

Tactic:
grind [Set.Nonempty]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line (η → α) ι
C : (ι × η → α) → κ
⊢ Subspace.IsMono C l.toSubspace ↔
    IsMono
      (fun x ↦
        C fun x_1 ↦
          match x_1 with
          | (i, e) => x i e)
      l

Tactic:
by
  simp [Subspace.IsMono, IsMono, funext (toSubspace_apply _ _)]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
κ : Type (max v u)
inst✝ : Finite κ
h : Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

Tactic:
← singleton_dep,

Goal state after:
α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).Dep {e} ↔ M.IsLoop e ∧ e ∉ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ (M ／ I).IsLoop e

Tactic:
← singleton_dep,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ (M ／ I).Dep {e}
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finite
⊢ (M ／ C).Finite

Tactic:
rw [← dual_delete_dual]

Goal state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finite
⊢ (M✶ ＼ C)✶.Finite
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (M ／ I).IsLoop e ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
← singleton_dep,

Goal state after:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (M ／ I).Dep {e} ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
x : σ → R
⊢ (∀ (i : σ), x i ∈ S (e i)) → (eval x) ((rename ⇑e.symm) P) = 0

Tactic:
hx

Goal state after:
case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
x : σ → R
hx : ∀ (i : σ), x i ∈ S (e i)
⊢ (eval x) ((rename ⇑e.symm) P) = 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
this : Q = 0
⊢ (optionEquivLeft R σ).symm 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
this : Q = 0
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')

Tactic:
rw [contract_delete_contract_delete', sdiff_eq_left.mpr h]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_option.Heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
x : σ → R
⊢ (∀ (i : σ), x i ∈ S (Option.some i)) → (eval x) (Q.coeff m) = 0

Tactic:
hx

Goal state after:
case h_option.Heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (eval x) (Q.coeff m) = 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
⊢ (∀ (i : σ), x i ∈ S i) → (eval x) r = 0

Tactic:
hx

Goal state after:
case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ (eval x) r = 0