awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 refine_2₁ refine_2₂ :
  x₁ ∈ s →
    G.Adj x₁ y₁ →
      x₂ ∈ s →
        G.Adj x₂ y₂ →
          y₁ ∈ t_1 → z₁ ∈ u → G.Adj x₁ z₁ → G.Adj y₁ z₁ → y₂ ∈ t_1 → z₂ ∈ u → G.Adj x₂ z₂ → G.Adj y₂ z₂ → x₁ ∈ s
⊢ x₁ ∈ s

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 refine_2₁ refine_2₂ :
  x₁ ∈ s →
    G.Adj x₁ y₁ →
      x₂ ∈ s →
        G.Adj x₂ y₂ →
          y₁ ∈ t_1 → z₁ ∈ u → G.Adj x₁ z₁ → G.Adj y₁ z₁ → y₂ ∈ t_1 → z₂ ∈ u → G.Adj x₂ z₂ → G.Adj y₂ z₂ → x₂ ∈ s
⊢ x₂ ∈ s

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 refine_2₁ refine_2₂ :
  x₁ ∈ s →
    G.Adj x₁ y₁ →
      x₂ ∈ s →
        G.Adj x₂ y₂ →
          y₁ ∈ t_1 → z₁ ∈ u → G.Adj x₁ z₁ → G.Adj y₁ z₁ → y₂ ∈ t_1 → z₂ ∈ u → G.Adj x₂ z₂ → G.Adj y₂ z₂ → y₁ ∈ t_1
⊢ y₁ ∈ t_1

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 refine_2₁ refine_2₂ :
  x₁ ∈ s →
    G.Adj x₁ y₁ →
      x₂ ∈ s →
        G.Adj x₂ y₂ →
          y₁ ∈ t_1 → z₁ ∈ u → G.Adj x₁ z₁ → G.Adj y₁ z₁ → y₂ ∈ t_1 → z₂ ∈ u → G.Adj x₂ z₂ → G.Adj y₂ z₂ → y₂ ∈ t_1
⊢ y₂ ∈ t_1

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 refine_2₁ refine_2₂ :
  x₁ ∈ s →
    G.Adj x₁ y₁ →
      x₂ ∈ s →
        G.Adj x₂ y₂ →
          y₁ ∈ t_1 → z₁ ∈ u → G.Adj x₁ z₁ → G.Adj y₁ z₁ → y₂ ∈ t_1 → z₂ ∈ u → G.Adj x₂ z₂ → G.Adj y₂ z₂ → z₁ ∈ u
⊢ z₁ ∈ u

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 refine_2₁ refine_2₂ :
  x₁ ∈ s →
    G.Adj x₁ y₁ →
      x₂ ∈ s →
        G.Adj x₂ y₂ →
          y₁ ∈ t_1 → z₁ ∈ u → G.Adj x₁ z₁ → G.Adj y₁ z₁ → y₂ ∈ t_1 → z₂ ∈ u → G.Adj x₂ z₂ → G.Adj y₂ z₂ → z₂ ∈ u
⊢ z₂ ∈ u

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
⊢ min 1 ε ≤ 1

Tactic:
have := min_le_left 1 ε
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
this : min 1 ε ≤ 1
linarith : 1 - min 1 ε / 4 ≤ 0 → 4 / 4 = 1
linarith₁ : 1 - min 1 ε / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 - min 1 ε / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
linarith₃ :
  1 - min 1 ε / 4 ≤ 0 →
    HMul.hMul (α := ℝ) 3 (-1) + (min 1 ε - 1) + (HMul.hMul (α := ℝ) 4 1 - 1 * min 1 ε - HMul.hMul (α := ℝ) 4 0) = 0
linarith₄ : 1 - min 1 ε / 4 ≤ 0 → GT.gt (α := ℝ) 3 0
⊢ 0 < 1 - min 1 ε / 4

Tactic:
linarith
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
⊢ 0 < 1 - min 1 ε / 4

Tactic:
have : 0 < 1 - min 1 ε / 4 := by have := min_le_left 1 ε; linarith
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
this : 0 < 1 - min 1 ε / 4
⊢ 0 <
    min (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹
      ((1 - min 1 ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : ε ≤ 0
rw :
  min (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 3)⁻¹
      ((1 - min 1 ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) 0) : ℝ)) 3) ≤
    0
rw₁ : LE.le (α := ℝ) 0 4
⊢ triangleRemovalBound ε ≤ 0

Tactic:
rw [triangleRemovalBound, ceil_eq_zero.2 (div_nonpos_of_nonneg_of_nonpos _ hε)]

Premises used: Iff.mpr, Nat.ceil_eq_zero, div_nonpos_of_nonneg_of_nonpos, SimpleGraph.triangleRemovalBound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : ε ≤ 0
⊢ min (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 3)⁻¹
      ((1 - min 1 ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) 0) : ℝ)) 3) ≤
    0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : ε ≤ 0
