𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₂ t₂ - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤
    1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁ ≤ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
refine' (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans _
case refine'_1
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₂ t₂ - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤
    (1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))) * edgeDensity r s₂ t₂

case refine'_2
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ 0 ≤ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₂ t₂ - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤
    1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
refine' le_trans _ (mul_le_of_le_one_right _ (edgeDensity_le_one r s₂ t₂))
case refine'_2.refine'_1
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ ↑(card s₂) / ↑(card s₁) ≤ 1

case refine'_2.refine'_2
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ 0 ≤ ↑(card t₂) / ↑(card t₁)

case refine'_2.refine'_3
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ ↑(card t₂) / ↑(card t₁) ≤ 1
case refine'_2
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ 0 ≤ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
refine' sub_nonneg_of_le (mul_le_one _ _ _)
no goals
case refine'_1
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₂ t₂ - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤
    (1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))) * edgeDensity r s₂ t₂
rw [sub_mul, one_mul]
no goals
case refine'_2.refine'_1
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ ↑(card s₂) / ↑(card s₁) ≤ 1
exact div_le_one_of_le ((@Nat.cast_le ℚ).2 (card_le_of_subset hs)) (Nat.cast_nonneg _)
no goals
case refine'_2.refine'_2
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ 0 ≤ ↑(card t₂) / ↑(card t₁)
apply div_nonneg <;> exact_mod_cast Nat.zero_le _
no goals
case refine'_2.refine'_3
𝕜 : Type ?u.34819
ι : Type ?u.34822
κ : Type ?u.34825
α : 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₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ ↑(card t₂) / ↑(card t₁) ≤ 1
exact div_le_one_of_le ((@Nat.cast_le ℚ).2 (card_le_of_subset ht)) (Nat.cast_nonneg _)