awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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 : x₁ ∈ s
refine_2₁ : x₂ ∈ s
refine_2₂ : y₁ ∈ t_1
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
have refine_2₃ : y₂ ∈ t_1
Tactic: apply triple_eq_triple_of_mem hst hsu htu t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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 : x₁ ∈ s
refine_2₁ : x₂ ∈ s
refine_2₂ : y₁ ∈ t_1
refine_2₃ : y₂ ∈ t_1
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
have refine_2₄ : z₁ ∈ u
Tactic: apply triple_eq_triple_of_mem hst hsu htu t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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 : x₁ ∈ s
refine_2₁ : x₂ ∈ s
refine_2₂ : y₁ ∈ t_1
refine_2₃ : y₂ ∈ t_1
refine_2₄ : z₁ ∈ u
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
have refine_2₅ : z₂ ∈ u
Tactic: apply triple_eq_triple_of_mem hst hsu htu t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ x₁ ∈ s
have 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
Tactic: tauto
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ x₂ ∈ s
have 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
Tactic: tauto
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ y₁ ∈ t_1
have 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
Tactic: tauto
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ y₂ ∈ t_1
have 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
Tactic: tauto
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ z₁ ∈ u
have 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
Tactic: tauto
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ z₂ ∈ u
have 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
Tactic: tauto
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
Goal:
ε : ℝ
hε : 0 < ε
⊢ 0 < 1 - min 1 ε / 4
have this : min 1 ε ≤ 1
Tactic: have := min_le_left 1 ε
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : 0 < ε
this : min 1 ε ≤ 1
⊢ 0 < 1 - min 1 ε / 4
have linarith : 1 - min 1 ε / 4 ≤ 0 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : 0 < ε
this : min 1 ε ≤ 1
linarith : 1 - min 1 ε / 4 ≤ 0 → 4 / 4 = 1
⊢ 0 < 1 - min 1 ε / 4
have linarith₁ : 1 - min 1 ε / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 < 1 - min 1 ε / 4
have linarith₂ : 1 - min 1 ε / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 < 1 - min 1 ε / 4
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ 0 < 1 - min 1 ε / 4
have linarith₄ : 1 - min 1 ε / 4 ≤ 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
Goal:
ε : ℝ
hε : 0 < ε
⊢ 0 < triangleRemovalBound ε
have this : 0 < 1 - min 1 ε / 4
Tactic: have : 0 < 1 - min 1 ε / 4 := by have := min_le_left 1 ε; linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : ε ≤ 0
⊢ triangleRemovalBound ε ≤ 0
have rw : min (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 3)⁻¹
    ((1 - min 1 ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) 0) : ℝ)) 3) ≤
  0
Tactic: rw [triangleRemovalBound, ceil_eq_zero.2 (div_nonpos_of_nonneg_of_nonpos _ hε)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : ε ≤ 0
rw :
  min (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 3)⁻¹
      ((1 - min 1 ε / 4) * HPow.hPow (β := ℕ) (ε / HMul.hMul (α := ℝ) 16 (↑(bound (ε / 8) 0) : ℝ)) 3) ≤
    0
⊢ triangleRemovalBound ε ≤ 0
have rw₁ : LE.le (α := ℝ) 0 4
Tactic: rw [triangleRemovalBound, ceil_eq_zero.2 (div_nonpos_of_nonneg_of_nonpos _ hε)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≤
    (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3
have hbc : triangleRemovalBound ε ≤ (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : 0 < ε
⊢ (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 = 2⁻¹
have h : HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≠ 0
Tactic: rw [mul_inv, inv_mul_cancel_right₀]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : 0 < ε
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 < 1
have _ : triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≤
  (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
ε : ℝ
hε : 0 < ε
_ :
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 ≤
    (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 < 1
have _₁ : (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3)⁻¹ * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 = 2⁻¹
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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⁻¹
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑⌈4 / ε⌉₊ : ℝ) 3 < 1
have _₂ : LT.lt (α := ℝ) 2⁻¹ 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < 2 * k * (n / k)
have rw : n % k < 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k < k * (n / k)
have apply : k ≤ k * (n / k)
Tactic: apply (mod_lt n hk).trans_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
have inl : IsEmpty α → (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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) : ℝ)
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
have inr : Nonempty α → (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (hypothesis)
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 α
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
have this : 0 < #P.parts
Tactic: have := Finset.Nonempty.card_pos ⟨_, hX⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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) : ℝ)
have hc : LE.le (α := ℝ) 0 (↑(Fintype.card α) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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 α) : ℝ)
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤
    (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)
have hd : 0 < HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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) : ℝ)
⊢ (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤
    (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)
have hdb : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
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 / ε⌉₊) : ℝ) ≤ (↑(#s) : ℝ)
have _ : (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(bound (ε / 8) ⌈4 / ε⌉₊) : ℝ) ≤
  (↑(Fintype.card α) : ℝ) / HMul.hMul (α := ℝ) 2 (↑(#P.parts) : ℝ)
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
-- 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
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
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have 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}
Tactic: rw [mem_cliqueFinset_iff, is3Clique_iff] at ht
Cleared hypotheses: ht
-- 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
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}
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have 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)) : ℝ)
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
Cleared hypotheses: t, ht