mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case succ
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ IsAddFreimanIso m (Iio ↑(k + 1)) (Iio (k + 1)) val

Tactic:
convert! isAddFreimanIso_Iic hm hkmn' using 1 <;> ext x

Goal state after:
case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ x ∈ Iio ↑(k + 1) ↔ x ∈ Iic ↑k

case e'_7
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : ℕ
⊢ x ∈ Iio (k + 1) ↔ x ∈ Iic k
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
y : EInt
f : ⊥ ⟶ y
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y

Tactic:
induction y using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y

Tactic:
induction y using WithBotTop.rec with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case top
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
y : EInt
f : ⊤ ⟶ y
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y

Tactic:
induction y using WithBotTop.rec with

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (↑(Finset.image g s)).PairwiseDisjoint f

Tactic:
rw [coe_image]
  exact hs.image_of_le hf

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b

Tactic:
exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hcd : c ≤ d
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
exact ⟨d, hd, hbc.trans hcd⟩

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } := ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) := ⋯
⊢ ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑((f.trans (finCongr ⋯)) t) < #s % #P.parts

Tactic:
intro ⟨p, _⟩

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
⊢ #↑⟨p, property✝⟩ = #s / #P.parts + 1 ↔ ↑((f.trans (finCongr ⋯)) ⟨p, property✝⟩) < #s % #P.parts
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
⊢ ∃ a_1 ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1

Tactic:
obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
⊢ ∃ a_1 ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case neg
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : ¬WellOrderingRel s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε t s).2)

Tactic:
exact G.right_nonuniformWitnesses_card fun i => h i.symm

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

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}

Tactic:
refine filter_congr fun x hx ↦ ?_

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2
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
ε : ℝ
⊢ (increment hP G ε).IsEquipartition

Tactic:
simp_rw [IsEquipartition, Set.equitableOn_iff_exists_eq_eq_add_one]
  refine ⟨m, fun A hA => ?_⟩
  rw [mem_coe, increment, mem_bind] at hA
  obtain ⟨U, hU, hA⟩ := hA
  exact card_eq_of_mem_parts_chunk hA

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support.toFinset \ {x}.toFinset)

Tactic:
← Set.toFinset_sdiff

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support \ {x}).toFinset
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 W
⊢ G.labelledCopyCount H = 0 ↔ H.Free G

Tactic:
simp [labelledCopyCount, Fintype.card_eq_zero_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
exact G.edgeSet_replaceVertex_of_not_adj hn

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).spanningCoe = (SimpleGraph.induce s G).spanningCoe

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was:
  `grind [induce_eq_coe_induce_top, Subgraph.spanningCoe_coe]` -/

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).spanningCoe = (SimpleGraph.induce s G).spanningCoe
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
i : ℕ
hi : (cons h✝ p✝).length ≤ i
⊢ (cons h✝ p✝).getVert i = w✝

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
p' : G.Walk u✝ w✝
h : Walk.map f (cons h✝ p✝) = Walk.map f p'
⊢ cons h✝ p✝ = p'

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.reverse.reverse = p✝
⊢ (cons h✝ p✝).reverse.reverse = cons h✝ p✝

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk v✝ w), (p✝.reverseAux q).length = p✝.length + q.length
q : G.Walk u✝ w
⊢ ((cons h✝ p✝).reverseAux q).length = (cons h✝ p✝).length + q.length

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v' : V
p : G.Walk v' v
hwp : w ∈ p.support
h : u ≠ w
hadj : G.Adj u v'
⊢ (cons hadj p).takeUntil w ⋯ = cons hadj (p.takeUntil w hwp)

Tactic:
simp [Walk.takeUntil, h]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : ¬v = u
⊢ u ∈ p.support

Tactic:
cases h
      · exact (hx rfl).elim
      · assumption

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
p' : G.Walk u✝ v'
he : (cons h✝ p✝).concat h = p'.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = p'

Tactic:
| cons _ _ ih =>

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
⊢ u :: p.tail.support = p.support

Tactic:
by
  simp [hp]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n < p.length
⊢ p.dropLast.getVert n = p.getVert n

Tactic:
by
  grind [getVert_eq_support_getElem, length_dropLast, support_dropLast]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
⊢ #s = G.cliqueNum

Tactic:
obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
t : Finset α
tc : G.IsClique ↑t
tcard : #t = G.cliqueNum
⊢ #s = G.cliqueNum
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
t : Finset α
tc : G.IsClique ↑t
tcard : #t = G.cliqueNum
⊢ ¬#s < G.cliqueNum

Tactic:
by simp [← tcard, sm t tc]

Goal state after:
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:
| cons _ _ ih =>

Goal state after:
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:
| cons _ _ ih =>

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), p✝.IsPath → (p✝.transfer H hp).IsPath
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
pp : (cons h✝ p✝).IsPath
⊢ ((cons h✝ p✝).transfer H hp).IsPath

Tactic:
| cons _ _ ih =>

Goal state after:
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] * ↑(#A) = ↑(#(A * B))

Tactic:
mulConst_mul_card

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#(A * B)) = ↑(#(A * B))
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 0 < ↑(#A)

Tactic:
· exact mod_cast card_le_card_mul_right hB

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 0 < ↑(#A)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
norm_cast; exact divConst_mul_card _ _

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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * ↑(#A) * ↑(#A) = ↑(#(A * A)) * ↑(#A)

Tactic:
mulConst_mul_card

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#A) = ↑(#(A * A)) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#(A / A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
rw [← divConst_mul_card]

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * ↑(#A) * (δₘ[A] * ↑(#A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))
Module: Mathlib.FieldTheory.ChevalleyWarning

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

Tactic:
by rw [mul_sum]

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ map (fun x ↦ x + 1) (map (fun x ↦ x + k) n.bitIndices) = map (fun x ↦ x + (1 + k)) n.bitIndices

Tactic:
List.map_map,

Goal state after:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ map ((fun x ↦ x + 1) ∘ fun x ↦ x + k) n.bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
hma : m < a
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
hab : a ≤ b
⊢ False

Tactic:
exact hbt <| (hw <| hwa.trans_le hab).1 <| mem_of_mem_erase hbs

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

Goal state before:
pp: V : Type u_1
adj adj' : V → V → Bool
⊢ (fun x ↦ { Adj := fun v w ↦ x v w = true }) adj = (fun x ↦ { Adj := fun v w ↦ x v w = true }) adj' → adj = adj'

Tactic:
simp_rw [mk.injEq]

Goal state after:
V : Type u_1
adj adj' : V → V → Bool
⊢ ((fun v w ↦ adj v w = true) = fun v w ↦ adj' v w = true) → adj = adj'
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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> ((A⁻¹ * A) <• a)

Tactic:
h₂

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
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)) =
    ↑(↑i).centralBinom / (↑↑i + 1) * ↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)

Tactic:
mul_div

Goal state after:
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) =
    ↑(↑i).centralBinom / (↑↑i + 1) * ↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)
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
⊢ r = z •> A⁻¹

Tactic:
rw [inter_eq_right, ← this, mul_assoc _ A,
      ← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), subset_smul_finset_iff]

Goal state after:
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
⊢ a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))
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
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
hx : x ∈ s
⊢ x ∣ g x

Tactic:
specialize hprod x hx
    contrapose hprod
    have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx)
    rw [map_add, (summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)]
    rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp]
    congrm (?_ + ∑' (i : ℕ), ?_)
    · suffices g x ≠ 0 by simp [this]
      contrapose hprod
      simp [hprod]
    · rw [map_smul, coeff_X_pow]
      apply smul_eq_zero_of_right
      suffices g x ≠ x * (i + 1) by simp [this]
      contrapose hprod
      simp [hprod]

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

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

Tactic:
apply take_of_length_le

Goal state after:
p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1
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
⊢ False

Tactic:
have one_sub_K_pos : 0 < 1 - K := by linarith

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
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ stirlingFirst 0 (n✝ + 1) = 0

Tactic:
stirlingFirst

Goal state after:
n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ 0 = 0
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
⊢ Tendsto
    (fun k ↦
      (-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)))
    atTop (𝓝 0)

Tactic:
rw [tendsto_iff_coeff_tendsto]

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
⊢ ∀ (d : ℕ),
    Tendsto
      (fun i ↦
        (coeff d)
          ((-1) ^ (i + 1) * X ^ ((i + 1) * (3 * i + 4) / 2) *
            ∑' (n : ℕ), X ^ ((i + 1) * n) * ∏ i_1 ∈ Finset.range (n + 1), (1 - X ^ (i + i_1 + 1))))
      atTop (𝓝 ((coeff d) 0))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#Z) ≤ 2 / ε - 1

Tactic:
calc
          (#Z : ℝ)
      _ = #(H : Set G).toFinset * #Z / #(H : Set G).toFinset          := by field
      _ = #(Set.toFinset H * Z) / #(H : Set G).toFinset               := by
        simp [← card_mul_eq_mul_card_of_injOn_opSMul hZinj, Nat.cast_mul]
      _ = #(Set.toFinset H * S) / #(H : Set G).toFinset               := by
        congr 3; simpa using congr(($hHZS).toFinset)
      _ ≤ (2 / ε - 1) * #(H : Set G).toFinset / #(H : Set G).toFinset := ?_
      _ = 2 / ε - 1                                                   := by field

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#((↑H).toFinset * S)) / ↑(#(↑H).toFinset) ≤ (2 / ε - 1) * ↑(#(↑H).toFinset) / ↑(#(↑H).toFinset)