no goals
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ : 𝕜
u v : Finset α
ε : 𝕜
⊢ (u, v) ∈ nonUniforms P G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬SimpleGraph.IsUniform G ε u v
rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]