mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
⊢ ThreeAPFree ↑(image (⇑(map (2 * d - 1))) (sphere n d k))

Tactic:
rw [coe_image]

Goal state after:
n d k : ℕ
⊢ ThreeAPFree (⇑(map (2 * d - 1)) '' ↑(sphere n d k))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i + 1 < 2 * d

Tactic:
← succ_le_iff,

Goal state after:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ ((a + b) i + 1).succ ≤ 2 * d
Module: Mathlib.Combinatorics.Additive.CovBySMul

Goal state before:
pp: M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
hBC : CovBySMul N L B C
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
⊢ CovBySMul N (K * L) A C

Tactic:
obtain ⟨F₂, hF₂, hFBC⟩ := hBC

Goal state after:
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : ↑(#F₁) ≤ K
hFAB : A ⊆ ↑F₁ • B
F₂ : Finset N
hF₂ : ↑(#F₂) ≤ L
hFBC : B ⊆ ↑F₂ • C
⊢ CovBySMul N (K * L) A C
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ∃ a_1, a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B
⊢ a ∈ F * (B / B)

Tactic:
obtain ⟨b, hb, c, hc₁, hc₂⟩ := H

Goal state after:
case neg
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
b : G
hb : b ∈ F
c : G
hc₁ : a⁻¹ • c ∈ B
hc₂ : b⁻¹ • c ∈ B
⊢ a ∈ F * (B / B)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ ↑G.edgeFinset

Tactic:
rw [mem_coe, mem_edgeFinset]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeSet
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]

Goal state after:
α : 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
⊢ (g '' ↑s).PairwiseDisjoint f
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G.degree v = 1 ↔ ∃! w, G.Adj v w

Tactic:
rw [degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ (∃! a, a ∈ G.neighborFinset v) ↔ ∃! w, G.Adj v w
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
⊢ (Finset.map (↑e).symm.toEmbedding u).sup id = u.sup (⇑e.symm ∘ id)

Tactic:
sup_map

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
⊢ u.sup (id ∘ ⇑(↑e).symm.toEmbedding) = u.sup (⇑e.symm ∘ id)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
b : α
P✝ : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
c : α
hc : c ∈ P.parts
⊢ b ∈ P.parts

Tactic:
simp_rw [← h c hc]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
b : α
P✝ : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
c : α
hc : c ∈ P.parts
⊢ c ∈ P.parts
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: 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
i : EInt
X : C
⊢ (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)

Tactic:
induction i using WithBotTop.rec with simp [truncGE_map_truncGEπ_app]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
⊢ G.IsUniform 1 s t

Tactic:
intro s' hs' t' ht' hs ht

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * 1 ≤ ↑(#s')
ht : ↑(#t) * 1 ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
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
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∑ x ∈ P.parts.attach,
      #(if h : #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then (equitabilise ⋯).parts
        else (equitabilise ⋯).parts) =
    stepBound #P.parts

Tactic:
apply_dite card,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ (∑ x ∈ P.parts.attach,
      if h : #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then #(equitabilise ⋯).parts
      else #(equitabilise ⋯).parts) =
    stepBound #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
h : H ≤ G
⊢ G.deleteEdges (G.edgeSet \ H.edgeSet) = H

Tactic:
rw [← edgeSet_sdiff, deleteEdges_edgeSet, sdiff_sdiff_eq_self h]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw

Tactic:
ext <;> simp [or_comm, and_comm]

Goal state after:
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 : Finset α
hU : U ∈ P.parts
s : Finset α
hs : s ∈ (chunk hP G ε hU).parts
⊢ #s = m ∨ #s = m + 1

Tactic:
unfold chunk at hs

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
hs :
  s ∈
    (if hUcard : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
      else equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m ≤ ↑(∑ i ∈ 𝒜, #i)

Tactic:
← cast_mul,

Goal state after:
case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜 * m) ≤ ↑(∑ i ∈ 𝒜, #i)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List V
hne : l ≠ []
hchain : List.IsChain G.Adj l
⊢ (ofSupport l hne hchain).length = l.length - 1

Tactic:
grind [support_ofSupport]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.support ++ q.support.tail).Nodup → p.support.Nodup

Tactic:
exact List.Nodup.of_append_left

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
⊢ w ∈ p.support ↔ ∃ q r, q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
by
  refine ⟨fun hw ↦ ?_, fun ⟨q, r, hq, hr, hqr⟩ ↦ p.mem_support_iff_exists_append.mpr ⟨q, r, hqr⟩⟩
  obtain ⟨q, r, hqr⟩ := p.mem_support_iff_exists_append.mp hw
  have : (q.append r).IsPath := hqr ▸ hp
  exact ⟨q, r, this.of_append_left, this.of_append_right, hqr⟩

Goal state after:
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.append q).support.tail.Nodup
⊢ q.IsPath

Tactic:
rw [tail_support_append, List.nodup_append'] at this

Goal state after:
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
⊢ q.IsPath
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}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert (m + 1)

Tactic:
simpa [getVert_cons] using hnm

Goal state after:
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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#(A.sup id)) * ↑(#(B.sup id))

Tactic:
← cast_mul,

Goal state after:
α : 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#(A.sup id) * #(B.sup id))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x : Sym2 α), x ∉ G.edgeSet

Tactic:
Sym2.forall,

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), s(x, y) ∉ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} n ↔ 1 < n

Tactic:
obtain _ | _ | n := n <;>
    simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

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 α
⊢ ↑(#(Rel.interedges G.Adj (G.badVertices ε s t) t)) ≤ ↑(#(G.badVertices ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
by
  classical
  refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
    card_biUnion_le).trans ?_
  simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]
  exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

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

Goal state before:
pp: case hab.refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
      (↑(4 ^ #P.parts) * ↑(4 ^ #P.parts)) ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts

Tactic:
← cast_mul,

Goal state after:
case hab.refine_2
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
      ↑(4 ^ #P.parts * 4 ^ #P.parts) ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts
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
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := ⋯
this :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ #X' • (ε ^ 3 * ↑(#t) * ↑(#u))

Tactic:
rw [nsmul_eq_mul]

Goal state after:
α : 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
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#X') * (ε ^ 3 * ↑(#t) * ↑(#u))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case h₂
α : 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 (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#B) ≤ ε / 2 * ↑(Fintype.card α) ^ 2

pp: case h₂
α : 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 (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#C) ≤ 4 * (ε / 4) * ↑(Fintype.card α) ^ 2

Tactic:
· exact hP.card_biUnion_offDiag_le hε hP'

Goal state after:
case h₂
α : 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 (α × α) := ⋯
B : Finset (α × α) := ⋯
C : Finset (α × α) := ⋯
⊢ ↑(#C) ≤ 4 * (ε / 4) * ↑(Fintype.card α) ^ 2
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
⊢ MulDissociated ∅

Tactic:
simp [MulDissociated, subset_empty_iff]

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

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

Tactic:
by gcongr; simp; unfold cornersTheoremBound at hn; lia

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 ↑A
⊢ ∀ a ∈ ↑A, ↑↑a = id a

Tactic:
simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree ↑A
⊢ ∀ a ∈ A, a < 2 * n + 1
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 σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Tactic:
let F : Unit → MvPolynomial σ K := fun _ => f
  have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h
  convert! char_dvd_card_solutions_of_sum_lt p this
  aesop

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

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
⊢ ∀ ⦃x : M⦄, x ∈ a +ᵥ A.subsetSum → x ∈ (insert a A).subsetSum

Tactic:
mem_vadd_finset,

Goal state after:
M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
⊢ ∀ ⦃x : M⦄, (∃ y ∈ A.subsetSum, a +ᵥ y = x) → x ∈ (insert a A).subsetSum
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
h : t₀ ∈ 𝒜
⊢ False

Tactic:
obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h

Goal state after:
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
k : ℕ
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
h : t₀ ∈ 𝒜
hn : 2 ≤ 0
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * 0 - 1 ≤ #s → ∃ t ⊆ s, #t = 0 ∧ ↑0 ∣ ∑ i ∈ t, a i
hs : 2 * (m * 0) - 1 ≤ #s
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ ↑0 ∣ ∑ i ∈ t, a i
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ ↑0 ∣ ∑ i ∈ t, a i
this : 2 * 0 - 1 ≤ #(s \ 𝒜.biUnion id)
ht₀card : #t₀ = 0
ht₀sum : ↑0 ∣ ∑ i ∈ t₀, a i
⊢ False
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w] ↔ True

Tactic:
iff_true

Goal state after:
case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w]
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: 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
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
p : P
hl : p ∉ l
⊢ #{l} ≤ #({l}.biUnion t)

Tactic:
rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]

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
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
p : P
hl : p ∉ l
⊢ #(t l) ≠ 0
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
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : #(s.biUnion t)ᶜ ≤ #sᶜ
⊢ #s ≤ #(s.biUnion t)

Tactic:
Finset.card_compl,

Goal state after:
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
hs₁ : ¬#s = 1
this : Fintype.card P - #(s.biUnion t) ≤ #sᶜ
⊢ #s ≤ #(s.biUnion t)