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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
⊢ (c.takeUntil w h).IsPath

Tactic:
by_cases hvw : v = w
  · subst hvw
    simp
  rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc
  exact (c.takeUntil w h).isPath_reverse_iff.mp (hc.isPath_of_append_right (not_nil_of_ne hvw))

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
h : G.CliqueFree n
v w : α
⊢ (G ⊔ edge v w).CliqueFree (n + 1)

Tactic:
exact fun _ hs ↦ (hs.erase_of_sup_edge_of_mem <|
    (h.mono n.le_succ).mem_of_sup_edge_isNClique hs).not_cliqueFree h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G H : SimpleGraph α
ε δ : 𝕜
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
⊢ ((↑(G.cliqueFinset 3)).Pairwise fun x y ↦ #(x ∩ y) ≤ 1) ↔ G.EdgeDisjointTriangles

Tactic:
by
    simp only [coe_cliqueFinset, EdgeDisjointTriangles, Finset.card_le_one, ← coe_inter]; rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
e : Sym2 α
he : e ∈ G.edgeFinset
⊢ #(bipartiteBelow (fun s e ↦ e ∈ s.sym2) (G.cliqueFinset 3) e) ≤ 1

Tactic:
simpa only [card_le_one, mem_bipartiteBelow, and_imp, Set.Subsingleton, Set.mem_ofPred_eq,
      mem_cliqueFinset_iff, mem_cliqueSet_iff]
      using hG.mem_sym2_subsingleton (G.not_isDiag_of_mem_edgeSet <| mem_edgeFinset.1 he)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(∑ a ∈ G.badVertices ε s t, #(map { toFun := fun x ↦ (a, x), inj' := ⋯ } ({y ∈ t | G.Adj a y}))) ≤
    ↑(#(G.badVertices ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, ↑(#({y ∈ t | G.Adj x y})) ≤ #(G.badVertices ε s t) • ((↑(G.edgeDensity s t) - ε) * ↑(#t))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case hbc
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹

Tactic:
exact min_le_left _ _

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H ↦ H.CliqueFree 3) (G.deleteEdges ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#∅)
⊢ ε ≤ 0

Tactic:
coe_empty,

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H ↦ H.CliqueFree 3) (G.deleteEdges ∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#∅)
⊢ ε ≤ 0
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
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤
    (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3 * ↑(Fintype.card α) ^ 3

Tactic:
by
      gcongr; exact triangleRemovalBound_le hε₁

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#({x ∈ s ×ˢ t ×ˢ u |
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}))

Tactic:
by
  classical
  have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  have : X'.biUnion _ ⊆ (s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
    triangle_split_helper _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i),
      sub_le_sub_iff_left, mul_assoc, mul_comm ε, two_mul]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop

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

Goal state before:
pp: G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ (graph (triangleIndices A)).FarFromTriangleFree (ε / 9)

Tactic:
by
  refine farFromTriangleFree _ ?_
  simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]
  ring_nf
  simpa only [mul_comm] using hε

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔ ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x

Tactic:
by
  grind [MulDissociated, InjOn]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑t \ ↑u ⊆ s

Tactic:
exact sdiff_subset.trans ‹_›

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑u \ ↑t ⊆ s

Tactic:
exact sdiff_subset.trans ‹_›

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

Goal state before:
pp: case h₂.refine_2.refine_2
α : 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
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
this : 0 < ε
UVl : 4 / 5 * ε * (4 / 5 * ε) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts * (↑(#(star hP G ε hV U)) / 4 ^ #P.parts)
⊢ 0 ≤ 9 / 4 ^ 2 * ε ^ 2

Tactic:
simp [pow_two_nonneg]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u : Finset α
a b : α
r : ℕ
s t : Colex (Finset α)
⊢ s ≤ t ∨ t ≤ s

Tactic:
obtain rfl | hts := eq_or_ne t s

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ u : Finset α
a b : α
r : ℕ
t : Colex (Finset α)
⊢ t ≤ t ∨ t ≤ t

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
⊢ s ≤ t ∨ t ≤ s
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v

Tactic:
c,

Goal state after:
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : 0 • w = v
c : a = 0
⊢ 0 = v
Module: Mathlib.LinearAlgebra.Projectivization.Basic

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

Tactic:
change FiniteDimensional K (K ∙ v.rep)

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

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
⊢ #s ≤ #(s.biUnion t)

Tactic:
by_cases hs₀ : #s = 0

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : #s = 0
⊢ #s ≤ #(s.biUnion t)

case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case ind
n : ℕ
hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n

Tactic:
rcases n with _ | _ | n

Goal state after:
case ind.zero
hyp : ∀ m < 0, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin 0)) = numDerangements 0

