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
ε : ℝ
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})) :
      ℝ)
_₁ :
  LE.le (α := ℝ)
    (↑(#({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})) :
      ℝ)
    (↑(#(A ∪ B ∪ C)) : ℝ)
_₂ : HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
have _₃ : HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ) <
  4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ)
Tactic: calc
    _ = (#((univ ×ˢ univ).filter fun (x, y) ↦
          G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) : ℝ) := by
      rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
      · norm_cast
        rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
      · gcongr with xy _
        exact fun hxy ↦ regularityReduced_le hxy
    _ ≤ #(A ∪ B ∪ C) := by gcongr; exact unreduced_edges_subset
    _ ≤ #(A ∪ B) + #C := mod_cast (card_union_le _ _)
    _ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _
    _ < 4 * (ε / 8) * card α ^ 2 + _ + _ := by
      gcongr; exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε
    _ ≤ _ + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 := by
      gcongr
      · exact hP.card_biUnion_offDiag_le hε hP'
      · exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)
    _ = 2 * ε * (card α ^ 2 : ℕ) := by norm_cast; ring
-- 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})) :
      ℝ)
_₁ :
  LE.le (α := ℝ)
    (↑(#({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})) :
      ℝ)
    (↑(#(A ∪ B ∪ C)) : ℝ)
_₂ : HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ)
_₃ :
  HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ) <
    4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
have _₄ : 4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ) ≤
  4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
      ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
    4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
Tactic: calc
    _ = (#((univ ×ˢ univ).filter fun (x, y) ↦
          G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) : ℝ) := by
      rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
      · norm_cast
        rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
      · gcongr with xy _
        exact fun hxy ↦ regularityReduced_le hxy
    _ ≤ #(A ∪ B ∪ C) := by gcongr; exact unreduced_edges_subset
    _ ≤ #(A ∪ B) + #C := mod_cast (card_union_le _ _)
    _ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _
    _ < 4 * (ε / 8) * card α ^ 2 + _ + _ := by
      gcongr; exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε
    _ ≤ _ + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 := by
      gcongr
      · exact hP.card_biUnion_offDiag_le hε hP'
      · exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)
    _ = 2 * ε * (card α ^ 2 : ℕ) := by norm_cast; ring
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inl : IsEmpty α →
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
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 α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
inl :
  IsEmpty α →
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr : Nonempty α →
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
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 α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr : ∀ (hε : ε ≤ 0),
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: obtain hε | hε := le_or_gt ε 0
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
inr :
  ∀ (hε : ε ≤ 0),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr₁ : ∀ (hε : 0 < ε),
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: obtain hε | hε := le_or_gt ε 0
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : ε ≤ 0
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr : LE.le (α := ℝ) 0 (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : ε ≤ 0
inr : LE.le (α := ℝ) 0 (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have apply : 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
Tactic: apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have hl : 4 / ε ≤ (↑l : ℝ)
Tactic: have hl : 4 / ε ≤ l := le_ceil (4 / ε)
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr : ∀ (hl' : Fintype.card α ≤ l),
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: rcases le_total (card α) l with hl' | hl'
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
inr :
  ∀ (hl' : Fintype.card α ≤ l),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr₁ : ∀ (hl' : l ≤ Fintype.card α),
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: rcases le_total (card α) l with hl' | hl'
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : Fintype.card α ≤ l
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑l : ℝ) 3
have ha : 0 ≤ triangleRemovalBound ε
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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : Fintype.card α ≤ l
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have _ : triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑l : ℝ) 3
Tactic: calc
      _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
        gcongr; exact (triangleRemovalBound_pos hε).le
      _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
      _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : Fintype.card α ≤ l
_ :
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑l : ℝ) 3
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have _₁ : LE.le (α := ℝ) 1 (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: calc
      _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
        gcongr; exact (triangleRemovalBound_pos hε).le
      _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
      _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr : ∀ (P : Finpartition (α := Finset α) univ) (hP₁ : P.IsEquipartition) (hP₂ : l ≤ #P.parts)
  (hP₃ : #P.parts ≤ bound (ε / 8) l) (hP₄ : P.IsUniform G (ε / 8)),
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G (by positivity : 0 < ε / 8) hl'
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have this : 4 / ε ≤ (↑(#P.parts) : ℝ)
Tactic: have : 4 / ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have k : 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
  2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
Tactic: have k := regularityReduced_edges_card_aux hε hP₁ hP₄ this
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have k₁ : 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
  2 * (ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ))
Tactic: rw [mul_assoc] at k
Cleared hypotheses: k
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * (ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ))
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have k₁ : HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
  ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
Tactic: replace k := lt_of_mul_lt_mul_left k zero_le_two
Cleared hypotheses: k
-- 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
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have inr : ∀ (t : Finset α) (ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3),
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
Tactic: obtain ⟨t, ht⟩ := hG.cliqueFinset_nonempty' regularityReduced_le k
-- 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
ε : ℝ
hG : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
⊢ ∃ G' ≤ G,
    ∃ (x : DecidableRel G'.Adj),
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
          ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ∧
        G'.CliqueFree 3
have by_contra! : ∀
  (h :
    ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
      (_ :
        HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
          ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
      ¬G'.CliqueFree 3),
  False
Tactic: by_contra! h
-- 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
ε : ℝ
hG : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
h :
  ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
    (_ :
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
    ¬G'.CliqueFree 3
⊢ False
have refine : ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
  H ≤ G →
    H.CliqueFree 3 →
      ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ≤
        HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#H.edgeFinset) : ℝ)
Tactic: refine hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
⊢ Rel t y x
have in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
⊢ Rel t y x
have in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₁ b)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₁ b)
⊢ Rel t y x
have in₀₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₀ a)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₁ b)
in₀₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₀ a)
⊢ Rel t y x
have in₂₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₂ c)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₁ b)
in₀₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₀ a)
in₂₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₂ c)
⊢ Rel t y x
have in₁₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₁ b)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₁ b)
in₀₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₀ a)
in₂₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₂ c)
in₁₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₁ b)
⊢ Rel t y x
have in₂₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₂ c)
Tactic: cases h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₁ (a, b, c).2.1)
have a₁ : ((a, b, c).1, (a, b, c).2.1, c) ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₀ (a, b, c).1)
have a₁ : ((a, b, c).1, (a, b, c).2.1, c) ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₂ (a, b, c).2.2)
have a₁ : ((a, b, c).1, b, (a, b, c).2.2) ∈ t
Tactic: constructor