mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
⊢ b ∈ t

Tactic:
mem_filter

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ edgeDensity r ∅ t = 0

Tactic:
by
  rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]

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

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
rw [if_pos lt, if_neg (asymm lt)]

Goal state after:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
    rw [two_mul]; gcongr; exact P.card_parts_le_card

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
have : Nonempty α := by
    rw [← Fintype.card_pos_iff]
    exact (bound_pos _ _).trans_le hα

Goal state after:
case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : A ∈ ↑(increment hP G ε).parts
⊢ #A = m ∨ #A = m + 1

Tactic:
rw [mem_coe, increment, mem_bind] at hA

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : ∃ A_1, ∃ (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts
⊢ #A = m ∨ #A = m + 1
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)

Tactic:
simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
  · have := h (sdiff_subset (t := H.edgeFinset))
    simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
    exact this hH
  · classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ G.copyCount H = #(image Copy.toSubgraph univ)

Tactic:
copyCount

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ #{G' | Nonempty (H ≃g G'.coe)} = #(image Copy.toSubgraph univ)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ G.copyCount ⊥ = 1

Tactic:
copyCount

Goal state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ #{G' | Nonempty (⊥ ≃g G'.coe)} = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))

Tactic:
exact ih (Nat.succ_lt_succ_iff.1 hi)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)

Tactic:
induction p with
  | nil => rfl
  | cons h _ ih => simp [ih (cons h.symm q)]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)

Tactic:
by
  induction p with
  | nil => rfl
  | cons h _ ih => simp [ih (cons h.symm q)]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ ((p.takeUntil w hw).append (p.dropUntil w hw)).takeUntil x ⋯ = p.takeUntil x ⋯

Tactic:
take_spec

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ ((c.takeUntil u h).append (c.dropUntil u h)).support.tail ~r c.support.tail

Tactic:
take_spec

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ c.support.tail ~r c.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ ((c.takeUntil u h).append (c.dropUntil u h)).darts ~r c.darts

Tactic:
take_spec

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ c.darts ~r c.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate u h).Nil ↔ c.Nil

Tactic:
by
  simp [← length_eq_zero_iff]

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
n : ℕ
⊢ (p.take n).Nil ↔ p.Nil ∨ n = 0

Tactic:
by
  cases p <;> cases n <;> simp [take]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert 0

Tactic:
getVert_cons _ _ n.add_one_ne_zero,

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ q.getVert (n + 1 - 1) = (cons h q).getVert 0
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ ⊥.IsNClique n s ↔ n ≤ 1 ∧ #s = n

Tactic:
rw [isNClique_iff, isClique_bot_iff]
  refine and_congr_left ?_
  rintro rfl
  exact card_le_one.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsNClique (Fintype.card β) (map f.toEmbedding univ)

Tactic:
by
  rw [isNClique_iff, card_map, card_univ, coe_map, coe_univ, Set.image_univ]
  exact ⟨isClique_range_copy_top f, rfl⟩

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

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
⊢ False

Tactic:
obtain ⟨v, w, hn, he⟩ := exists_ne_map_eq_of_card_lt (Sigma.fst ∘ f) (by simp [hc])

Goal state after:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : v ≠ w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w ↦ ¬G.Adj v w

Tactic:
repeat rw [Set.Pairwise]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj

Tactic:
repeat rw [Set.Pairwise]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s

Tactic:
rw [isNClique_iff]
  simp [isNIndepSet_iff]

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
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
⊢ 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)

Tactic:
let C := (P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

Tactic:
mulConst

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ ↑(#(A * B)) / ↑(#A) ≤ ↑(Fintype.card G) / ↑(#A)
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ (i : (α × α) × α × α),
    i ∈ {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2} ↔
      (Equiv.prodProdProdComm α α α α) i ∈ {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}

Tactic:
by simp [and_and_and_comm]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝ : ↑A = Fin.val '' Nat.cast '' ↑A
this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
x : ℕ
hx : x ∈ Set.Iio n
⊢ x < n

Tactic:
simpa only [coe_range, Set.mem_Iio] using hx

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

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Tactic:
have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')

Goal state after:
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
by_cases a ∈ s <;> aesop

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u : Finset α
a✝ b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha : a ∈ ofColex t ∧ a ∉ ofColex s ∨ a ∈ ofColex s ∧ a ∉ ofColex t
hamax : ∀ (x' : α), x' ∈ ofColex t ∧ x' ∉ ofColex s ∨ x' ∈ ofColex s ∧ x' ∉ ofColex t → id x' ≤ id a
⊢ s ≤ t ∨ t ≤ s

Tactic:
exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩)
      (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩)

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

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
simp_rw [this]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ s (n + 1)) atTop (𝓝 (Real.exp (-1)))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!

Tactic:
unfold rest

Goal state after:
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)! = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < (↑p.nest).length
⊢ count D (List.take i ↑p.nest) < count U (List.take i ↑p.nest)

Tactic:
nest,

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < ([U] ++ ↑p ++ [D]).length
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.denest ⋯ = p

Tactic:
nest,

Goal state after:
p : DyckWord
⊢ { toList := [U] ++ ↑p ++ [D], count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯ = p
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✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ 1 * f = f

Tactic:
by ext; simp [*]

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✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 1 = f

Tactic:
by ext; simp [*]

Goal state after:
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_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)

Tactic:
have r_inv z : r z⁻¹ = r z := by simp [r, inv_inv]

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
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
rw [hm, factorial_zero, eq_comm]
      rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]

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

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

Tactic:
nest,

Goal state after:
p : DyckWord
⊢ ([U] ++ ↑p ++ [D]).length ≤ (↑p).length + 1 + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case refl
p q : DyckWord
⊢ ↑p <:+: ↑p

Tactic:
| refl =>

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

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' = count D r'
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Tactic:
simp [hq]

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

Goal state before:
pp: case refl
p q : DyckWord
⊢ p.semilength ≤ p.semilength

Tactic:
| refl =>

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

Goal state before:
pp: p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ p = q

Tactic:
simp_rw [two_mul_semilength_eq_length] at pnq

Goal state after:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : (↑p).length = (↑q).length
⊢ p = q
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ powMulProdOneSubPow 0 x_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
simp_rw [powMulProdOneSubPow, zero_add, one_mul] at hsum

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ex A ∈ M

Tactic:
mem_filter

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A