no goals
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < ε'
refine' (hε hs' ht' (le_trans _ hs) (le_trans _ ht)).trans_le h <;> gcongr