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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m : ℕ
hm : 3 ≤ m
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ k ^ (m - 2) * ↑(#A)

Tactic:
induction m, hm using Nat.le_induction with
  | base => simpa using h ε hε
  | succ m hm ih =>
    obtain _ | m := m
    · simp at hm
    have hm₀ : m ≠ 0 := by simp at hm; positivity
    have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
    obtain rfl | hA := A.eq_empty_or_nonempty
    · simp [hε₀]
    have hk : 0 ≤ k :=
      nonneg_of_mul_nonneg_left ((h 1 (by simp)).trans' (by positivity)) (by positivity)
    let π {n} (δ : Fin n → ℤ) : Finset G := ((finRange _).map fun i ↦ A ^ δ i).prod
    let V : Finset G := π ![-ε 1, -ε 0]
    let W : Finset G := π <| tail <| tail ε
    refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)
    calc
      (#A * #(π ε) : ℝ)
        = #A * #(V⁻¹ * W) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def, mul_assoc]
      _ ≤ #(A * V) * #(A * W) := by norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul ..
      _ = #(π ![1, -ε 1, -ε 0]) * #(π <| Fin.cons 1 <| tail <| tail ε) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def]
      _ ≤ (k * #A) * (k ^ (m - 1) * #A) := by
        gcongr
        · exact h ![1, -ε 1, -ε 0] fun i ↦ by fin_cases i <;> simp [hε]
        · exact ih (Fin.cons 1 <| tail <| tail ε) <| Fin.cons (by simp) (by simp [hε, Fin.tail])
      _ = #A * (k ^ m * #A) := by rw [← pow_sub_one_mul hm₀]; ring

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
w : V
⊢ w ≠ v ∧ Odd (G.degree w) ↔ Odd (G.degree w) ∧ w ≠ v

Tactic:
rw [and_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
rw [hg]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < 2 * k + 1
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
⊢ (∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1

Tactic:
Nat.le_and_le_add_one_iff

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1) ↔
    ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1

Tactic:
Nat.le_and_le_add_one_iff

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
H : SimpleGraph V
inst✝ : Fintype ↑(H.neighborSet v)
hle : G ≤ H
⊢ G.degree v ≤ H.degree v

Tactic:
by
  simp_rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card fun v hv => hle hv

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #s / #P.parts ≤ #t

Tactic:
by
  rw [← P.sum_card_parts]
  exact Finset.EquitableOn.le hP ht

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : ↥({p ∈ P.parts | #p = #s / #P.parts + 1}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1}) :=
  {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
mem_filter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1})
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
mem_filter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts})
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
⊢ (P.parts.preimage Subtype.val ⋯).sup id = ⟨s, hs⟩

Tactic:
simpa [Finset.sup_preimage_val_id Prsup Prbot hP] using P.sup_parts

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

Goal state before:
pp: case bc
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := ⋯
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts
⊢ ↑(g (f a).fst) < #P.parts

Tactic:
exact gl a

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Tactic:
obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
r : Set α
hrs : r ⊆ ↑s
hr : Set.BijOn P.part r ↑P.parts
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 < 4 ^ initialBound ε l * ε ^ 5

Tactic:
rw [← rpow_natCast 4, ← div_lt_iff₀ (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ←
    div_lt_iff₀, initialBound, Nat.cast_max, Nat.cast_max]

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ (∃ i ∈ x, a ∈ x ∧ s i a) ↔ a ∈ x

Tactic:
refine ⟨(·.choose_spec.2.1), fun _ ↦ by use a⟩

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

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
obtain hscard | hscard := ((#s).cast_nonneg : (0 : 𝕜) ≤ #s).eq_or_lt

Goal state after:
case inl
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 = ↑(#s)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} → ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x

Tactic:
mem_filter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ (atomise s F).parts ∧ x ⊆ t ∧ x.Nonempty → ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
⊢ x ∈ {e ∈ s ×ˢ t | r e.1 e.2} ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2

Tactic:
mem_filter,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
⊢ x ∈ s ×ˢ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
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 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

Tactic:
mul_one

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) ≤ ↑(#s')
ht : ↑(#t) ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
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 - δ ≤ ↑(#t₂) / ↑(#t₁)

Tactic:
refine (le_div_iff₀ ?_).2 ht₂

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
⊢ 0 < ↑(#t₁)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
⊢ (u, v) ∈
      {x ∈ P.parts.offDiag |
        match x with
        | (u, v) => ↑(G.edgeDensity u v) < ε} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε

Tactic:
mem_filter,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
⊢ ((u, v) ∈ P.parts.offDiag ∧
      match (u, v) with
      | (u, v) => ↑(G.edgeDensity u v) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ (u, v) ∈
      {x ∈ P.parts.offDiag |
        match x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v

Tactic:
mem_filter,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ ((u, v) ∈ P.parts.offDiag ∧
      match (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
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
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts - #P.parts * 1

Tactic:
mul_one

Goal state after:
α : 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
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts - #P.parts
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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ ↑(#A) * (2 * ↑(#A)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
rw [mul_left_comm, ← sq]

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)
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 ε
⊢ #(increment hP G ε).parts = stepBound #P.parts

Tactic:
by
  have hPα' : stepBound #P.parts ≤ card α := by grw [← hPα, stepBound]; gcongr; simp
  have hPpos : 0 < stepBound #P.parts := stepBound_pos (nonempty_of_not_uniform hPG).card_pos
  rw [increment, card_bind]
  simp_rw [chunk, apply_dite Finpartition.parts, apply_dite card, sum_dite]
  rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]
  any_goals exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'
  rw [Nat.sub_add_cancel a_add_one_le_four_pow_parts_card,
    Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), ← add_mul]
  congr
  rw [card_filter_add_card_filter_not, card_attach]

Goal state after:
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
ε : ℝ
⊢ (↑P.parts.offDiag.attach).PairwiseDisjoint (distinctPairs hP G ε)

Tactic:
by
  simp +unfoldPartialApp only [distinctPairs, Set.PairwiseDisjoint,
    Function.onFun, Finset.disjoint_left, mem_product]
  rintro ⟨⟨s₁, s₂⟩, hs⟩ _ ⟨⟨t₁, t₂⟩, ht⟩ _ hst ⟨u, v⟩ huv₁ huv₂
  rw [mem_offDiag] at hs ht
  obtain ⟨a, ha⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.1
  obtain ⟨b, hb⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.2
  exact hst <| Subtype.ext <| Prod.ext
    (P.disjoint.elim_finset hs.1 ht.1 a (Finpartition.le _ huv₁.1 ha) <|
      Finpartition.le _ huv₂.1 ha) <|
        P.disjoint.elim_finset hs.2.1 ht.2.1 b (Finpartition.le _ huv₁.2 hb) <|
          Finpartition.le _ huv₂.2 hb

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      (↑(#P.parts) ^ 2 * (4 ^ #P.parts) ^ 2)

Tactic:
pow_right_comm,

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      (↑(#P.parts) ^ 2 * (4 ^ 2) ^ #P.parts)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case neg.refine_3
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑i + ε ^ 5 / 4 * 1 ≤ ↑(P.energy G) + ε ^ 5 / 4

Tactic:
mul_one

Goal state after:
case neg.refine_3
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑i + ε ^ 5 / 4 ≤ ↑(P.energy G) + ε ^ 5 / 4
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
⊢ 1 ≤ (2 ^ #P.parts) ^ 2 * (ε ^ 2) ^ 2 / 10 ^ 2

Tactic:
pow_right_comm,

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
⊢ 1 ≤ (2 ^ 2) ^ #P.parts * (ε ^ 2) ^ 2 / 10 ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
⊢ H = G.singletonSubgraph v ↔ H.verts = {v}

Tactic:
by
  refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩
  ext
  · rw [h, singletonSubgraph_verts]
  · simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]
    intro ha
    have ha1 := ha.fst_mem
    have ha2 := ha.snd_mem
    rw [h, Set.mem_singleton_iff] at ha1 ha2
    subst_vars
    exact ha.ne rfl

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
ha : G.Adj s t
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
by
  have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
  rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff_of_subset (by simp [ha]),
    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
    ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]
  congr 2
  rw [card_image_of_injective, card_neighborFinset_eq_degree]
  unfold Function.Injective
  aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s

Tactic:
ext <;> simp +contextual

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s

Tactic:
ext <;> simp +contextual

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s

Tactic:
ext <;> simp +contextual

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 - ε ^ 5 / 50 ≤ 1 - 2 * 1 * (1 / (↑m + 1)) + (1 / (↑m + 1)) ^ 2

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 - ε ^ 5 / 50 ≤ 1 - 2 * (1 / (↑m + 1)) + (1 / (↑m + 1)) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
⊢ (q₂.append ((q₁.append p₁).append r₁)).append r₂ = ((q₂.append q₁).append p₁).append (r₁.append r₂)

Tactic:
simp [append_assoc]

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsTrail → p.IsTrail

Tactic:
intro h
      convert! h.reverse _
      try rw [reverse_reverse]

Goal state after: