awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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) : ℝ)
X' : Finset α
hX' : X' ∈ P.parts
Z : Finset α
hZ : Z ∈ P.parts
xX' : x ∈ X'
zZ : z ∈ Z
nXZ : X' ≠ Z
uXZ : G.IsUniform (ε / 8) X' Z
dXZ : ε / 4 ≤ (↑(G.edgeDensity X' 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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have nXZ₁ : s ≠ Z
Tactic: cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)
Cleared hypotheses: X', hX', xX', nXZ, uXZ, dXZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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) : ℝ)
X' : Finset α
hX' : X' ∈ P.parts
Z : Finset α
hZ : Z ∈ P.parts
xX' : x ∈ X'
zZ : z ∈ Z
nXZ : X' ≠ Z
uXZ : G.IsUniform (ε / 8) X' Z
dXZ : ε / 4 ≤ (↑(G.edgeDensity X' 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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have uXZ₁ : G.IsUniform (ε / 8) s Z
Tactic: cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)
Cleared hypotheses: X', hX', xX', nXZ, uXZ, dXZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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) : ℝ)
X' : Finset α
hX' : X' ∈ P.parts
Z : Finset α
hZ : Z ∈ P.parts
xX' : x ∈ X'
zZ : z ∈ Z
nXZ : X' ≠ Z
uXZ : G.IsUniform (ε / 8) X' Z
dXZ : ε / 4 ≤ (↑(G.edgeDensity X' 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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have dXZ₁ : ε / 4 ≤ (↑(G.edgeDensity s Z) : ℝ)
Tactic: cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)
Cleared hypotheses: X', hX', xX', nXZ, uXZ, dXZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have nYZ₁ : Y ≠ Z'
Tactic: cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)
Cleared hypotheses: Y', hY', yY', nYZ, uYZ, dYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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'
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have uYZ₁ : G.IsUniform (ε / 8) Y Z'
Tactic: cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)
Cleared hypotheses: Y', hY', yY', nYZ, uYZ, dYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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'
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have dYZ₁ : ε / 4 ≤ (↑(G.edgeDensity Y Z') : ℝ)
Tactic: cases P.disjoint.elim hY hY' (not_disjoint_iff.2 ⟨y, yY, yY'⟩)
Cleared hypotheses: Y', hY', yY', nYZ, uYZ, dYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have nYZ₁ : Y ≠ Z
Tactic: cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)
Cleared hypotheses: Z', hZ', zZ', nYZ, uYZ, dYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have uYZ₁ : G.IsUniform (ε / 8) Y Z
Tactic: cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)
Cleared hypotheses: Z', hZ', zZ', nYZ, uYZ, dYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have dYZ₁ : ε / 4 ≤ (↑(G.edgeDensity Y Z) : ℝ)
Tactic: cases P.disjoint.elim hZ hZ' (not_disjoint_iff.2 ⟨z, zZ, zZ'⟩)
Cleared hypotheses: Z', hZ', zZ', nYZ, uYZ, dYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have dXY₁ : Function.onFun Disjoint id s Y
Tactic: have dXY := P.disjoint hX hY nXY
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have dXZ₁ : Function.onFun Disjoint id s Z
Tactic: have dXZ := P.disjoint hX hZ nXZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have dYZ₁ : Function.onFun Disjoint id Y Z
Tactic: have dYZ := P.disjoint hY hZ nYZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have that : 2 * (ε / 8) = ε / 4
Tactic: have that : 2 * (ε / 8) = ε / 4 := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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)
have this : ε / 4 ≤ 1
Tactic: have : ε / 4 ≤ 1 := ‹ε / 4 ≤ _›.trans (by exact mod_cast G.edgeDensity_le_one _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith : 1 - 2 * (ε / 8) < 0 → 8 / 8 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₁ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 8 = 8
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₃ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 8 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₄ : 1 - 2 * (ε / 8) < 0 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₅ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₆ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₁₁ : 1 - 2 * (ε / 8) < 0 → HMul.hMul (α := ℝ) 2 4 = 8
Tactic: linarith