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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.edgeSet \ Sym2.diagSet = G.edgeSet

Tactic:
exact Set.disjoint_left.mpr G.edgeSet_subset_compl_diagSet |>.sdiff_eq_left

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.induce G'.verts = G'

Tactic:
by
  ext
  · simp
  · constructor <;>
      simp +contextual only [induce_adj, imp_true_iff, and_true]
    exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n < p.darts.length
⊢ p.darts[n] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }

Tactic:
p.length_darts

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h✝ : n < p.darts.length
h : n < p.length
⊢ p.darts[n] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.reverse = p

Tactic:
by
  induction p with
  | nil => rfl
  | cons _ _ ih => simp [ih]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)

Tactic:
simp [Nat.succ_sub hi.le]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts

Tactic:
rw [isSubwalk_iff_support_isInfix, List.infix_iff_getElem?, List.infix_iff_getElem?]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ (∃ k,
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]) ↔
    ∃ k,
      p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.support

Tactic:
← List.mem_reverse,

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.support.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup

Tactic:
exact ⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.tail.length + 1 = p.length

Tactic:
← length_cons (p.adj_snd hp),

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ (cons ⋯ p.tail).length = p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝¹ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
w✝ : y✝ ∈ F
binA : ⟨y✝, ⋯⟩ ∈ A
anb : x✝ ≠ y✝
⊢ G.Adj x✝ y✝

Tactic:
exact S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map (⇑e.toEmbedding) (SimpleGraph.map (⇑e.symm.toEmbedding) G)).LocallyLinear

Tactic:
map_symm

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map (⇑e.toEmbedding) (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : completeGraph (Fin n) ⊑ H
⊢ completeGraph (Fin n) ⊑ G

Tactic:
exact h.trans hle

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

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

Tactic:
ENat.card_eq_coe_fintype_card,

Goal state after:
case neg
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
h : ¬Infinite ι
this : Fintype ι
hc : ↑n ≤ ↑(Fintype.card ι)
⊢ ¬(completeMultipartiteGraph V).CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : G.IsIndepSet ↑t
⊢ #t ≤ G.indepNum

Tactic:
rw [← isClique_compl] at tc

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ G.indepNum
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsCircuit
⊢ p.IsCircuit

Tactic:
by
  rw [isCircuit_def, ne_eq, eq_nil_iff_nil]
  rw [isCircuit_def, ne_eq, eq_nil_iff_nil, nil_map_iff] at hp
  exact hp.imp_left .of_map

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 : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε * (↑(Fintype.card G) * ↑(Fintype.card G)) ≤ ↑(Fintype.card G) * ↑(Fintype.card G)
⊢ ε ≤ 1

Tactic:
rwa [mul_le_iff_le_one_left] at this

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε * (↑(Fintype.card G) * ↑(Fintype.card G)) ≤ ↑(Fintype.card G) * ↑(Fintype.card G)
⊢ 0 < ↑(Fintype.card G) * ↑(Fintype.card G)
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ insert a s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
⊢ a ∈ s'.mulSpan

Tactic:
subset_insert_iff_of_notMem hat

Goal state after:
case neg
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
⊢ a ∈ s'.mulSpan
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
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
    ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2

Tactic:
gcongr
      have Ul : 4 / 5 * ε ≤ #(star hP G ε hU V) / _ :=
        eps_le_card_star_div hPα hPε hε₁ hU hV hUVne hUV
      have Vl : 4 / 5 * ε ≤ #(star hP G ε hV U) / _ :=
        eps_le_card_star_div hPα hPε hε₁ hV hU hUVne.symm fun h => hUV h.symm
      rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _), ←
        _root_.div_mul_div_comm, mul_assoc]
      have : 0 < ε := by sz_positivity
      have UVl := mul_le_mul Ul Vl (by positivity) ?_
      swap
      · -- This seems faster than `exact div_nonneg (by positivity) (by positivity)` and *much*
        -- (tens of seconds) faster than `positivity` on its own.
        apply div_nonneg <;> positivity
      refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)
      · norm_num
        nlinarith
      · simp [pow_two_nonneg]

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

Goal state before:

Tactic:
_ ≤ (p - 1) + (p - 1) := by
      gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _
      · exact (totalDegree_X_pow ..).le
      · exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le
    _ < 2 * p - 1 := by have := (Fact.out : p.Prime).two_le; lia

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t

Tactic:
toColex_le_toColex,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ (∀ ⦃a : α⦄, a ∈ s \ u → a ∉ t \ u → ∃ b ∈ t \ u, b ∉ s \ u ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ ¬toColex t ≤ toColex s ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
toColex_le_toColex,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (¬∀ ⦃a : α⦄, a ∈ t → a ∉ s → ∃ b ∈ s, b ∉ t ∧ a ≤ b) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
Module: Mathlib.LinearAlgebra.Projectivization.Basic

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

Tactic:
simp [f.map_smulₛₗ, ← ha, Units.smul_def]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
rw [x_vs_a, swap_apply_right]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f a) ≠ none
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
l : L
x✝ : l ∈ univ
⊢ ∑ a ∈ {p | p ∈ l}.toFinset, pointCount P (a, l).2 = ∑ a ∈ {l_1 | f l ∈ l_1}.toFinset, lineCount L (f l, a).1

Tactic:
simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]

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
l : L
x✝ : l ∈ univ
⊢ Nat.card ↑{p | p ∈ l} • lineCount L (f l) = Nat.card ↑{l_1 | f l ∈ l_1} • lineCount L (f l)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
apply sum_congr rfl

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) = catalan x.1 * catalan x.2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
A : Finset G
Z : Set G
hZA : Z ⊆ ↑A
hZinj : Set.InjOn (fun x ↦ ↑H <• x) Z
hHZA : (fun x ↦ ↑H <• x) '' Z = (fun x ↦ ↑H <• x) '' ↑A
⊢ ∃ Z ⊆ A, ↑H * ↑Z = ↑H * ↑A ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z

