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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
Y' : Finset α
hY' : Y' ∈ P.parts
Z' : Finset α
hZ' : Z' ∈ P.parts
yY' : y ∈ Y'
zZ' : z ∈ Z'
nYZ : Y' ≠ Z'
uYZ : G.IsUniform (ε / 8) Y' Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y' Z') : ℝ)
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ : ε / 4 ≤ (↑(G.edgeDensity s Z) : ℝ)
⊢ Y ∈ P.parts

Tactic:
cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
Y' : Finset α
hY' : Y' ∈ P.parts
Z' : Finset α
hZ' : Z' ∈ P.parts
yY' : y ∈ Y'
zZ' : z ∈ Z'
nYZ : Y' ≠ Z'
uYZ : G.IsUniform (ε / 8) Y' Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y' 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
⊢ y ∈ Y

Tactic:
cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
Y' : Finset α
hY' : Y' ∈ P.parts
Z' : Finset α
hZ' : Z' ∈ P.parts
yY' : y ∈ Y'
zZ' : z ∈ Z'
nYZ : Y' ≠ Z'
uYZ : G.IsUniform (ε / 8) Y' Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y' 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
⊢ Y ≠ Z'

Tactic:
cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
Y' : Finset α
hY' : Y' ∈ P.parts
Z' : Finset α
hZ' : Z' ∈ P.parts
yY' : y ∈ Y'
zZ' : z ∈ Z'
nYZ : Y' ≠ Z'
uYZ : G.IsUniform (ε / 8) Y' Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y' 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
nYZ₁ : Y ≠ Z'
⊢ G.IsUniform (ε / 8) Y Z'

Tactic:
cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
Y' : Finset α
hY' : Y' ∈ P.parts
Z' : Finset α
hZ' : Z' ∈ P.parts
yY' : y ∈ Y'
zZ' : z ∈ Z'
nYZ : Y' ≠ Z'
uYZ : G.IsUniform (ε / 8) Y' Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y' 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
nYZ₁ : Y ≠ Z'
uYZ₁ : G.IsUniform (ε / 8) Y Z'
⊢ ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)

Tactic:
cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
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
nYZ : Y ≠ Z'
uYZ : G.IsUniform (ε / 8) Y Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)
⊢ Z ∈ P.parts

Tactic:
cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
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
nYZ : Y ≠ Z'
uYZ : G.IsUniform (ε / 8) Y Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)
hZ'₁ : Z ∈ P.parts
⊢ z ∈ Z

Tactic:
cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
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
nYZ : Y ≠ Z'
uYZ : G.IsUniform (ε / 8) Y Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)
hZ'₁ : Z ∈ P.parts
zZ'₁ : z ∈ Z
⊢ Y ≠ Z

Tactic:
cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
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
nYZ : Y ≠ Z'
uYZ : G.IsUniform (ε / 8) Y Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)
hZ'₁ : Z ∈ P.parts
zZ'₁ : z ∈ Z
nYZ₁ : Y ≠ Z
⊢ G.IsUniform (ε / 8) Y Z

Tactic:
cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 4 ≤ (↑(G.edgeDensity s Y) : ℝ)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
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
nYZ : Y ≠ Z'
uYZ : G.IsUniform (ε / 8) Y Z'
dYZ : ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)
hZ'₁ : Z ∈ P.parts
zZ'₁ : z ∈ Z
nYZ₁ : Y ≠ Z
uYZ₁ : G.IsUniform (ε / 8) Y Z
⊢ ε / 4 ≤ (↑(G.edgeDensity Y Z) : ℝ)

Tactic:
cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- 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 : ε / 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) : ℝ)
⊢ Function.onFun Disjoint id s Y

Tactic:
have dXY := P.disjoint hX hY nXY
-- 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 : ε / 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
⊢ Function.onFun Disjoint id s Z

Tactic:
have dXZ := P.disjoint hX hZ nXZ
-- 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 : ε / 4 ≤ (↑(G.edgeDensity Y Z) : ℝ)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
⊢ Function.onFun Disjoint id Y Z

Tactic:
have dYZ := P.disjoint hY hZ nYZ
-- 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
⊢ 2 * (ε / 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
⊢ 2 * (ε / 8) = ε / 4

Tactic:
have that : 2 * (ε / 8) = ε / 4 := by 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
⊢ LE.le (α := ℝ) (↑(G.edgeDensity Y Z) : ℝ) 1

Tactic:
mod_cast G.edgeDensity_le_one _ _

Premises used: SimpleGraph.edgeDensity_le_one, congrArg, SimpleGraph.edgeDensity, cast, Rat.cast, LE.le, Rat.cast_le_natCast._simp_1, Eq.symm, Nat.cast_one, Eq.trans
-- 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
⊢ LE.le (α := ℝ) (↑(G.edgeDensity Y Z) : ℝ) 1

Tactic:
exact mod_cast G.edgeDensity_le_one _ _

Premises used: SimpleGraph.edgeDensity_le_one
-- 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
⊢ ε / 4 ≤ 1

Tactic:
have : ε / 4 ≤ 1 := ‹ε / 4 ≤ _›.trans (by exact mod_cast G.edgeDensity_le_one _ _)
-- 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 : ε / 4 ≤ 1
linarith : 1 - 2 * (ε / 8) < 0 → 8 / 8 = 1
linarith₁ linarith₂ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 8 0
linarith₄ : 1 - 2 * (ε / 8) < 0 → 4 / 4 = 1
linarith₅ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 4 0
linarith₇ : 1 - 2 * (ε / 8) < 0 → 8 / 8 = 1
linarith₈ linarith₉ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₁₀ : 1 - 2 * (ε / 8) < 0 → 4 / 4 = 1
linarith₁₁ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₁₂ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 8 0
linarith₁₃ : 1 - 2 * (ε / 8) < 0 → 4 / 4 = 1
linarith₁₄ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₅ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 4 0
linarith₁₆ : 1 - 2 * (ε / 8) < 0 → 4 / 4 = 1
linarith₁₇ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₈ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 4 0
linarith₁₉ : 1 - 2 * (ε / 8) < 0 → 4 / 4 = 1
linarith₂₀ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂₁ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 4 0
linarith₂₂ :
  1 - 2 * (ε / 8) < 0 →
    HMul.hMul (α := ℝ) 6 (-1) + 2 * (ε - 1) +
        (HMul.hMul (α := ℝ) 8 1 - HMul.hMul (α := ℝ) 1 2 * (1 * ε) - HMul.hMul (α := ℝ) 8 0) =
      0
linarith₂₃ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 6 0
linarith₂₄ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 - 2 * (ε / 8)

Tactic:
linarith
-- 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
⊢ 0 ≤ 1 - 2 * (ε / 8)

Tactic:
have : 0 ≤ 1 - 2 * (ε / 8) := by
    have : ε / 4 ≤ 1 := ‹ε / 4 ≤ _›.trans (by exact mod_cast G.edgeDensity_le_one _ _); linarith
-- 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)
hbc :
  triangleRemovalBound ε ≤
    (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
    (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3 *
      HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3

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)
⊢ triangleRemovalBound ε ≤
    (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3

Tactic:
triangleRemovalBound_le hε₁

Premises used: SimpleGraph.triangleRemovalBound_le