𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
  rw [sub_nonneg, sq]
  gcongr
  exact hδ₁.le.trans (by norm_num)
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
rw [← sub_pos] at hδ₁
case inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2

case inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
obtain rfl | hs₂' := s₂.eq_empty_or_nonempty
case inr.inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2

case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
case inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
obtain rfl | ht₂' := t₂.eq_empty_or_nonempty
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by ring
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 1 - (1 - δ) * (1 - δ)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
rw [hr]
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ ↑(abs (edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁)) ≤ 1 - (1 - δ) * (1 - δ)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ abs (↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 1 - (1 - δ) * (1 - δ)
norm_cast
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ ↑(1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))) ≤ 1 - (1 - δ) * (1 - δ)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ ↑(abs (edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁)) ≤ 1 - (1 - δ) * (1 - δ)
refine'
  (Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans _
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) ≤ 1 - (1 - δ) * (1 - δ)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ ↑(1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))) ≤ 1 - (1 - δ) * (1 - δ)
push_cast
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
⊢ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) ≤ 1 - (1 - δ) * (1 - δ)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) ≤ 1 - (1 - δ) * (1 - δ)
have h₁ := hs₂'.mono hs
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) ≤ 1 - (1 - δ) * (1 - δ)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
⊢ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) ≤ 1 - (1 - δ) * (1 - δ)
have h₂ := ht₂'.mono ht
case inr.inr.h.h₁
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 1 - δ ≤ ↑(card s₂) / ↑(card s₁)

case inr.inr.h.h₂
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 1 - δ ≤ ↑(card t₂) / ↑(card t₁)
case inr.inr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) ≤ 1 - (1 - δ) * (1 - δ)
gcongr
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ δ * δ ≤ 2 * δ
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ 0 ≤ 2 * δ - δ ^ 2
rw [sub_nonneg, sq]
case h
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ δ ≤ 2
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ δ * δ ≤ 2 * δ
gcongr
no goals
case h
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ δ ≤ 2
exact hδ₁.le.trans (by norm_num)
no goals
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
⊢ 1 ≤ 2
norm_num
case inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * ↑(card s₁) ≤ 0
⊢ abs (↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
case inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
rw [Finset.card_empty, Nat.cast_zero] at hs₂
no goals
case inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * ↑(card s₁) ≤ 0
⊢ abs (↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
case inr.inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(card t₁) ≤ 0
⊢ abs (↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
case inr.inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
rw [Finset.card_empty, Nat.cast_zero] at ht₂
no goals
case inr.inl
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * ↑(card t₁) ≤ 0
⊢ abs (↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)) ≤ 2 * δ - δ ^ 2
simpa [edgeDensity, (nonpos_of_mul_nonpos_right ht₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
no goals
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
⊢ 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
ring
case inr.inr.h.h₁
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 0 < ↑(card s₁)
case inr.inr.h.h₁
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 1 - δ ≤ ↑(card s₂) / ↑(card s₁)
refine' (le_div_iff _).2 hs₂
no goals
case inr.inr.h.h₁
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 0 < ↑(card s₁)
exact_mod_cast h₁.card_pos
case inr.inr.h.h₂
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 0 < ↑(card t₁)
case inr.inr.h.h₂
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 1 - δ ≤ ↑(card t₂) / ↑(card t₁)
refine' (le_div_iff _).2 ht₂
no goals
case inr.inr.h.h₂
𝕜 : Type u_3
ι : Type ?u.39508
κ : Type ?u.39511
α : 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 ≤ δ
hδ₁✝ : δ < 1
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(card s₁) ≤ ↑(card s₂)
ht₂ : (1 - δ) * ↑(card t₁) ≤ ↑(card t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : Finset.Nonempty s₂
ht₂' : Finset.Nonempty t₂
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : Finset.Nonempty s₁
h₂ : Finset.Nonempty t₁
⊢ 0 < ↑(card t₁)
exact_mod_cast h₂.card_pos