[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
x : α × β
⊢ x ∈ interedges r s t ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ r x.fst x.snd
[PROOFSTEP]
rw [interedges, mem_filter, Finset.mem_product, and_assoc]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
t : Finset β
⊢ interedges r ∅ t = ∅
[PROOFSTEP]
rw [interedges, Finset.empty_product, filter_empty]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁
x : α × β
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁
[PROOFSTEP]
simp_rw [mem_interedges_iff]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁
x : α × β
⊢ x.fst ∈ s₂ ∧ x.snd ∈ t₂ ∧ r x.fst x.snd → x.fst ∈ s₁ ∧ x.snd ∈ t₁ ∧ r x.fst x.snd
[PROOFSTEP]
exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ card (interedges r s t) + card (interedges (fun x y => ¬r x y) s t) = card s * card t
[PROOFSTEP]
classical
rw [← card_product, interedges, interedges, ← card_union_eq, filter_union_filter_neg_eq]
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ card (interedges r s t) + card (interedges (fun x y => ¬r x y) s t) = card s * card t
[PROOFSTEP]
rw [← card_product, interedges, interedges, ← card_union_eq, filter_union_filter_neg_eq]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ Disjoint (filter (fun e => r e.fst e.snd) (s ×ˢ t)) (filter (fun e => ¬r e.fst e.snd) (s ×ˢ t))
[PROOFSTEP]
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : Disjoint s s'
t : Finset β
⊢ Disjoint (interedges r s t) (interedges r s' t)
[PROOFSTEP]
rw [Finset.disjoint_left] at hs ⊢
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → ¬a ∈ interedges r s' t
[PROOFSTEP]
intro _ hx hy
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s' t
⊢ False
[PROOFSTEP]
rw [mem_interedges_iff] at hx hy 
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
a✝ : α × β
hx : a✝.fst ∈ s ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
hy : a✝.fst ∈ s' ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
⊢ False
[PROOFSTEP]
exact hs hx.1 hy.1
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t t' : Finset β
ht : Disjoint t t'
⊢ Disjoint (interedges r s t) (interedges r s t')
[PROOFSTEP]
rw [Finset.disjoint_left] at ht ⊢
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → ¬a ∈ t'
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → ¬a ∈ interedges r s t'
[PROOFSTEP]
intro _ hx hy
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → ¬a ∈ t'
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s t'
⊢ False
[PROOFSTEP]
rw [mem_interedges_iff] at hx hy 
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → ¬a ∈ t'
a✝ : α × β
hx : a✝.fst ∈ s ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
hy : a✝.fst ∈ s ∧ a✝.snd ∈ t' ∧ r a✝.fst a✝.snd
⊢ False
[PROOFSTEP]
exact ht hx.2.1 hy.2.1
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
⊢ interedges r (Finset.biUnion s f) t = Finset.biUnion s fun a => interedges r (f a) t
[PROOFSTEP]
ext
[GOAL]
case a
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
a✝ : α × β
⊢ a✝ ∈ interedges r (Finset.biUnion s f) t ↔ a✝ ∈ Finset.biUnion s fun a => interedges r (f a) t
[PROOFSTEP]
simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
⊢ interedges r s (Finset.biUnion t f) = Finset.biUnion t fun b => interedges r s (f b)
[PROOFSTEP]
ext a
[GOAL]
case a
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a✝ : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a ∈ interedges r s (Finset.biUnion t f) ↔ a ∈ Finset.biUnion t fun b => interedges r s (f b)
[PROOFSTEP]
simp only [mem_interedges_iff, mem_biUnion]
[GOAL]
case a
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a✝ : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a.fst ∈ s ∧ (∃ a_1, a_1 ∈ t ∧ a.snd ∈ f a_1) ∧ r a.fst a.snd ↔
    ∃ a_1, a_1 ∈ t ∧ a.fst ∈ s ∧ a.snd ∈ f a_1 ∧ r a.fst a.snd
[PROOFSTEP]
exact ⟨fun ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩ ↦ ⟨x₂, x₃, x₁, x₄, x₅⟩, fun ⟨x₂, x₃, x₁, x₄, x₅⟩ ↦ ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩⟩
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
⊢ interedges r (Finset.biUnion s f) (Finset.biUnion t g) =
    Finset.biUnion (s ×ˢ t) fun ab => interedges r (f ab.fst) (g ab.snd)
[PROOFSTEP]
simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ 0 ≤ edgeDensity r s t
[PROOFSTEP]
apply div_nonneg
[GOAL]
case ha
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(card (interedges r s t))
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
case hb
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(card s) * ↑(card t)
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ edgeDensity r s t ≤ 1
[PROOFSTEP]
apply div_le_one_of_le
[GOAL]
case h
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ ↑(card (interedges r s t)) ≤ ↑(card s) * ↑(card t)
[PROOFSTEP]
exact_mod_cast card_interedges_le_mul r s t
[GOAL]
case hb
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(card s) * ↑(card t)
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ edgeDensity r s t + edgeDensity (fun x y => ¬r x y) s t = 1
[PROOFSTEP]
rw [edgeDensity, edgeDensity, div_add_div_same, div_eq_one_iff_eq]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ ↑(card (interedges r s t)) + ↑(card (interedges (fun x y => ¬r x y) s t)) = ↑(card s) * ↑(card t)
[PROOFSTEP]
exact_mod_cast card_interedges_add_card_interedges_compl r s t
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : Finset.Nonempty s
ht : Finset.Nonempty t
⊢ ↑(card s) * ↑(card t) ≠ 0
[PROOFSTEP]
exact_mod_cast (mul_pos hs.card_pos ht.card_pos).ne'
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
t : Finset β
⊢ edgeDensity r ∅ t = 0
[PROOFSTEP]
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s : Finset α
⊢ edgeDensity r s ∅ = 0
[PROOFSTEP]
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ card (interedges r s t) = ∑ a in P.parts, card (interedges r a t)
[PROOFSTEP]
classical
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id.def]
rw [card_biUnion]
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ card (interedges r s t) = ∑ a in P.parts, card (interedges r a t)
[PROOFSTEP]
simp_rw [← P.biUnion_parts, interedges_biUnion_left, id.def]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ card (Finset.biUnion P.parts fun a => interedges r a t) = ∑ a in P.parts, card (interedges r a t)
[PROOFSTEP]
rw [card_biUnion]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ ∀ (x : Finset α), x ∈ P.parts → ∀ (y : Finset α), y ∈ P.parts → x ≠ y → Disjoint (interedges r x t) (interedges r y t)
[PROOFSTEP]
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (interedges r s t) = ∑ b in P.parts, card (interedges r s b)
[PROOFSTEP]
classical
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
rw [card_biUnion]
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (interedges r s t) = ∑ b in P.parts, card (interedges r s b)
[PROOFSTEP]
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (Finset.biUnion P.parts fun b => interedges r s b) = ∑ b in P.parts, card (interedges r s b)
[PROOFSTEP]
rw [card_biUnion]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝² : LinearOrderedField 𝕜
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ ∀ (x : Finset β), x ∈ P.parts → ∀ (y : Finset β), y ∈ P.parts → x ≠ y → Disjoint (interedges r s x) (interedges r s y)
[PROOFSTEP]
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ card (interedges r s t) = ∑ ab in P.parts ×ˢ Q.parts, card (interedges r ab.fst ab.snd)
[PROOFSTEP]
rw [card_interedges_finpartition_left _ P, sum_product]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a in P.parts, card (interedges r a t) = ∑ x in P.parts, ∑ y in Q.parts, card (interedges r (x, y).fst (x, y).snd)
[PROOFSTEP]
congr
[GOAL]
case e_f
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a => card (interedges r a t)) = fun x => ∑ y in Q.parts, card (interedges r (x, y).fst (x, y).snd)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ card (interedges r x✝ t) = ∑ y in Q.parts, card (interedges r (x✝, y).fst (x✝, y).snd)
[PROOFSTEP]
rw [card_interedges_finpartition_right]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
[PROOFSTEP]
have hst : (s₂.card : ℚ) * t₂.card ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 t₂) ≠ 0
[PROOFSTEP]
simp [hs₂.ne_empty, ht₂.ne_empty]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
[PROOFSTEP]
rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel _ hst]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card (interedges r s₂ t₂)) / (↑(card s₁) * ↑(card t₁)) ≤ ↑(card (interedges r s₁ t₁)) / (↑(card s₁) * ↑(card t₁))
[PROOFSTEP]
refine' div_le_div_of_le (by exact_mod_cast (s₁.card * t₁.card).zero_le) _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ 0 ≤ ↑(card s₁) * ↑(card t₁)
[PROOFSTEP]
exact_mod_cast (s₁.card * t₁.card).zero_le
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
hst : ↑(card s₂) * ↑(card t₂) ≠ 0
⊢ ↑(card (interedges r s₂ t₂)) ≤ ↑(card (interedges r s₁ t₁))
[PROOFSTEP]
exact_mod_cast card_le_of_subset (interedges_mono hs ht)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁))
[PROOFSTEP]
refine' (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁))
[PROOFSTEP]
refine' le_trans _ (mul_le_of_le_one_right _ (edgeDensity_le_one r s₂ t₂))
[GOAL]
case refine'_1
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
case refine'_2
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁))
[PROOFSTEP]
refine' sub_nonneg_of_le (mul_le_one _ _ _)
[GOAL]
case refine'_2.refine'_1
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
exact div_le_one_of_le ((@Nat.cast_le ℚ).2 (card_le_of_subset hs)) (Nat.cast_nonneg _)
[GOAL]
case refine'_2.refine'_2
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
apply div_nonneg
[GOAL]
case refine'_2.refine'_2.ha
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂)
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
case refine'_2.refine'_2.hb
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
case refine'_2.refine'_3
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
exact div_le_one_of_le ((@Nat.cast_le ℚ).2 (card_le_of_subset ht)) (Nat.cast_nonneg _)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁))
[PROOFSTEP]
refine' abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, _⟩
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁))
[PROOFSTEP]
rw [← add_sub_cancel (edgeDensity r s₁ t₁) (edgeDensity (fun x y ↦ ¬r x y) s₁ t₁), ←
  add_sub_cancel (edgeDensity r s₂ t₂) (edgeDensity (fun x y ↦ ¬r x y) s₂ t₂),
  edgeDensity_add_edgeDensity_compl _ (hs₂.mono hs) (ht₂.mono ht), edgeDensity_add_edgeDensity_compl _ hs₂ ht₂,
  sub_sub_sub_cancel_left]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 (fun x y => ¬r x y) s₂ t₂ - edgeDensity (fun x y => ¬r x y) s₁ t₁ ≤
    1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
