awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ε : ℝ
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
xy : α × α
h : Membership.mem (γ := Finset (α × α)) univ xy
⊢ (regularityReduced P G (ε / 8) (ε / 4)).Adj xy.1 xy.2 → G.Adj xy.1 xy.2

Tactic:
exact fun hxy ↦ regularityReduced_le hxy

Premises used: SimpleGraph.regularityReduced_le
-- 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
ε : ℝ
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
a :
  {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
⊢ 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)) : ℝ)

Tactic:
gcongr
-- 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
ε : ℝ
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
⊢ {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

Tactic:
unreduced_edges_subset

Premises used: Set.Mem, setOf, SimpleGraph.unreduced_edges_subset
-- 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
ε : ℝ
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
⊢ {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

Tactic:
exact unreduced_edges_subset

Premises used: SimpleGraph.unreduced_edges_subset
-- 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
ε : ℝ
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
⊢ (↑(#(A ∪ B ∪ C)) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ)

Tactic:
mod_cast (card_union_le _ _)

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Finset.card_union_le, Nat.cast, Finset.card, Union.union, Eq.symm, Eq.trans
-- 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
ε : ℝ
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
bc : (↑(#(A ∪ B)) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ)

Tactic:
gcongr
-- 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
ε : ℝ
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
⊢ (↑(#(A ∪ B)) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
mod_cast card_union_le _ _

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast_le._simp_1, LE.le, Finset.card_union_le, Nat.cast, Finset.card, Union.union, Eq.symm, Eq.trans
-- 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
ε : ℝ
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
⊢ (↑(#(A ∪ B)) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
exact mod_cast card_union_le _ _

Premises used: Finset.card_union_le
-- 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
ε : ℝ
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
bc : (↑(#A) : ℝ) < 4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
⊢ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ) <
    4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ)

Tactic:
gcongr
-- 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
ε : ℝ
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
⊢ 0 < ε / 8

Tactic:
positivity
-- 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
ε : ℝ
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
⊢ (↑(#A) : ℝ) < 4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2

Tactic:
exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε

Premises used: Finset.univ_nonempty, Finpartition.IsEquipartition.sum_nonUniforms_lt
-- 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
ε : ℝ
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
h₁ : (↑(#B) : ℝ) ≤ ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
h₂ : (↑(#C) : ℝ) ≤ 4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
⊢ 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:
gcongr
-- 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
ε : ℝ
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
⊢ (↑(#B) : ℝ) ≤ ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2

Tactic:
hP.card_biUnion_offDiag_le hε hP'

Premises used: Finpartition.IsEquipartition.card_biUnion_offDiag_le, Fintype.card
-- 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
ε : ℝ
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
⊢ (↑(#B) : ℝ) ≤ ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2

Tactic:
exact hP.card_biUnion_offDiag_le hε hP'

Premises used: Finpartition.IsEquipartition.card_biUnion_offDiag_le
-- 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
ε : ℝ
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
⊢ 0 ≤ ε / 4

Tactic:
positivity
-- 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
ε : ℝ
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
⊢ (↑(#C) : ℝ) ≤ 4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2

Tactic:
exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)

Premises used: Finpartition.IsEquipartition.card_interedges_sparsePairs_le
-- 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
ε : ℝ
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
norm_cast :
  4 * (ε / 8) * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) +
        ε / 2 * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) +
      4 * (ε / 4) * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) =
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
⊢ 4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
        ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
      4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 =
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)

Tactic:
norm_cast
-- 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
ε : ℝ
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
⊢ 4 * (ε / 8) * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) +
        ε / 2 * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) +
      4 * (ε / 4) * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) =
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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)) : ℝ)
inr :
  Nonempty α →
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

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 α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : IsEmpty α
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

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 α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
inr :
  ∀ (hε : ε ≤ 0),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
inr₁ :
  ∀ (hε : 0 < ε),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
obtain hε | hε := le_or_gt ε 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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)) : ℝ)
apply : 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans

Premises used: mul_nonpos_of_nonpos_of_nonneg, LE.le.trans, SimpleGraph.triangleRemovalBound_nonpos
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : ε ≤ 0
⊢ LE.le (α := ℝ) 0 (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : ε ≤ 0
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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 / ε⌉₊
⊢ 4 / ε ≤ (↑l : ℝ)

Tactic:
have hl : 4 / ε ≤ l := le_ceil (4 / ε)
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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)) : ℝ)
inr₁ :
  ∀ (hl' : l ≤ Fintype.card α),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
rcases le_total (card α) l with hl' | hl'

Premises used: Fintype.card, le_total
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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
ha : 0 ≤ triangleRemovalBound ε
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑l : ℝ) 3

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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
⊢ 0 ≤ triangleRemovalBound ε

Tactic:
(triangleRemovalBound_pos hε).le

Premises used: LT.lt.le, SimpleGraph.triangleRemovalBound_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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
⊢ 0 ≤ triangleRemovalBound ε

Tactic:
exact (triangleRemovalBound_pos hε).le

Premises used: LT.lt.le, SimpleGraph.triangleRemovalBound_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
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 (α := ℝ) (β := ℕ) (↑l : ℝ) 3 ≤ 1

Tactic:
(triangleRemovalBound_mul_cube_lt hε).le

Premises used: SimpleGraph.triangleRemovalBound_mul_cube_lt, LT.lt.le