awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
inl :
  ∀ (hs : ∅ ⊆ s₁) (hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(card.{u_4} (α := α) ∅) : 𝕜)),
    |HSub.hSub (α := 𝕜) (↑(edgeDensity r ∅ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
inr :
  ∀ (hs₂' : s₂.Nonempty),
    |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
obtain rfl | hs₂' := s₂.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(card.{u_4} (α := α) ∅) : 𝕜)
⊢ (1 - δ) * (↑(#s₁) : 𝕜) ≤ 0

Tactic:
rw [Finset.card_empty, Nat.cast_zero] at hs₂

Premises used: Finset.card_empty, Nat.cast_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs : ∅ ⊆ s₁
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ 0
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r ∅ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'

Premises used: Nat.cast_nonneg, LE.le.antisymm, Rel.edgeDensity, nonpos_of_mul_nonpos_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
inr :
  ∀ (ht : ∅ ⊆ t₁) (ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(card.{u_5} (α := β) ∅) : 𝕜)),
    |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ ∅) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
inr₁ :
  ∀ (ht₂' : t₂.Nonempty),
    |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
obtain rfl | ht₂' := t₂.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(card.{u_5} (α := β) ∅) : 𝕜)
⊢ (1 - δ) * (↑(#t₁) : 𝕜) ≤ 0

Tactic:
rw [Finset.card_empty, Nat.cast_zero] at ht₂

Premises used: Finset.card_empty, Nat.cast_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht : ∅ ⊆ t₁
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ 0
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ ∅) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
simpa [edgeDensity, (nonpos_of_mul_nonpos_right ht₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'

Premises used: Nat.cast_nonneg, LE.le.antisymm, Rel.edgeDensity, nonpos_of_mul_nonpos_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
⊢ 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
⊢ 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)

Tactic:
have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
inr : |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 1 - (1 - δ) * (1 - δ)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
rw [hr]
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
inr : (↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| : 𝕜) ≤ 1 - (1 - δ) * (1 - δ)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 1 - (1 - δ) * (1 - δ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
⊢ (↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| : 𝕜) ≤ 1 - (1 - δ) * (1 - δ)

Tactic:
(Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans ?_

Premises used: Iff.mpr, Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul, LE.le.trans, Rat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
inr :
  (↑(1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
⊢ (↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| : 𝕜) ≤ 1 - (1 - δ) * (1 - δ)

Tactic:
refine
    (Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans ?_

Premises used: Iff.mpr, Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul, LE.le.trans, Rat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
inr :
  1 - HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
⊢ (↑(1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
⊢ s₁.Nonempty

Tactic:
have h₁ := hs₂'.mono hs
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
⊢ t₁.Nonempty

Tactic:
have h₂ := ht₂'.mono ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
inr : 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜)
inr₁ : 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜)
⊢ 1 - HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜)

Tactic:
(le_div_iff₀ ?_).2 hs₂

Premises used: Iff.mpr, le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
inr : LT.lt.{u_1} (α := 𝕜) 0 (↑(#s₁) : 𝕜)
⊢ 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜)

Tactic:
refine (le_div_iff₀ ?_).2 hs₂

Premises used: Iff.mpr, le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑(#s₁) : 𝕜)

Tactic:
mod_cast h₁.card_pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Finset.Nonempty.card_pos, Nat.cast, LT.lt, Finset.card, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑(#s₁) : 𝕜)

Tactic:
exact mod_cast h₁.card_pos

Premises used: Finset.Nonempty.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜)

Tactic:
(le_div_iff₀ ?_).2 ht₂

Premises used: Iff.mpr, le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
inr : LT.lt.{u_1} (α := 𝕜) 0 (↑(#t₁) : 𝕜)
⊢ 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜)

Tactic:
refine (le_div_iff₀ ?_).2 ht₂

Premises used: Iff.mpr, le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑(#t₁) : 𝕜)

Tactic:
mod_cast h₂.card_pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Finset.Nonempty.card_pos, Nat.cast, LT.lt, Finset.card, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
h₁ : s₁.Nonempty
h₂ : t₁.Nonempty
⊢ LT.lt.{u_1} (α := 𝕜) 0 (↑(#t₁) : 𝕜)

Tactic:
exact mod_cast h₂.card_pos

Premises used: Finset.Nonempty.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
inl : ∀ (h : δ < 1), |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
inr : ∀ (h : 1 ≤ δ), |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ

Tactic:
rcases lt_or_ge δ 1 with h | h

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : δ < 1
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ

Tactic:
(abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq r hs ht hδ h hscard htcard).trans
      ((sub_le_self_iff _).2 <| sq_nonneg δ)

Premises used: Iff.mpr, Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq, sq_nonneg, LE.le.trans, sub_le_self_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : δ < 1
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ

Tactic:
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 δ)

Premises used: Iff.mpr, Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq, sq_nonneg, LE.le.trans, sub_le_self_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ δ + δ
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ δ + δ

Tactic:
(abs_sub _ _).trans (add_le_add (le_trans ?_ h) (le_trans ?_ h))

Premises used: abs_sub, add_le_add, LE.le.trans, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₂ t₂) : 𝕜)| 1
inr₁ : LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₁ t₁) : 𝕜)| 1
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ δ + δ

Tactic:
refine (abs_sub _ _).trans (add_le_add (le_trans ?_ h) (le_trans ?_ h))

Premises used: abs_sub, add_le_add, LE.le.trans, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) 1
inr₁ : LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₂ t₂) : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₂ t₂) : 𝕜)| 1

Tactic:
rw [abs_of_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) 1

Tactic:
mod_cast edgeDensity_le_one r _ _

Premises used: congrArg, cast, Rel.edgeDensity, Rat.cast, LE.le, Rat.cast_le_natCast._simp_1, Eq.symm, Rel.edgeDensity_le_one, Nat.cast_one, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst_3 : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) 1

Tactic:
exact mod_cast edgeDensity_le_one r _ _

Premises used: Rel.edgeDensity_le_one