awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
⊢ triangleRemovalBound ε ≤
    (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3

Tactic:
exact triangleRemovalBound_le hε₁

Premises used: SimpleGraph.triangleRemovalBound_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
⊢ (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3 *
      HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 =
    (1 - 2 * (ε / 8)) * HPow.hPow (β := ℕ) (ε / 8) 3 *
          ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
        ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
      ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ))

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
h₁ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
h₂ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Y) : ℝ)
h₃ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Z) : ℝ)
⊢ (1 - 2 * (ε / 8)) * HPow.hPow (β := ℕ) (ε / 8) 3 *
          ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
        ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
      ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) ≤
    (1 - 2 * (ε / 8)) * HPow.hPow (β := ℕ) (ε / 8) 3 * (↑(#s) : ℝ) * (↑(#Y) : ℝ) * (↑(#Z) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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 α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)

Tactic:
card_bound hP₁ hP₃ ‹_›

Premises used: _private.0.SimpleGraph.card_bound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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 α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)

Tactic:
exact card_bound hP₁ hP₃ ‹_›

Premises used: _private.0.SimpleGraph.card_bound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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 α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Y) : ℝ)

Tactic:
card_bound hP₁ hP₃ ‹_›

Premises used: _private.0.SimpleGraph.card_bound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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 α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Y) : ℝ)

Tactic:
exact card_bound hP₁ hP₃ ‹_›

Premises used: _private.0.SimpleGraph.card_bound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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 α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Z) : ℝ)

Tactic:
card_bound hP₁ hP₃ ‹_›

Premises used: _private.0.SimpleGraph.card_bound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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 α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Z) : ℝ)

Tactic:
exact card_bound hP₁ hP₃ ‹_›

Premises used: _private.0.SimpleGraph.card_bound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
rwa rwa₁ rwa₂ rwa₃ : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
⊢ 2 * (ε / 8) ≤ (↑(G.edgeDensity s Y) : ℝ)

Tactic:
rwa [that]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
rwa rwa₁ rwa₂ rwa₃ : ε / 4 ≤ (↑(G.edgeDensity s Z) : ℝ)
⊢ 2 * (ε / 8) ≤ (↑(G.edgeDensity s Z) : ℝ)

Tactic:
rwa [that]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
rwa rwa₁ rwa₂ rwa₃ : ε / 4 ≤ (↑(G.edgeDensity Y Z) : ℝ)
⊢ 2 * (ε / 8) ≤ (↑(G.edgeDensity Y Z) : ℝ)

Tactic:
rwa [that]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) 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_1 : ε / 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_1 : ε / 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_1 : ε / 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)
_ :
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
    (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3 *
      HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
_₁ :
  (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3 *
      HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 =
    (1 - 2 * (ε / 8)) * HPow.hPow (β := ℕ) (ε / 8) 3 *
          ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
        ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
      ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ))
_₂ :
  (1 - 2 * (ε / 8)) * HPow.hPow (β := ℕ) (ε / 8) 3 *
          ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
        ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) *
      ((↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) ≤
    (1 - 2 * (ε / 8)) * HPow.hPow (β := ℕ) (ε / 8) 3 * (↑(#s) : ℝ) * (↑(#Y) : ℝ) * (↑(#Z) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
calc
    _ ≤ (1 - ε / 4) * (ε / (16 * bound (ε / 8) ⌈4 / ε⌉₊)) ^ 3 * card α ^ 3 := by
      gcongr; exact triangleRemovalBound_le hε₁
    _ = (1 - 2 * (ε / 8)) * (ε / 8) ^ 3 * (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) *
          (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) * (card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊)) := by
      ring
    _ ≤ (1 - 2 * (ε / 8)) * (ε / 8) ^ 3 * #s * #Y * #Z := by
      gcongr <;> exact card_bound hP₁ hP₃ ‹_›
    _ ≤ _ :=
      triangle_counting G (by rwa [that]) uXY dXY (by rwa [that]) uXZ dXZ (by rwa [that]) uYZ dYZ

Premises used: SzemerediRegularity.bound, HMul.hMul, HSub.hSub, Fintype.card, HDiv.hDiv, Nat.cast, Nat.ceil, OfNat.ofNat, SimpleGraph.triangle_counting
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_3 : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ (↑(#P.parts) : ℝ)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => G.interedges U V
rw :
  HMul.hMul (α := ℝ) 2 (↑(#G.edgeFinset) : ℝ) -
      HMul.hMul (α := ℝ) 2 (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    HSub.hSub (α := ℝ) (↑(Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2}) : ℝ)
      (↑(Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}) : ℝ)
rw₁ :
  Subset.{u_1} (α := Finset (α × α)) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}
    {x : α × α | G.Adj x.1 x.2}
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    (↑(#({x ∈ SProd.sprod (α := Finset α) (β := Finset α) univ univ |
            match (motive := α × α → Prop) x with
            | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y})) :
      ℝ)

Tactic:
rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]

Premises used: mul_sub, Finset.filter_and_not, Finset.univ_product_univ, Finset.cast_card_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_3 : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ (↑(#P.parts) : ℝ)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => G.interedges U V
norm_cast :
  Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
⊢ HMul.hMul (α := ℝ) 2 (↑(#G.edgeFinset) : ℝ) -
      HMul.hMul (α := ℝ) 2 (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    HSub.hSub (α := ℝ) (↑(Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2}) : ℝ)
      (↑(Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_3 : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ (↑(#P.parts) : ℝ)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => G.interedges U V
rw :
  Int.subNatNat
      (Finset.card.{u_1} (α := α × α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (x, y) => G.Adj x y})
      (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
rw₁ rw₂ :
  Int.subNatNat
      (Finset.card.{u_1} (α := α × α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (x, y) => G.Adj x y})
      (Finset.card.{u_1} (α := α × α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (x, y) => (regularityReduced P G (ε / 8) (ε / 4)).Adj x y}) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
⊢ Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})

Tactic:
rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]

Premises used: SimpleGraph.two_mul_card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_3 : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ (↑(#P.parts) : ℝ)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => G.interedges U V
h :
  ∀ (xy : α × α),
    Membership.mem (γ := Finset (α × α)) univ xy →
      (regularityReduced P G (ε / 8) (ε / 4)).Adj xy.1 xy.2 → G.Adj xy.1 xy.2
⊢ Subset.{u_1} (α := Finset (α × α)) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}
    {x : α × α | G.Adj x.1 x.2}

Tactic:
gcongr with xy _
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
inst_3 : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ (↑(#P.parts) : ℝ)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
    match (motive := Finset α × Finset α → Finset (α × α)) x with
    | (U, V) => G.interedges U V
xy : α × α
h : Membership.mem (γ := Finset (α × α)) univ xy
⊢ (regularityReduced P G (ε / 8) (ε / 4)).Adj xy.1 xy.2 → G.Adj xy.1 xy.2

Tactic:
fun hxy ↦ regularityReduced_le hxy

Premises used: SimpleGraph.regularityReduced_le