awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have 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
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
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₂₃ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 6 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
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
⊢ 0 ≤ 1 - 2 * (ε / 8)
have linarith₂₄ : 1 - 2 * (ε / 8) < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have this : 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
-- 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 : 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
have hbc : triangleRemovalBound ε ≤ (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3
Tactic: gcongr
-- 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 : 0 ≤ 1 - 2 * (ε / 8)
⊢ (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) : ℝ)
have h₁ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
Tactic: gcongr
-- 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 : 0 ≤ 1 - 2 * (ε / 8)
h₁ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
⊢ (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) : ℝ)
have h₂ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Y) : ℝ)
Tactic: gcongr
-- 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 : 0 ≤ 1 - 2 * (ε / 8)
h₁ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
h₂ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Y) : ℝ)
⊢ (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) : ℝ)
have h₃ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#Z) : ℝ)
Tactic: gcongr
-- 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 : 0 ≤ 1 - 2 * (ε / 8)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have _ : triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
  (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3 *
    HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 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
-- 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 : 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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have _₁ : (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: 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
-- 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 : 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 / ε⌉₊) : ℝ))
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have _₂ : (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: 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
-- 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
ε : ℝ
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
⊢ 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})) :
      ℝ)
have 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}) : ℝ)
Tactic: rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]