Tactic:
lift Z to Finset G using A.finite_toSet.subset hZA

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
A Z : Finset G
hZA : ↑Z ⊆ ↑A
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
hHZA : (fun x ↦ ↑H <• x) '' ↑Z = (fun x ↦ ↑H <• x) '' ↑A
⊢ ∃ Z ⊆ A, ↑H * ↑Z = ↑H * ↑A ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case inr.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

Tactic:
have H_toFinset_mul_Z : Set.toFinset H * Z = S := by simpa [← Finset.coe_inj]

Goal state after:
case inr.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹
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 j ↑p) < count U (List.take j ↑p)
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
rw [← (p.toList.take j).take_append_drop 1, count_append, count_append, take_take,
      min_eq_left (by lia), l1, head_eq_U] at eq

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 [U] + count D (List.drop 1 (List.take j ↑p)) < count U [U] + 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.Partition.GenFun

Goal state before:
pp: case neg
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
x : ℕ
hx : g x ≠ 0
⊢ x ∈ s

Tactic:
exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 <| by simpa using hx

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

Goal state before:
pp: case tail.inr.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength

Tactic:
· exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

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

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

Tactic:
simp_rw [Finsupp.prod, Multiset.toFinsupp_support, Multiset.toFinsupp_apply]

Goal state after:
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
⊢ ∏ a ∈ p.parts.toFinset, f a (Multiset.count a p.parts) =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
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
this : ↑(#(A ∩ B)) + ↑(#(A ∪ B)) = ↑(#A) + ↑(#B)
⊢ K * ↑(#(A ∩ B)) + K * ↑(#(A ∪ B)) = K * ↑(#A) + K * ↑(#B)

Tactic:
simp only [← mul_add, this]

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

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

Tactic:
rw [mul_assoc]
  obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0
  · exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)
  exact
    (mul_le_mul_of_nonneg_left Behrend.roth_lower_bound hn).trans
      (rothNumberNat_le_ruzsaSzemerediNumberNat' _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
h : G.IsLink e x y
h' : G.IsLink e x z
⊢ y = z

Tactic:
obtain rfl | rfl := h.right_eq_or_eq h'.symm

Goal state after:
case inl
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h h' : G.IsLink e x y
⊢ y = y

case inr
α : Type u_1
β : Type u_2
y z : α
e : β
G : Graph α β
h : G.IsLink e y y
h' : G.IsLink e y z
⊢ y = z
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x✝² : β
x✝¹ x✝ : α
⊢ G₁.IsLink x✝² x✝¹ x✝ ↔ G₂.IsLink x✝² x✝¹ x✝

Tactic:
by simp_rw [isLink_iff_inc, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).IsNonloopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v

Tactic:
isNonloopAt_iff_inc_not_isLoopAt,

Goal state after:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).Inc e x ∧ ¬(banana u v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I)

Tactic:
rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_sdiff, disjoint_comm,
    union_subset_iff, and_iff_left hI.subset_ground]
  tauto

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
a✝ :
  ∀ (y : MvPolynomial σ R),
    (invImage (fun x ↦ ⋯.wrap (m.toSyn (m.degree x))) Acc.wfRel).1 y f →
      ∃ g r,
        y = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree y)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
hb' : ¬∃ i, m.degree (b i) = 0
hf0 : ¬f = 0
hf : ¬∃ i, m.degree (b i) ≤ m.degree f
hf'0 : ¬m.subLTerm f = 0
⊢ ↑(⋯.wrap (m.toSyn (m.degree (m.subLTerm f)))) < ↑(⋯.wrap (m.toSyn (m.degree f)))

Tactic:
apply degree_sub_LTerm_lt
    intro hf0
    apply hf'0
    simp only [subLTerm, sub_eq_zero]
    nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0]
    simp

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

Goal state before:
pp: case nil
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hn : n ≤ nil.length
⊢ ∃ v p₁ p₂, nil = p₁.comp p₂ ∧ p₁.length = n

Tactic:
obtain ⟨rfl⟩ : n = 0 := by simpa using hn

Goal state after:
case nil
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
hn : 0 ≤ nil.length
⊢ ∃ v p₁ p₂, nil = p₁.comp p₂ ∧ p₁.length = 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_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
ha_not_in_compl : ¬a ∈ Sᶜ
hb_in_compl : b ∈ Sᶜ
u v : V
e : u ⟶ v
p₁ : Path a u
p₂ : Path v b
hp : p = p₁.comp (e.toPath.comp p₂)
hu_not_in_compl : u ∈ S
hv_in_compl : ¬v ∈ S
⊢ ∃ u, u ∈ S ∧ ∃ v, ¬v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hn : n < p.length + 1
⊢ n ≤ p.length

Tactic:
exact Nat.le_of_lt_succ hn

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ p 𝒜

Tactic:
obtain rfl | rfl := hu <;> assumption

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ #({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1

Tactic:
exact card_filter_le _ _

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⋯
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

Tactic:
div_lt_iff₀ (Nat.cast_pos.2 hn),

Goal state after:
case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) < ε * ↑n
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∉ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (t ∪ s).truncatedSup a = t.truncatedSup a

Tactic:
truncatedSup_union_left ht hs

Goal state after:
α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∉ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ t.truncatedSup a = t.truncatedSup a
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s t : Finset α
⊢ sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ

Tactic:
← compls_subset_compls,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s t : Finset α
⊢ sᶜˢᶜˢ ⊆ tᶜˢ ↔ s ⊆ tᶜˢ