case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)
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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
have h₁ : ∀ p : P, 0 < lineCount L p := fun p =>
        Exists.elim (exists_ne p) fun q hq =>
          (congr_arg _ Nat.card_eq_fintype_card).mpr
            (Fintype.card_pos_iff.mpr ⟨⟨mkLine hq, (mkLine_ax hq).2⟩⟩)

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
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
⊢ ∃ p ∈ l₁, p ∈ l₂
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ Fintype.card { l // q ∈ l } = Fintype.card { l // q ∈ l } - 1 + 1

Tactic:
Nat.sub_add_cancel

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ Fintype.card { l // q ∈ l } = Fintype.card { l // q ∈ l }

case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ 1 ≤ Fintype.card { l // q ∈ l }
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card P = order P L ^ 2 + order P L + 1

Tactic:
have h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P := by
      apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
      convert! (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
    have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L := by
      intro l
      rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
        Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ←
        Nat.card_eq_fintype_card]
      refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)
      rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
      simp_rw [Subtype.ext_iff]
    simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]
    rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]

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⁻¹
⊢ l ∪ r ⊆ a •> (A⁻¹ * A)

Tactic:
union_subset_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
hr : r = z •> A⁻¹
⊢ l ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
suffices this : _ by
      by_cases hm : 0 ∈ m.toFinset
      · rw [← Finset.prod_erase_mul _ _ hm]
        rw [← Finset.prod_erase_mul _ _ hm]
        simp only [factorial_zero, one_pow, mul_one, zero_mul]
        exact this
      · nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
        nth_rewrite 3 [← Finset.erase_eq_of_notMem hm]
        exact this

Goal state after:
case e_a
m : Multiset ℕ
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
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:
by
    rw [show i = min i (i + k) by omega, ← take_take] at hi
    rw [take_drop, ← add_le_add_iff_left (((p.toList.take (i + k)).take i).count U),
      ← count_append, hi, ← count_append, take_append_drop]
    exact p.count_D_le_count_U _

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x ∈ range (↑p).length, decide (count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)) = true

Tactic:
simp only [mem_range, decide_eq_true_eq]

Goal state after:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x < (↑p).length, count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case a
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
ha0 : a ≠ 0
hsum : (p.parts.erase a).sum + a = n + 1
⊢ a * (count a p.parts * p.parts.bell) = (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)

Tactic:
grind [Nat.add_one_mul_choose_eq, cons_erase, bell_cons_mul_count]

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
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hg' : g ∉ Set.range toFinsuppAntidiag
this : ∃ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0
⊢ ∏ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) = 0

Tactic:
obtain ⟨i, hi, hi'⟩ := this
    apply prod_eq_zero hi hi'

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

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

Tactic:
take,

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = List.take ((↑q).length - (↑p).length) ↑q
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_3
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
h1 : s.sum ⇑g = d
h2 : g.support ⊆ s
⊢ (Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ }).sum = d

Tactic:
refine Eq.trans ?_ h1

Goal state after:
case refine_3
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
h1 : s.sum ⇑g = d
h2 : g.support ⊆ s
⊢ (Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ }).sum = s.sum ⇑g
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)

Tactic:
rcases Nat.eq_zero_or_pos m with rfl | hm

Goal state after:
case inl
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
⊢ Multipliable fun i ↦ ∑ j ∈ range 0, X ^ ((i + 1) * j)

case inr
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) ≤ ↑(ruzsaSzemerediNumberNat (n + 3))

Tactic:
grw [Nat.mul_div_le]

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

Goal state before:
pp: case calc_1
n : ℕ
⊢ n ≤ 2 * 3 * (n / 6) + 2 * 3

Tactic:
rw [← mul_add_one]

Goal state after:
case calc_1
n : ℕ
⊢ n ≤ 2 * 3 * (n / 6 + 1)
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
⊢ e ∈ E(H)

Tactic:
obtain ⟨_, _, hxy⟩ := G.exists_isLink_of_mem_edgeSet he

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
w✝¹ w✝ : α
hxy : G.IsLink e w✝¹ w✝
⊢ e ∈ E(H)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a

Tactic:
have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_

Goal state after:
case refine_5
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
h : ∃ m ∈ S, m * m = m
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a

case refine_1
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (r : Ultrafilter M), Continuous fun x ↦ x * r

case refine_2
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ S.Nonempty

case refine_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S

case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.tail'
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
b : Stream' M
n : M
h : FP b.tail n
ih : ∀ (p : { s // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → n ∈ ↑p

Tactic:
rintro p rfl
    refine Set.inter_subset_left (ih (succ p) ?_)
    rw [Stream'.corec_eq, Stream'.tail_cons]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ (M ＼ D).loops = M.loops \ D

Tactic:
simp [loops]

Goal state after: