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

Goal state before:
pp: case h₁
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ 1 - δ ≤ ↑(#s₂) / ↑(#s₁)

Tactic:
refine (le_div_iff₀ ?_).2 hs₂
    exact mod_cast h₁.card_pos

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

Goal state before:
pp: case h₁
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ 1 - δ ≤ ↑(#s₂) / ↑(#s₁)

pp: case h₂
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ 1 - δ ≤ ↑(#t₂) / ↑(#t₁)

Tactic:
· refine (le_div_iff₀ ?_).2 hs₂
    exact mod_cast h₁.card_pos

Goal state after:
case h₂
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ 1 - δ ≤ ↑(#t₂) / ↑(#t₁)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #((P.nonUniforms G ε).biUnion fun x ↦ x.1 ×ˢ x.2) ≤ ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)

Tactic:
exact card_biUnion_le

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
x : Finset α
| x ∈ P.parts

Tactic:
← insert_erase hu₁

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
x : Finset α
| x ∈ insert u (P.parts.erase u)
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
ε : ℝ
s₁ s₂ : Finset α
hs✝ : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
a✝¹ : ⟨(s₁, s₂), hs✝⟩ ∈ ↑P.parts.offDiag.attach
t₁ t₂ : Finset α
ht✝ : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
a✝ : ⟨(t₁, t₂), ht✝⟩ ∈ ↑P.parts.offDiag.attach
hst : ⟨(s₁, s₂), hs✝⟩ ≠ ⟨(t₁, t₂), ht✝⟩
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
⊢ False

Tactic:
obtain ⟨a, ha⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.1

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs✝ : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
a✝¹ : ⟨(s₁, s₂), hs✝⟩ ∈ ↑P.parts.offDiag.attach
t₁ t₂ : Finset α
ht✝ : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
a✝ : ⟨(t₁, t₂), ht✝⟩ ∈ ↑P.parts.offDiag.attach
hst : ⟨(s₁, s₂), hs✝⟩ ≠ ⟨(t₁, t₂), ht✝⟩
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
a : α
ha : a ∈ (u, v).1
⊢ False
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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx : ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ G.nonuniformWitness ε U V → x ∉ x_1
B : Finset α
hB₁ : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts ∧ B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty
hB₂ : x ∈ B
⊢ ∃ a,
    (a ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧
      x ∈ a ∧ ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ a → x ∉ x_1

Tactic:
exact ⟨B, hB₁, hB₂, fun A hA AB => hx A hA <| AB.trans hB₁.2.1⟩

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

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x✝ ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts

Tactic:
simp [Set.image_union, map_adj, sup_adj, Relation.Map, or_and_right, exists_or]

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

Goal state before:
pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝¹ x✝ : W
⊢ (Subgraph.map f (H₁ ⊔ H₂)).Adj x✝¹ x✝ ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x✝¹ x✝

Tactic:
simp [Set.image_union, map_adj, sup_adj, Relation.Map, or_and_right, exists_or]

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
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty

Tactic:
rw [Subgraph.edgeSet_map]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' G'.edgeSet).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ (G.subgraphOfAdj ⋯).verts ⊆ H.verts

Tactic:
grind [subgraphOfAdj_verts, h.fst_mem, h.snd_mem]

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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2

Tactic:
← _root_.pow_succ,

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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ 2 ^ #P.parts = 2 ^ (#P.parts - 1 + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
⊢ G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe

Tactic:
by
  ext ⟨v, hv⟩ ⟨w, hw⟩
  simp only [SimpleGraph.deleteEdges_adj, coe_adj, deleteEdges_adj, Set.mem_image, not_exists,
    not_and, and_congr_right_iff]
  intro
  constructor
  · intro hs
    refine Sym2.ind ?_
    rintro ⟨v', hv'⟩ ⟨w', hw'⟩
    simp only [Sym2.map_mk, Sym2.eq]
    contrapose
    rintro (_ | _) <;> simpa only [Sym2.eq_swap]
  · intro h' hs
    exact h' _ hs rfl

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

Goal state before:
pp: case succ
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
n✝ : ℕ
hs : G.IsNClique (n✝ + 1) s
⊢ G.IsNClique (n✝ + 1) (insert a (s.erase b))

Tactic:
exact (hs.erase_of_mem hb).insert fun w h ↦ by aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) → G.IsNClique 3 s

Tactic:
rintro ⟨a, b, c, hab, hbc, hca, rfl⟩

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
a b c : α
hab : G.Adj a b
hbc : G.Adj a c
hca : G.Adj b c
⊢ G.IsNClique 3 {a, b, c}
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)
v w : Fin n
hn : ⊤.Adj v w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Tactic:
← f.topEmbedding.map_adj_iff,

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 : (completeMultipartiteGraph V).Adj (f.topEmbedding v) (f.topEmbedding w)
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v✝ : V
h✝ : G.Adj u v✝
q : G.Walk v✝ u
hq✝ : ∀ e ∈ (cons h✝ q).edges, e ∈ H.edgeSet
hq : s(u, v✝) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
qc : q.IsPath ∧ s(u, v✝) ∉ q.edges
⊢ (q.transfer H ⋯).IsPath ∧ s(u, v✝) ∉ q.edges

Tactic:
exact ⟨qc.1.transfer hq.2, qc.2⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
⊢ (q.transfer H hq).IsCycle

Tactic:
cases q with
  | nil => simp at qc
  | cons _ q =>
    simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
    simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
    exact ⟨qc.1.transfer hq.2, qc.2⟩

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 α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
      (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y})))
