case inl
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : δ < 1
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ

case inr
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ
cases' lt_or_le δ 1 with h h
case inr
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ δ + δ
case inr
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ
rw [two_mul]
no goals
case inl
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : δ < 1
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ
exact (abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq r hs ht hδ h hscard htcard).trans
  ((sub_le_self_iff _).2 <| sq_nonneg δ)
case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ ↑(edgeDensity r s₁ t₁) ≤ 1

case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ 0 ≤ ↑(edgeDensity r s₁ t₁)
case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ abs ↑(edgeDensity r s₁ t₁) ≤ 1
rw [abs_of_nonneg]
case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ 0 ≤ ↑(edgeDensity r s₁ t₁)
case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ ↑(edgeDensity r s₁ t₁) ≤ 1

case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ 0 ≤ ↑(edgeDensity r s₁ t₁)
exact_mod_cast edgeDensity_le_one r _ _
no goals
case inr.refine'_2
𝕜 : Type u_3
ι : Type ?u.73664
κ : Type ?u.73667
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
htcard : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
h : 1 ≤ δ
⊢ 0 ≤ ↑(edgeDensity r s₁ t₁)
exact_mod_cast edgeDensity_nonneg r _ _