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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tmc : G.IsMaximumIndepSet t
⊢ #t = G.indepNum

Tactic:
rw [← isMaximumClique_compl] at tmc
  simp_rw [indepNum, ← isNClique_compl]
  exact Gᶜ.maximumClique_card_eq_cliqueNum t tmc

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
⊢ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49

Tactic:
by
  have : (↑1 + ε ^ 5 / ↑49) * G.edgeDensity (A.biUnion id) (B.biUnion id) ≤
      G.edgeDensity (A.biUnion id) (B.biUnion id) + ε ^ 5 / 49 := by
    rw [add_mul, one_mul, add_le_add_iff_left]
    refine mul_le_of_le_one_right (by sz_positivity) ?_
    exact mod_cast G.edgeDensity_le_one _ _
  refine le_trans ?_ this
  conv_lhs => -- Porting note: LHS and RHS need separate treatment to get the desired form
    simp only [SimpleGraph.edgeDensity, edgeDensity, sum_div, Rat.cast_div, div_div]
  conv_rhs =>
    rw [SimpleGraph.edgeDensity, edgeDensity, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl)]
    simp only [cast_sum, mul_sum, sum_div, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) + _)]
  push_cast
  apply sum_le_sum
  simp only [and_imp, Prod.forall, mem_product, show A.product B = A ×ˢ B by rfl]
  intro x y hx hy
  rw [mul_mul_mul_comm, mul_comm (#x : ℝ), mul_comm (#y : ℝ), div_le_iff₀, mul_assoc]
  · refine le_mul_of_one_le_right (cast_nonneg _) ?_
    rw [div_mul_eq_mul_div, one_le_div]
    · refine le_trans ?_ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) ?_)
      · rw [sq, mul_mul_mul_comm, mul_comm (_ / (m : ℝ)), mul_comm (_ / (m : ℝ))]
        gcongr
        exacts [sum_card_subset_chunk_parts_le (by sz_positivity) hA hx,
          sum_card_subset_chunk_parts_le (by sz_positivity) hB hy]
      · exact_mod_cast _root_.zero_le
    rw [← cast_mul, cast_pos]
    apply mul_pos <;> rw [Finset.card_pos, sup_eq_biUnion, biUnion_nonempty]
    · exact ⟨_, hx, nonempty_of_mem_parts _ (hA hx)⟩
    · exact ⟨_, hy, nonempty_of_mem_parts _ (hB hy)⟩
  refine mul_pos (mul_pos ?_ ?_) (mul_pos ?_ ?_) <;> rw [cast_pos, Finset.card_pos]
  exacts [⟨_, hx⟩, nonempty_of_mem_parts _ (hA hx), ⟨_, hy⟩, nonempty_of_mem_parts _ (hB hy)]

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

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < 2 * k * (n / k)

Tactic:
mul_assoc,

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < 2 * (k * (n / k))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case hbc
α : 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)
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
exact card_bound hP₁ hP₃ ‹_›

Goal state after:
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
ε : ℝ
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)
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#Y)

Tactic:
exact card_bound hP₁ hP₃ ‹_›

Goal state after:
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
ε : ℝ
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)
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#Z)

Tactic:
exact card_bound hP₁ hP₃ ‹_›

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
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}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) ≤ 2 * ε * ↑(#s)

Tactic:
mul_assoc,

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}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) ≤ 2 * (ε * ↑(#s))
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * (1 - (↑m)⁻¹) * (↑(#(G.nonuniformWitness ε U V)) / ↑(#U)) =
    (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U))

Tactic:
mul_assoc,

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * ((1 - (↑m)⁻¹) * (↑(#(G.nonuniformWitness ε U V)) / ↑(#U))) =
    (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U))
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * ((1 - (↑m)⁻¹) * (↑(#(G.nonuniformWitness ε U V)) / ↑(#U))) =
    (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U))

Tactic:
mul_assoc,

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * ((1 - (↑m)⁻¹) * (↑(#(G.nonuniformWitness ε U V)) / ↑(#U))) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U)))
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) * (↑m + 1) * ((1 - (↑m)⁻¹) / (4 ^ #P.parts * ↑m)) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
mul_assoc,

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) * ((↑m + 1) * ((1 - (↑m)⁻¹) / (4 ^ #P.parts * ↑m))) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
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 (α × α) := ⋯
⊢ ↑(#C) ≤ 4 * (ε / 4) * ↑(Fintype.card α) ^ 2

Tactic:
· exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)

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

Goal state before:

Tactic:
4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      linarith

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
⊢ 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
by
  have hm : (0 : ℝ) ≤ 1 - (↑m)⁻¹ := sub_nonneg_of_le (inv_le_one_of_one_le₀ <| one_le_m_coe hPα)
  have hε : 0 ≤ 1 - ε / 10 :=
    sub_nonneg_of_le (div_le_one_of_le₀ (hε₁.trans <| by simp) <| by norm_num)
  have hε₀ : 0 < ε := by sz_positivity
  calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      linarith

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

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

Tactic:
mul_assoc,

Goal state after:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 * (2 ^ k * n)).bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices
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
⊢ 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t

Tactic:
mul_assoc,

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
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
⊢ 2 * (m * n) - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t : Colex (Finset α)
⊢ s ≤ t ↔ ↑(ofColex s) \ ↑(ofColex t) ⊆ ↑(lowerClosure (↑(ofColex t) \ ↑(ofColex s)))

Tactic:
simp [le_def, Set.subset_def, and_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ \ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ \ 𝒜₁
⊢ False

Tactic:
rw [mem_sdiff] at hs ht

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
⊢ False
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
rw [x_vs_a, swap_apply_right]
        apply Option.some_ne_none

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) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z = x⁻¹ * y * w

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z = x⁻¹ * (y * w)
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.Nonempty

Tactic:
by_contra! rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
h : ↑(#(∅ * ∅)) < 3 / 2 * ↑(#∅)
⊢ False
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ Projectivization.mk K c hc = Projectivization.mk K d hd

Tactic:
mk_eq_mk_iff_crossProduct_eq_zero

Goal state after:
case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ ((∑ k ∈ m.toFinset, k * count k m)! *
          ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        (map (fun j ↦ j !) m).prod *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
mul_assoc,

Goal state after:
m : Multiset ℕ
⊢ ((∑ k ∈ m.toFinset, k * count k m)! *
        ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ ((∑ k ∈ m.toFinset, k * count k m)! *
        ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
mul_assoc,

Goal state after:
m : Multiset ℕ
⊢ (∑ k ∈ m.toFinset, k * count k m)! *
      ((∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
mul_assoc,

Goal state after:
case e_a
m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod *
      ((∏ j ∈ m.toFinset.erase 0, (count j m)!) *
        ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) =
    ∏ i ∈ m.toFinset, (i * count i m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case e_val
p q a b : DyckWord
h : a + b = 0
neg_val✝ : b + a = 0
ha : ↑a = []
hb : ↑b = []
⊢ a = 0

pp: case e_neg
p q a b : DyckWord
h : a + b = 0
neg_val✝ : b + a = 0
ha : ↑a = []
hb : ↑b = []
⊢ b = 0

Tactic:
· exact toList_eq_nil.mp ha

Goal state after:
case e_neg
p q a b : DyckWord
h : a + b = 0
neg_val✝ : b + a = 0
ha : ↑a = []
hb : ↑b = []
⊢ b = 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑(A.invMulSubgroup h) * ↑A * ↑A⁻¹ = ↑A⁻¹ * ↑A

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑(A.invMulSubgroup h) * (↑A * ↑A⁻¹) = ↑A⁻¹ * ↑A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * (↑A * ↑A⁻¹ * ↑A) = ↑A * ↑A⁻¹

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * (↑A * (↑A⁻¹ * ↑A)) = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:

Tactic:
_ = ∑ x ∈ Icc a b, mu' 𝕜 x b := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu'_left ..

Goal state after: