mathlib-initiative/mathlib-tactics huggingface dataset:
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 * 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:
]

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 * 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 α := 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 ≤ ε
hX' : (1 - 2 * ε) * ↑(#s) ≤ ↑(#X')
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) = (1 - 2 * ε) * ↑(#s) * (ε ^ 3 * ↑(#t) * ↑(#u))

Tactic:
by ring

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ ε / 4 ≤ ↑(G.edgeDensity s Z)

Tactic:
]

Goal state after:
α : 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)
⊢ ε / 4 ≤ ↑(G.edgeDensity s Z)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : 0 ≤ 1 - 2 * (ε / 8)
⊢ ε / 4 ≤ ↑(G.edgeDensity Y Z)

Tactic:
]

Goal state after:
α : 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)
⊢ ε / 4 ≤ ↑(G.edgeDensity Y Z)
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)) ≤ ↑(#s) * ε + ↑(#s) * ε

Tactic:
]

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)) ≤ ↑(#s) * ε + ↑(#s) * ε
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)) ≤ ↑(#s) * ε + ↑(#s) * ε

Tactic:
]

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)) ≤ ↑(#s) * ε + ↑(#s) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#{x | G.Adj x.1 x.2}) - ↑(#{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})

pp: α : 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 (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ {x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2} ⊆ {x | G.Adj x.1 x.2}

Tactic:
]

Goal state after:
α : 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 (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#{x | G.Adj x.1 x.2}) - ↑(#{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})

α : 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 (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ {x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2} ⊆ {x | G.Adj x.1 x.2}
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}
a : α
a✝¹ : a ∈ ↑X'
b : α
a✝ : b ∈ ↑X'
t : a ≠ b
⊢ ∀ ⦃a_1 : α × α × α⦄,
    a_1 ∈ image (fun x ↦ (a, x)) (G.interedges ({y ∈ t✝ | G.Adj a y}) ({y ∈ u | G.Adj a y})) →
      a_1 ∉ image (fun x ↦ (b, x)) (G.interedges ({y ∈ t✝ | G.Adj b y}) ({y ∈ u | G.Adj b y}))

Tactic:
]

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}
a : α
a✝¹ : a ∈ ↑X'
b : α
a✝ : b ∈ ↑X'
t : a ≠ b
⊢ ∀ ⦃a_1 : α × α × α⦄,
    a_1 ∈ image (fun x ↦ (a, x)) (G.interedges ({y ∈ t✝ | G.Adj a y}) ({y ∈ u | G.Adj a y})) →
      a_1 ∉ image (fun x ↦ (b, x)) (G.interedges ({y ∈ t✝ | G.Adj b y}) ({y ∈ u | G.Adj b y}))
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) * (↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U))) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U)))

Tactic:
]

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 α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ #({x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ #({x ∈ s ×ˢ t ×ˢ u |
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ Int.subNatNat
      (#{x |
          match x with
          | (x, y) => G.Adj x y})
      (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (#{x | G.Adj x.1 x.2}) #{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}

Tactic:
two_mul_card_edgeFinset

Goal state after:
α : 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 (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ Int.subNatNat
      (#{x |
          match x with
          | (x, y) => G.Adj x y})
      #{x |
          match x with
          | (x, y) => (regularityReduced P G (ε / 8) (ε / 4)).Adj x y} =
    Int.subNatNat (#{x | G.Adj x.1 x.2}) #{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ Int.subNatNat
      (#{x |
          match x with
          | (x, y) => G.Adj x y})
      #{x |
          match x with
          | (x, y) => (regularityReduced P G (ε / 8) (ε / 4)).Adj x y} =
    Int.subNatNat (#{x | G.Adj x.1 x.2}) #{x | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}

Tactic:
]

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

Tactic:
]

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)) / 4 ^ #P.parts * ((↑m + 1) * ((1 - (↑m)⁻¹) / ↑m)) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x ↦
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x ↦
    match x with
    | (U, V) => G.interedges U V
⊢ 4 * (ε / 8) * ↑(Fintype.card α) ^ 2 + ↑(#B) + ↑(#C) ≤
    ?m.336 + ε / 2 * ↑(Fintype.card α) ^ 2 + 4 * (ε / 4) * ↑(Fintype.card α) ^ 2

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

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
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (↑m - 1) ≤ ↑m * ↑m

Tactic:
]

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 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (↑m - 1) ≤ ↑m * ↑m
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : IsEmpty α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
· simp [Fintype.card_eq_zero]

Goal state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : ∃ a b c, (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
⊢ ∃ x ∈ t, toTriangle x = s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : ∃ a b c, (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
⊢ ∃ x ∈ t, toTriangle x = s
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ False