awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
⊢ 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
have inr : 0 < ε / 4
Tactic: rwa [← div_le_iff₀', one_div_div]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜) <
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_1 : ∀ x ∈ P.nonUniforms G ε,
  HMul.hMul (α := 𝕜) (↑(#x.1) : 𝕜) (↑(#x.2) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2
Tactic: calc
    _ ≤ #(P.nonUniforms G ε) • (↑(#A / #P.parts + 1) : 𝕜) ^ 2 :=
      sum_le_card_nsmul _ _ _ ?_
    _ = _ := nsmul_eq_mul _ _
    _ ≤ _ := mul_le_mul_of_nonneg_right hG <| by positivity
    _ < _ := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
calc_1 :
  ∀ x ∈ P.nonUniforms G ε,
    HMul.hMul (α := 𝕜) (↑(#x.1) : 𝕜) (↑(#x.2) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2
⊢ ∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜) <
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_2 : (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
Tactic: calc
    _ ≤ #(P.nonUniforms G ε) • (↑(#A / #P.parts + 1) : 𝕜) ^ 2 :=
      sum_le_card_nsmul _ _ _ ?_
    _ = _ := nsmul_eq_mul _ _
    _ ≤ _ := mul_le_mul_of_nonneg_right hG <| by positivity
    _ < _ := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∀ x ∈ P.nonUniforms G ε,
    HMul.hMul (α := 𝕜) (↑(#x.1) : 𝕜) (↑(#x.2) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2
have calc_1 : ∀ (a b : Finset α),
  a ∈ P.parts →
    b ∈ P.parts →
      a ≠ b →
        ¬G.IsUniform ε a b →
          HMul.hMul (α := 𝕜) (↑(#a) : 𝕜) (↑(#b) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2
Tactic: simp only [Prod.forall, Finpartition.mk_mem_nonUniforms, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2
have calc_1 : #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)
Tactic: rw [sq, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_2 : (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 * ε <
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 * ε
Tactic: rw [mul_right_comm _ ε, mul_comm ε]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 * ε <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 * ε
have calc_2 : (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_2 : #P.parts * (#P.parts - 1) * HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 < HPow.hPow (β := ℕ) (#A + #P.parts) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ LE.le.{u_2} (α := 𝕜)
    (↑(card (α := α × α)
          ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V)) :
      𝕜)
    (∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜))
have norm_cast : card (α := α × α)
    ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
      match (motive := Finset α × Finset α → Finset (α × α)) x with
      | (U, V) => U ×ˢ V) ≤
  ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ card (α := α × α)
      ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
        match (motive := Finset α × Finset α → Finset (α × α)) x with
        | (U, V) => U ×ˢ V) ≤
    ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.2
have simp_rw : card (α := α × α) ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦ x.1 ×ˢ x.2) ≤
  ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)
Tactic: simp_rw [← card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
have hbc : #P.parts ≤ #A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ (↑(card (α := α × α)
          ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V)) :
      𝕜) <
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have _ : LE.le.{u_2} (α := 𝕜)
  (↑(card (α := α × α)
        ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
          match (motive := Finset α × Finset α → Finset (α × α)) x with
          | (U, V) => U ×ˢ V)) :
    𝕜)
  (∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜))
Tactic: calc
    _ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by
        norm_cast; simp_rw [← card_product]; exact card_biUnion_le
    _ < _ := hP.sum_nonUniforms_lt' hA hε hG
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
_ :
  LE.le.{u_2} (α := 𝕜)
    (↑(card (α := α × α)
          ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V)) :
      𝕜)
    (∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜))
⊢ (↑(card (α := α × α)
          ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V)) :
      𝕜) <
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have _₁ : ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
Tactic: calc
    _ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by
        norm_cast; simp_rw [← card_product]; exact card_biUnion_le
    _ < _ := hP.sum_nonUniforms_lt' hA hε hG
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
_ :
  LE.le.{u_2} (α := 𝕜)
    (↑(card (α := α × α)
          ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V)) :
      𝕜)
    (∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜))
_₁ :
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
⊢ (↑(card (α := α × α)
          ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V)) :
      𝕜) <
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have _₂ : ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2 =
  4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