hε : 0 ≤ ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤ ε * (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y})))

Tactic:
refine Eq.trans_le ?_
    (mul_le_mul_of_nonneg_left (mul_le_mul hY hZ (by positivity) (by positivity)) hε)

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#({y ∈ t | G.Adj x y}))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#({y ∈ u | G.Adj x y}))
hY : ↑(#t) * ε ≤ ↑(#({y ∈ t | G.Adj x y}))
hZ : ↑(#u) * ε ≤ ↑(#({y ∈ u | G.Adj x y}))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) /
      (↑(#({y ∈ t | G.Adj x y})) * ↑(#({y ∈ u | G.Adj x y})))
hε : 0 ≤ ε
⊢ ε ^ 3 * ↑(#t) * ↑(#u) = ε * (↑(#t) * ε * (↑(#u) * ε))
Module: Mathlib.Combinatorics.Additive.Dissociation

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

Tactic:
prod_erase_eq_div hau,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
⊢ a = (∏ b ∈ t, b) / ((∏ x ∈ u, x) / a)
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:

Tactic:
(∑ x : σ → K, ∏ i, x i ^ d i) =
        ∑ x₀ : { j // j ≠ i } → K, ∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j :=
      (Fintype.sum_fiberwise _ _).symm
    _ = 0 := Fintype.sum_eq_zero _ ?_

Goal state after:
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
⊢ ∀ (a : { j // j ≠ i } → K), ∑ x, ∏ j, ↑x j ^ d j = 0
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_1
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
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∑ u ∈ ℬ, #u = m * n

Tactic:
sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1,

Goal state after:
case refine_1
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
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ #ℬ * n = m * n
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case hcd
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
⊢ #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t

Tactic:
exact card_biUnion_le

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬toColex s = toColex {a} ↔ ∀ b ∈ s, b < a

Tactic:
toColex_inj

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b

Tactic:
cons_le_cons

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
⊢ (∃ s, #s = r ∧ 𝒜 = initSeg s) → IsInitSeg 𝒜 r ∧ 𝒜.Nonempty

Tactic:
rintro ⟨s, rfl, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Fintype α
s : Finset α
⊢ IsInitSeg (initSeg s) #s ∧ (initSeg s).Nonempty
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial
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)
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
have : Nontrivial L := ⟨⟨l₁, l₂, hl⟩⟩

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
⊢ ∃ p ∈ l₁, p ∈ l₂
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
⊢ z ∈ A * A

Tactic:
let l : Finset G := A ∩ ((z * a⁻¹) • (A⁻¹ * A))

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)
⊢ z ∈ A * A
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: n : ℕ
ijh : ↥(antidiagonal n)
⊢ (↑ijh).2 < n + 1

Tactic:
have := snd_le ijh.2

Goal state after:
n : ℕ
ijh : ↥(antidiagonal n)
this : (↑ijh).2 ≤ n
⊢ (↑ijh).2 < n + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take (min 1 j) ↑p) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take (min 1 j) ↑p) + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
min_eq_left (by lia),

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D (List.take 1 ↑p) + count D (List.drop 1 (List.take j ↑p)) <
    count U (List.take 1 ↑p) + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.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✝ : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ (f + g) * h = f * h + g * h

Tactic:
by
    ext; exact Eq.trans (sum_congr rfl fun x _ ↦ right_distrib _ _ _) sum_add_distrib

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

Goal state before:
pp: case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0

Tactic:
insidePart_zero,

Goal state after:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
insidePart_zero,

Goal state after:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0 ∨ m = outsidePart 0
⊢ p.semilength ≤ semilength 0