[PROOFSTEP]
exact edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
  rw [sub_nonneg, sq]
  gcongr
  exact hδ₁.le.trans (by norm_num)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
rw [sub_nonneg, sq]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 * δ
[PROOFSTEP]
gcongr
[GOAL]
case h
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
exact hδ₁.le.trans (by norm_num)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
rw [← sub_pos] at hδ₁ 
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
obtain rfl | hs₂' := s₂.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 ∅)
⊢ |↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
rw [Finset.card_empty, Nat.cast_zero] at hs₂ 
[GOAL]
case inl
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
⊢ |↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
[GOAL]
case inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
obtain rfl | ht₂' := t₂.eq_empty_or_nonempty
[GOAL]
case inr.inl
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 ∅)
⊢ |↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
rw [Finset.card_empty, Nat.cast_zero] at ht₂ 
[GOAL]
case inr.inl
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
⊢ |↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
simpa [edgeDensity, (nonpos_of_mul_nonpos_right ht₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by ring
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
[PROOFSTEP]
ring
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
[PROOFSTEP]
rw [hr]
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 1 - (1 - δ) * (1 - δ)
[PROOFSTEP]
norm_cast
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
⊢ ↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - (1 - δ) * (1 - δ)
[PROOFSTEP]
refine' (Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans _
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
[PROOFSTEP]
push_cast
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
[PROOFSTEP]
have h₁ := hs₂'.mono hs
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
[PROOFSTEP]
have h₂ := ht₂'.mono ht
[GOAL]
case inr.inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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 - δ)
[PROOFSTEP]
gcongr
[GOAL]
case inr.inr.h.h₁
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
refine' (le_div_iff _).2 hs₂
[GOAL]
case inr.inr.h.h₁
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
exact_mod_cast h₁.card_pos
[GOAL]
case inr.inr.h.h₂
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
refine' (le_div_iff _).2 ht₂
[GOAL]
case inr.inr.h.h₂
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
exact_mod_cast h₂.card_pos
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ
[PROOFSTEP]
cases' lt_or_le δ 1 with h h
[GOAL]
case inl
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ
[PROOFSTEP]
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 δ)
[GOAL]
case inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ
[PROOFSTEP]
rw [two_mul]
[GOAL]
case inr
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂) - ↑(edgeDensity r s₁ t₁)| ≤ δ + δ
[PROOFSTEP]
refine' (abs_sub _ _).trans (add_le_add (le_trans _ h) (le_trans _ h))
[GOAL]
case inr.refine'_1
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
rw [abs_of_nonneg]
[GOAL]
case inr.refine'_1
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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'_1
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂)
[PROOFSTEP]
exact_mod_cast edgeDensity_le_one r _ _
[GOAL]
case inr.refine'_1
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₂)
[PROOFSTEP]
exact_mod_cast edgeDensity_nonneg r _ _
[GOAL]
case inr.refine'_2
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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
[PROOFSTEP]
rw [abs_of_nonneg]
[GOAL]
case inr.refine'_2
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
exact_mod_cast edgeDensity_le_one r _ _
[GOAL]
case inr.refine'_2
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
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₁)
[PROOFSTEP]
exact_mod_cast edgeDensity_nonneg r _ _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → α → Prop
inst✝ : DecidableRel r
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
hr : Symmetric r
x : α × α
⊢ Prod.swap x ∈ interedges r s t ↔ x ∈ interedges r t s
[PROOFSTEP]
rw [mem_interedges_iff, mem_interedges_iff, hr.iff]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → α → Prop
inst✝ : DecidableRel r
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
hr : Symmetric r
x : α × α
⊢ (Prod.swap x).fst ∈ s ∧ (Prod.swap x).snd ∈ t ∧ r (Prod.swap x).snd (Prod.swap x).fst ↔
    x.fst ∈ t ∧ x.snd ∈ s ∧ r x.fst x.snd
[PROOFSTEP]
exact and_left_comm
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → α → Prop
inst✝ : DecidableRel r
s✝ s₁ s₂ t✝ t₁ t₂ : Finset α
a b : α
hr : Symmetric r
s t : Finset α
⊢ edgeDensity r s t = edgeDensity r t s
[PROOFSTEP]
rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ card (interedges G s t) + card (interedges Gᶜ s t) = card s * card t
[PROOFSTEP]
rw [← card_product, interedges_def, interedges_def]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ card (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) + card (filter (fun e => Adj Gᶜ e.fst e.snd) (s ×ˢ t)) =
    card (s ×ˢ t)
[PROOFSTEP]
have : ((s ×ˢ t).filter fun e ↦ Gᶜ.Adj e.1 e.2) = (s ×ˢ t).filter fun e ↦ ¬G.Adj e.1 e.2 :=
  by
  refine' filter_congr fun x hx ↦ _
  rw [mem_product] at hx 
  rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ filter (fun e => Adj Gᶜ e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
[PROOFSTEP]
refine' filter_congr fun x hx ↦ _
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Adj Gᶜ x.fst x.snd ↔ ¬Adj G x.fst x.snd
[PROOFSTEP]
rw [mem_product] at hx 
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.fst ∈ s ∧ x.snd ∈ t
⊢ Adj Gᶜ x.fst x.snd ↔ ¬Adj G x.fst x.snd
[PROOFSTEP]
rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Adj Gᶜ e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
⊢ card (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) + card (filter (fun e => Adj Gᶜ e.fst e.snd) (s ×ˢ t)) =
    card (s ×ˢ t)
[PROOFSTEP]
rw [this, ← card_union_eq, filter_union_filter_neg_eq]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Adj Gᶜ e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
⊢ Disjoint (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) (filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t))
[PROOFSTEP]
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ edgeDensity G s t + edgeDensity Gᶜ s t = 1
[PROOFSTEP]
rw [edgeDensity_def, edgeDensity_def, div_add_div_same, div_eq_one_iff_eq]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card (interedges G s t)) + ↑(card (interedges Gᶜ s t)) = ↑(card s) * ↑(card t)
[PROOFSTEP]
exact_mod_cast card_interedges_add_card_interedges_compl _ h
[GOAL]
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card s) * ↑(card t) ≠ 0
[PROOFSTEP]
apply mul_ne_zero
[GOAL]
case ha
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card s) ≠ 0
[PROOFSTEP]
exact_mod_cast Nat.pos_iff_ne_zero.1 (Nonempty.card_pos ‹_›)
[GOAL]
case hb
𝕜 : Type u_1
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card t) ≠ 0
[PROOFSTEP]
exact_mod_cast Nat.pos_iff_ne_zero.1 (Nonempty.card_pos ‹_›)