Tactic: calc
    _ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by
        norm_cast; simp_rw [← card_product]; exact card_biUnion_le
    _ < _ := hP.sum_nonUniforms_lt' hA hε hG
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε_1 δ_1 : 𝕜
u v : Finset α
ε δ : 𝕜
a b : α
ab : G.Adj a b
U : Finset α
UP : U ∈ P.parts
V : Finset α
VP : V ∈ P.parts
xU : a ∈ U
yV : b ∈ V
UV : U ≠ V
GUV : G.IsUniform ε U V
εUV : δ ≤ (↑(G.edgeDensity U V) : 𝕜)
⊢ G.Adj b a ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, b ∈ U ∧ a ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ (↑(G.edgeDensity U V) : 𝕜)
have refine : δ ≤ (↑(G.edgeDensity V U) : 𝕜)
Tactic: refine ⟨G.symm ab, V, VP, U, UP, yV, xU, UV.symm, GUV.symm, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
⊢ (x, y) ∈
      {x ∈ A ×ˢ A |
        match (motive := α × α → Prop) x with
        | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} →
    (x, y) ∈
      ((P.nonUniforms G (ε / 8)).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => U ×ˢ V) ∪
          P.parts.biUnion offDiag ∪
        (P.sparsePairs G (ε / 4)).biUnion fun (x : Finset α × Finset α) ↦
          match (motive := Finset α × Finset α → Finset (α × α)) x with
          | (U, V) => G.interedges U V
have simp : x ∈ A →
  y ∈ A →
    G.Adj x y →
      (G.Adj x y →
          ∀ x_1 ∈ P.parts,
            ∀ x_2 ∈ P.parts,
              x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4) →
        (∃ (a : Finset α) (b : Finset α),
            a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
          (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
            ∃ (a : Finset α) (b : Finset α),
              a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: simp only [mem_filter, regularityReduced_adj, not_and, not_exists,
    not_le, mem_biUnion, mem_union, mem_product, Prod.exists, mem_offDiag, and_imp,
    or_assoc, and_assoc, P.mk_mem_nonUniforms, Finpartition.mk_mem_sparsePairs, mem_interedges_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  G.Adj x y →
    ∀ x_1 ∈ P.parts,
      ∀ x_2 ∈ P.parts,
        x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have h'₁ : ∀ x_1 ∈ P.parts,
  ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
Tactic: replace h' := h' h
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have obtain : ∀ (U : Finset α) (hU : U ∈ P.parts) (hx : x ∈ U),
  (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: obtain ⟨U, hU, hx⟩ := P.exists_mem hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have obtain : ∀ (V : Finset α) (hV : V ∈ P.parts) (hy : y ∈ V),
  (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: obtain ⟨V, hV, hy⟩ := P.exists_mem hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have inl : ∀ (hV : U ∈ P.parts) (hy : y ∈ U),
  (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: obtain rfl | hUV := eq_or_ne U V
Cleared hypotheses: V, hV, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
inl :
  ∀ (hV : U ∈ P.parts) (hy : y ∈ U),
    (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
      (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
        ∃ (a : Finset α) (b : Finset α),
          a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have inr : ∀ (hUV : U ≠ V),
  (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: obtain rfl | hUV := eq_or_ne U V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have pos : ∀ (h₂ : G.IsUniform (ε / 8) U V),
  (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: by_cases h₂ : G.IsUniform (ε / 8) U V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
x y : α
hx_1 : x ∈ A
hy_1 : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts,
      x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → (↑(G.edgeDensity x_1 x_2) : 𝕜) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
pos :
  ∀ (h₂ : G.IsUniform (ε / 8) U V),
    (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
      (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
        ∃ (a : Finset α) (b : Finset α),
          a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
⊢ (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
have neg : ∀ (h₂ : ¬G.IsUniform (ε / 8) U V),
  (∃ (a : Finset α) (b : Finset α), a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ (a : Finset α) (b : Finset α),
        a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ (↑(G.edgeDensity a b) : 𝕜) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Tactic: by_cases h₂ : G.IsUniform (ε / 8) U V