⊢ LE.le (α := ℝ) 0 4

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
hbc : triangleRemovalBound ε ≤ (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≤
    (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹

Tactic:
min_le_left _ _

Premises used: min_le_left, SimpleGraph.triangleRemovalBound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε ≤ (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹

Tactic:
exact min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
h : HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≠ 0
⊢ (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 = 2⁻¹

Tactic:
rw [mul_inv, inv_mul_cancel_right₀]

Premises used: mul_inv, inv_mul_cancel_right₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε : 0 < ε
_ :
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≤
    (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3
_₁ : (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 = 2⁻¹
_₂ : LT.lt (α := ℝ) 2⁻¹ 1
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 < 1

Tactic:
calc
    _ ≤ (2 * ⌈4 / ε⌉₊ ^ 3 : ℝ)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 := by gcongr; exact min_le_left _ _
    _ = 2⁻¹ := by rw [mul_inv, inv_mul_cancel_right₀]; positivity
    _ < 1 := by norm_num

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, HPow.hPow, Nat.ceil, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
ε : ℝ
hε₁ : ε ≤ 1
⊢ triangleRemovalBound ε ≤
    (1 - ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ)) 3

Tactic:
simp [triangleRemovalBound, hε₁]

Premises used: SimpleGraph.triangleRemovalBound
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
n k : ℕ
hk : 0 < k
hn : k ≤ n
rw : n % k < k * (n / k)
⊢ n < 2 * k * (n / k)

Tactic:
rw [mul_assoc, two_mul, ← add_lt_add_iff_right (n % k), add_right_comm, add_assoc,
    mod_add_div n k, add_comm, add_lt_add_iff_right]

Premises used: add_assoc, mul_assoc, two_mul, add_right_comm, add_comm, Nat.mod_add_div, HMod.hMod, add_lt_add_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
n k : ℕ
hk : 0 < k
hn : k ≤ n
apply : k ≤ k * (n / k)
⊢ n % k < k * (n / k)

Tactic:
apply (mod_lt n hk).trans_le

Premises used: Nat.mod_lt, LT.lt.trans_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ k ≤ k * (n / k)

Tactic:
simpa using Nat.mul_le_mul_left k ((Nat.one_le_div_iff hk).2 hn)

Premises used: Iff.mpr, Nat.mul_le_mul_left, Nat.one_le_div_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
inl : IsEmpty α → (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
inr : Nonempty α → (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h : IsEmpty α
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)

Tactic:
simp [Fintype.card_eq_zero]

Premises used: Fintype.card_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h : Nonempty α
⊢ 0 < #P.parts

Tactic:
have := Finset.Nonempty.card_pos ⟨_, hX⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h : Nonempty α
this : 0 < #P.parts
hc : LE.le (α := ℝ) 0 (↑(Fintype.card α) : ℝ)
hd : 0 < HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)
hdb : LE.le (α := ℝ) 0 2
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤
    (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h : Nonempty α
this : 0 < #P.parts
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h : Nonempty α
this : 0 < #P.parts
⊢ LE.le (α := ℝ) (↑(Fintype.card α / #P.parts) : ℝ) (↑(#s) : ℝ)

Tactic:
mod_cast hP₁.average_le_card_part hX

Premises used: Finpartition.IsEquipartition.average_le_card_part, cast, Nat.cast_le._simp_1, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h : Nonempty α
this : 0 < #P.parts
_ :
  (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤
    (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)

Tactic:
calc
    _ ≤ card α / (2 * #P.parts : ℝ) := by gcongr
    _ ≤ ↑(card α / #P.parts) :=
      (div_le_iff₀' (by positivity)).2 <| mod_cast (aux ‹_› P.card_parts_le_card).le
    _ ≤ (#s : ℝ) := mod_cast hP₁.average_le_card_part hX

Premises used: Iff.mpr, Finpartition.IsEquipartition.average_le_card_part, HMul.hMul, _private.0.SimpleGraph.aux, Finpartition.card_parts_le_card, Fintype.card, HDiv.hDiv, LT.lt.le, Finpartition.parts, Nat.cast, Finset.card, OfNat.ofNat, div_le_iff₀'
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
t : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3
⊢ ∃ (a : α) (b : α) (c : α),
    (regularityReduced P G (ε / 8) (ε / 4)).Adj a b ∧
      (regularityReduced P G (ε / 8) (ε / 4)).Adj a c ∧ (regularityReduced P G (ε / 8) (ε / 4)).Adj b c ∧ t = {a, b, c}

Tactic:
rw [mem_cliqueFinset_iff, is3Clique_iff] at ht

Premises used: SimpleGraph.is3Clique_iff, SimpleGraph.mem_cliqueFinset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
t : Finset α
P : Finpartition (α := Finset α) univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
ht :
  ∃ (a : α) (b : α) (c : α),
    (regularityReduced P G (ε / 8) (ε / 4)).Adj a b ∧
      (regularityReduced P G (ε / 8) (ε / 4)).Adj a c ∧ (regularityReduced P G (ε / 8) (ε / 4)).Adj b c ∧ t = {a, b, c}
obtain :
  ∀ (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') : ℝ)),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
obtain ⟨x, y, z, ⟨-, s, hX, Y, hY, xX, yY, nXY, uXY, dXY⟩,
                   ⟨-, X', hX', Z, hZ, xX', zZ, nXZ, uXZ, dXZ⟩,
                   ⟨-, Y', hY', Z', hZ', yY', zZ', nYZ, uYZ, dYZ⟩, rfl⟩ := ht

Premises used: rfl
-- 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) : ℝ)
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') : ℝ)
⊢ s ∈ P.parts

Tactic:
cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)

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) : ℝ)
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
⊢ x ∈ s

Tactic:
cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)

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) : ℝ)
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
⊢ s ≠ Z

Tactic:
cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)

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) : ℝ)
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
⊢ G.IsUniform (ε / 8) s Z

Tactic:
cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)

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) : ℝ)
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
⊢ ε / 4 ≤ (↑(G.edgeDensity s Z) : ℝ)

Tactic:
cases P.disjoint.elim hX hX' (not_disjoint_iff.2 ⟨x, xX, xX'⟩)

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff