awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 :
  ∀ (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
⊢ ∀ x ∈ P.nonUniforms G ε,
    HMul.hMul (α := 𝕜) (↑(#x.1) : 𝕜) (↑(#x.2) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2

Tactic:
simp only [Prod.forall, Finpartition.mk_mem_nonUniforms, and_imp]

Premises used: Finpartition.mk_mem_nonUniforms, and_imp, Prod.forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
calc_1 : #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)
⊢ HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2

Tactic:
rw [sq, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_le]

Premises used: sq, Nat.cast_mul, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

Tactic:
Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

Premises used: Finpartition.IsEquipartition.card_part_le_average_add_one, Nat.mul_le_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

Tactic:
exact Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

Premises used: Finpartition.IsEquipartition.card_part_le_average_add_one, Nat.mul_le_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 :
  (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 * ε <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 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 ε]

Premises used: mul_right_comm, mul_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 :
  (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 * ε <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 * ε

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 : #P.parts * (#P.parts - 1) * HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 < HPow.hPow (β := ℕ) (#A + #P.parts) 2
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 (β := ℕ) (#A + #P.parts) 2

Tactic:
aux (P.parts_nonempty hA.ne_empty).card_pos

Premises used: Finset.Nonempty.card_pos, Finset.Nonempty.ne_empty, _private.0.Finpartition.aux, Finpartition.parts_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 (β := ℕ) (#A + #P.parts) 2

Tactic:
exact aux (P.parts_nonempty hA.ne_empty).card_pos

Premises used: Finset.Nonempty.card_pos, Finset.Nonempty.ne_empty, _private.0.Finpartition.aux, Finpartition.parts_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ε
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
⊢ 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:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ε
simp_rw :
  card (α := α × α) ((P.nonUniforms G ε).biUnion fun (x : Finset α × Finset α) ↦ x.1 ×ˢ x.2) ≤
    ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)
⊢ 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:
simp_rw [← card_product]

Premises used: Finset.card_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 α) ↦ x.1 ×ˢ x.2) ≤
    ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)

Tactic:
card_biUnion_le

Premises used: Finset.card_biUnion_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 α) ↦ x.1 ×ˢ x.2) ≤
    ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)

Tactic:
exact card_biUnion_le

Premises used: Finset.card_biUnion_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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

Tactic:
hP.sum_nonUniforms_lt' hA hε hG

Premises used: Finpartition.IsEquipartition.sum_nonUniforms_lt'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ε
hbc : #P.parts ≤ #A
⊢ ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ #A

Tactic:
P.card_parts_le_card

Premises used: Finpartition.card_parts_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ #A

Tactic:
exact P.card_parts_le_card

Premises used: Finpartition.card_parts_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜) (↑(#A) : 𝕜)) 2 =
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
_₂ :
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2 =
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#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

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

Premises used: Finpartition.IsEquipartition.sum_nonUniforms_lt', HAdd.hAdd, Finset.card, Finpartition.nonUniforms
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜)

Tactic:
⟨G.symm ab, V, VP, U, UP, yV, xU, UV.symm, GUV.symm, ?_⟩

Premises used: Ne.symm, SimpleGraph.symm, And.intro, Exists.intro, SimpleGraph.IsUniform.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜)
refine : δ ≤ (↑(G.edgeDensity V U) : 𝕜)
⊢ G.Adj b a ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, b ∈ U ∧ a ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ (↑(G.edgeDensity U V) : 𝕜)

Tactic:
refine ⟨G.symm ab, V, VP, U, UP, yV, xU, UV.symm, GUV.symm, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 rwa rwa₁ rwa₂ rwa₃ : δ ≤ (↑(G.edgeDensity U V) : 𝕜)
⊢ δ ≤ (↑(G.edgeDensity V U) : 𝕜)

Tactic:
rwa [edgeDensity_comm]

Premises used: SimpleGraph.edgeDensity_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
ε δ : 𝕜
⊢ regularityReduced P G ε δ ≤ G

Tactic:
fun _ _ ↦ And.left

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
δ ε₁ ε₂ : 𝕜
hε : ε₁ ≤ ε₂
⊢ regularityReduced P G ε₁ δ ≤ regularityReduced P G ε₂ δ

Tactic:
fun _a _b ⟨hab, U, hU, V, hV, ha, hb, hUV, hGε, hGδ⟩ ↦
    ⟨hab, U, hU, V, hV, ha, hb, hUV, hGε.mono hε, hGδ⟩

Premises used: SimpleGraph.Adj, _private.0.SimpleGraph.regularityReduced_mono.match_1, And.intro, SimpleGraph.regularityReduced, Exists.intro, SimpleGraph.IsUniform.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
ε δ₁ δ₂ : 𝕜
hδ : δ₁ ≤ δ₂
⊢ regularityReduced P G ε δ₂ ≤ regularityReduced P G ε δ₁

Tactic:
fun _a _b ⟨hab, U, hU, V, hV, ha, hb, hUV, hUVε, hUVδ⟩ ↦
    ⟨hab, U, hU, V, hV, ha, hb, hUV, hUVε, hδ.trans hUVδ⟩

Premises used: _private.0.SimpleGraph.regularityReduced_anti.match_1, SimpleGraph.Adj, And.intro, SimpleGraph.regularityReduced, Exists.intro, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 : α
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
⊢ (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

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]

Premises used: not_le, SimpleGraph.regularityReduced_adj, Finpartition.mk_mem_nonUniforms, and_imp, not_exists, SimpleGraph.mem_interedges_iff, and_assoc, Finpartition.mk_mem_sparsePairs, Finset.mem_offDiag, Finset.mem_filter, Finset.mem_union, Prod.exists, not_and, Finset.mem_product, Finset.mem_biUnion, or_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
⊢ ∀ 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
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
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
⊢ (∃ (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

Premises used: Finpartition.exists_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
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
⊢ (∃ (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

Premises used: Finpartition.exists_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
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
⊢ (∃ (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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
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:
Or.inr (Or.inl ⟨U, hU, hx, hy, G.ne_of_adj h⟩)

Premises used: SimpleGraph.ne_of_adj, And.intro, Exists.intro, Or.inl, Or.inr