[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 ‹_›)


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e x).fst * (mulDysonEtransform e x).snd ⊆ x.fst * x.snd
[PROOFSTEP]
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.snd * e⁻¹ • x.fst ⊆ x.fst * x.snd
[PROOFSTEP]
rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (mulDysonEtransform e x).fst + Finset.card (mulDysonEtransform e x).snd =
    Finset.card x.fst + Finset.card x.snd
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (x.fst ∪ e • x.snd) + Finset.card (x.snd ∩ e⁻¹ • x.fst) = Finset.card x.fst + Finset.card x.snd
[PROOFSTEP]
rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm, card_union_add_card_inter,
  card_smul_finset]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonEtransform e (mulDysonEtransform e x) = mulDysonEtransform e x
[PROOFSTEP]
ext : 1
[GOAL]
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e (mulDysonEtransform e x)).fst = (mulDysonEtransform e x).fst
[PROOFSTEP]
dsimp
[GOAL]
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e (mulDysonEtransform e x)).snd = (mulDysonEtransform e x).snd
[PROOFSTEP]
dsimp
[GOAL]
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∪ e • x.snd ∪ e • (x.snd ∩ e⁻¹ • x.fst) = x.fst ∪ e • x.snd
[PROOFSTEP]
rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left_iff_subset]
[GOAL]
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
[PROOFSTEP]
exact inter_subset_union
[GOAL]
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ∩ e⁻¹ • (x.fst ∪ e • x.snd) = x.snd ∩ e⁻¹ • x.fst
[PROOFSTEP]
rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left_iff_subset]
[GOAL]
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ⊆ x.snd ∪ e⁻¹ • x.fst
[PROOFSTEP]
exact inter_subset_union
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (mulDysonEtransform e x).snd ⊆ (mulDysonEtransform e x).fst
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.snd ∩ e⁻¹ • x.fst) ⊆ x.fst ∪ e • x.snd
[PROOFSTEP]
rw [smul_finset_inter, smul_inv_smul, inter_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
[PROOFSTEP]
exact inter_subset_union
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ mulEtransformLeft 1 x = x
[PROOFSTEP]
simp [mulEtransformLeft]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ mulEtransformRight 1 x = x
[PROOFSTEP]
simp [mulEtransformRight]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulEtransformLeft e x).fst * (mulEtransformLeft e x).snd ⊆ x.fst * x.snd
[PROOFSTEP]
refine' inter_mul_union_subset_union.trans (union_subset Subset.rfl _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.fst * e⁻¹ • x.snd ⊆ x.fst * x.snd
[PROOFSTEP]
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulEtransformRight e x).fst * (mulEtransformRight e x).snd ⊆ x.fst * x.snd
[PROOFSTEP]
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.fst * e⁻¹ • x.snd ⊆ x.fst * x.snd
[PROOFSTEP]
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ Finset.card x.fst + Finset.card (op e • x.fst) = 2 * Finset.card x.fst
[PROOFSTEP]
rw [card_smul_finset, two_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ Finset.card x.snd + Finset.card (e⁻¹ • x.snd) = 2 * Finset.card x.snd
[PROOFSTEP]
rw [card_smul_finset, two_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ card (mulEtransformLeft e x).fst + card (mulEtransformLeft e x).snd +
      (card (mulEtransformRight e x).fst + card (mulEtransformRight e x).snd) =
    card x.fst + card x.snd + (card x.fst + card x.snd)
[PROOFSTEP]
rw [add_add_add_comm, mulEtransformLeft.card, mulEtransformRight.card, ← mul_add, two_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulEtransformLeft e⁻¹ x = Prod.swap (mulEtransformRight e (Prod.swap x))
[PROOFSTEP]
simp [-op_inv, op_smul_eq_smul, mulEtransformLeft, mulEtransformRight]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulEtransformRight e⁻¹ x = Prod.swap (mulEtransformLeft e (Prod.swap x))
[PROOFSTEP]
simp [-op_inv, op_smul_eq_smul, mulEtransformLeft, mulEtransformRight]


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
haveI : ∀ u, Decidable ((u : Set α).PairwiseDisjoint (· • t)) := fun u ↦ Classical.dec _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
set C := s.powerset.filter fun u ↦ u.toSet.PairwiseDisjoint (· • t)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
obtain ⟨u, hu, hCmax⟩ :=
  C.exists_maximal
    (filter_nonempty_iff.2 ⟨∅, empty_mem_powerset _, by rw [coe_empty]; exact Set.pairwiseDisjoint_empty⟩)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
⊢ Set.PairwiseDisjoint ↑∅ fun x => x • t
[PROOFSTEP]
rw [coe_empty]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
⊢ Set.PairwiseDisjoint ∅ fun x => x • t
[PROOFSTEP]
exact Set.pairwiseDisjoint_empty
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ∈ C
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
rw [mem_filter, mem_powerset] at hu
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
⊢ ∃ u, card u * card t ≤ card (s * t) ∧ s ⊆ u * t / t
[PROOFSTEP]
refine'
  ⟨u, (card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hu.2).ge.trans (card_le_of_subset <| mul_subset_mul_right hu.1),
    fun a ha ↦ _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
⊢ a ∈ u * t / t
[PROOFSTEP]
rw [mul_div_assoc]
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
⊢ a ∈ u * (t / t)
[PROOFSTEP]
by_cases hau : a ∈ u
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : a ∈ u
⊢ a ∈ u * (t / t)
[PROOFSTEP]
exact subset_mul_left _ ht.one_mem_div hau
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
⊢ a ∈ u * (t / t)
[PROOFSTEP]
by_cases H : ∀ b ∈ u, Disjoint (a • t) (b • t)
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ a ∈ u * (t / t)
[PROOFSTEP]
refine' (hCmax _ _ <| ssubset_insert hau).elim
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ insert a u ∈ C
[PROOFSTEP]
rw [mem_filter, mem_powerset, insert_subset_iff, coe_insert]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ (a ∈ s ∧ u ⊆ s) ∧ Set.PairwiseDisjoint (insert a ↑u) fun x => x • t
[PROOFSTEP]
exact ⟨⟨ha, hu.1⟩, hu.2.insert fun _ hb _ ↦ H _ hb⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ¬∀ (b : α), b ∈ u → Disjoint (a • t) (b • t)
⊢ a ∈ u * (t / t)
[PROOFSTEP]
push_neg at H
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∃ b, b ∈ u ∧ ¬Disjoint (a • t) (b • t)
⊢ a ∈ u * (t / t)
[PROOFSTEP]
simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
H : ∃ b, b ∈ u ∧ ∃ a_1, a⁻¹ • a_1 ∈ t ∧ b⁻¹ • a_1 ∈ t
⊢ a ∈ u * (t / t)
[PROOFSTEP]
obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ a ∈ u * (t / t)
[PROOFSTEP]
refine' mem_mul.2 ⟨b, a / b, hb, _, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ b * (a / b) = a
[PROOFSTEP]
simp
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ a / b ∈ t / t
[PROOFSTEP]
exact mem_div.2 ⟨_, _, hc₂, hc₁, by simp [div_eq_mul_inv a b, mul_comm]⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
s t : Finset α
ht : Finset.Nonempty t
this : (u : Set α) → Decidable (Set.PairwiseDisjoint u fun x => x • t)
C : Finset (Finset α) := filter (fun u => Set.PairwiseDisjoint ↑u fun x => x • t) (powerset s)
u : Finset α
hu : u ⊆ s ∧ Set.PairwiseDisjoint ↑u fun x => x • t
hCmax : ∀ (x : Finset α), x ∈ C → ¬u < x
a : α
ha : a ∈ s
hau : ¬a ∈ u
b : α
hb : b ∈ u
c : α
hc₁ : a⁻¹ • c ∈ t
hc₂ : b⁻¹ • c ∈ t
⊢ b⁻¹ • c / a⁻¹ • c = a / b
[PROOFSTEP]
simp [div_eq_mul_inv a b, mul_comm]


[GOAL]
V : Type
G : SimpleGraph V
inst✝ : Finite V
⊢ ↑(SimpleGraph.end G) → False
[PROOFSTEP]
rintro ⟨s, _⟩
[GOAL]
case mk
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
⊢ False
[PROOFSTEP]
cases nonempty_fintype V
[GOAL]
case mk.intro
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
val✝ : Fintype V
⊢ False
[PROOFSTEP]
obtain ⟨v, h⟩ := (s <| Opposite.op Finset.univ).nonempty
[GOAL]
case mk.intro.intro
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
val✝ : Fintype V
v : V
h : v ∈ ↑(s (Opposite.op Finset.univ))
⊢ False
[PROOFSTEP]
exact Set.disjoint_iff.mp (s _).disjoint_right ⟨by simp only [Opposite.unop_op, Finset.coe_univ, Set.mem_univ], h⟩
[GOAL]
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
val✝ : Fintype V
v : V
h : v ∈ ↑(s (Opposite.op Finset.univ))
⊢ v ∈ ↑(Opposite.op Finset.univ).unop
[PROOFSTEP]
simp only [Opposite.unop_op, Finset.coe_univ, Set.mem_univ]
[GOAL]
V : Type
G : SimpleGraph V
e : ↑(SimpleGraph.end G)
K : (Finset V)ᵒᵖ
⊢ Set.Infinite (ComponentCompl.supp (↑e K))
[PROOFSTEP]
refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)
[GOAL]
V : Type
G : SimpleGraph V
e : ↑(SimpleGraph.end G)
K : (Finset V)ᵒᵖ
L : Finset V
h : K.unop ⊆ L
⊢ ∃ D, ComponentCompl.hom h D = ↑e K
[PROOFSTEP]
change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h
[GOAL]
V : Type
G : SimpleGraph V
e : ↑(SimpleGraph.end G)
K : (Finset V)ᵒᵖ
L : Finset V
h : K.unop ⊆ (Opposite.op L).unop
⊢ ∃ D, ComponentCompl.hom h D = ↑e K
[PROOFSTEP]
exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩
[GOAL]
V : Type
G : SimpleGraph V
inst✝² : LocallyFinite G
inst✝¹ : Fact (Preconnected G)
inst✝ : Infinite V
⊢ Set.Nonempty (SimpleGraph.end G)
[PROOFSTEP]
classical apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor
[GOAL]
V : Type
G : SimpleGraph V
inst✝² : LocallyFinite G
inst✝¹ : Fact (Preconnected G)
inst✝ : Infinite V
⊢ Set.Nonempty (SimpleGraph.end G)
[PROOFSTEP]
apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor