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
rw :
  HMul.hMul (α := ℝ) 2 (↑(#G.edgeFinset) : ℝ) -
      HMul.hMul (α := ℝ) 2 (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    HSub.hSub (α := ℝ) (↑(Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2}) : ℝ)
      (↑(Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    (↑(#({x ∈ SProd.sprod (α := Finset α) (β := Finset α) univ univ |
            match (motive := α × α → Prop) x with
            | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y})) :
      ℝ)
have rw₁ : Subset.{u_1} (α := Finset (α × α)) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}
  {x : α × α | G.Adj x.1 x.2}
Tactic: rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
-- 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
⊢ HMul.hMul (α := ℝ) 2 (↑(#G.edgeFinset) : ℝ) -
      HMul.hMul (α := ℝ) 2 (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) =
    HSub.hSub (α := ℝ) (↑(Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2}) : ℝ)
      (↑(Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}) : ℝ)
have norm_cast : Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
  Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
    (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
Tactic: norm_cast
-- 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
⊢ Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
have rw : Int.subNatNat
    (Finset.card.{u_1} (α := α × α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (x, y) => G.Adj x y})
    (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
  Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
    (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
Tactic: rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
-- 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
rw :
  Int.subNatNat
      (Finset.card.{u_1} (α := α × α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (x, y) => G.Adj x y})
      (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
⊢ Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
      (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
have rw₁ : Int.subNatNat
    (Finset.card.{u_1} (α := α × α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (x, y) => G.Adj x y})
    (Finset.card.{u_1} (α := α × α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (x, y) => (regularityReduced P G (ε / 8) (ε / 4)).Adj x y}) =
  Int.subNatNat (Finset.card.{u_1} (α := α × α) {x : α × α | G.Adj x.1 x.2})
    (Finset.card.{u_1} (α := α × α) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2})
Tactic: rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
-- 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
⊢ Subset.{u_1} (α := Finset (α × α)) {x : α × α | (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2}
    {x : α × α | G.Adj x.1 x.2}
have h : ∀ (xy : α × α),
  Membership.mem (γ := Finset (α × α)) univ xy → (regularityReduced P G (ε / 8) (ε / 4)).Adj xy.1 xy.2 → G.Adj xy.1 xy.2
Tactic: gcongr with xy _
-- 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
⊢ 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)) : ℝ)
have 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
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
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
⊢ HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ)
have bc : (↑(#(A ∪ B)) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
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
⊢ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) + (↑(#C) : ℝ) <
    4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 + (↑(#B) : ℝ) + (↑(#C) : ℝ)
have bc : (↑(#A) : ℝ) < 4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
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 + (↑(#B) : ℝ) + (↑(#C) : ℝ) ≤
    4 * (ε / 8) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
        ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2 +
      4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
have h₁ : (↑(#B) : ℝ) ≤ ε / 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
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
⊢ 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
have h₂ : (↑(#C) : ℝ) ≤ 4 * (ε / 4) * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Removal (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
P : Finpartition (α := Finset α) univ
ε : ℝ
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) : ℝ)
have 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) : ℝ)
Tactic: norm_cast
-- 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) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
have _ : 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})) :
    ℝ)
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})) :
      ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
have _₁ : 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: 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)) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
have _₂ : HAdd.hAdd (α := ℝ) (↑(#(A ∪ B)) : ℝ) (↑(#C) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#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