awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
simp_rw : #(interedges r s (P.parts.biUnion id)) = ∑ b ∈ P.parts, #(interedges r s b)
simp_rw₁ :
  card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s (id b)) = ∑ b ∈ P.parts, #(interedges r s b)
simp_rw₂ :
  card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)
simp_rw₃ : (↑P.parts : Set (Finset β)).PairwiseDisjoint (α := Finset (α × β)) fun (b : Finset β) ↦ interedges r s b
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

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

Premises used: Finpartition.disjoint, id, Finset.card_biUnion, Rel.interedges_biUnion_right, Finpartition.biUnion_parts, Rel.interedges_disjoint_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
P : Finpartition s
Q : Finpartition t
rw : Eq (α := ℕ) (∑ a ∈ P.parts, #(interedges r a t)) (∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))
⊢ #(interedges r s t) = ∑ ab ∈ P.parts ×ˢ Q.parts, #(interedges r ab.1 ab.2)

Tactic:
rw [card_interedges_finpartition_left _ P, sum_product]

Premises used: Rel.card_interedges_finpartition_left, Finset.sum_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
P : Finpartition s
Q : Finpartition t
e_f :
  Eq.{u_4 + 1} (α := Finset α → ℕ) (fun (a : Finset α) ↦ #(interedges r a t)) fun (x : Finset α) ↦
    ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
⊢ Eq (α := ℕ) (∑ a ∈ P.parts, #(interedges r a t)) (∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
P : Finpartition s
Q : Finpartition t
e_f : ∀ (x : Finset α), #(interedges r x t) = ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
⊢ Eq.{u_4 + 1} (α := Finset α → ℕ) (fun (a : Finset α) ↦ #(interedges r a t)) fun (x : Finset α) ↦
    ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
P : Finpartition s
Q : Finpartition t
x : Finset α
e_f : Eq (α := ℕ) (∑ b ∈ Q.parts, #(interedges r x b)) (∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))
e_f₁ : Finpartition t
e_f₂ : Eq (α := ℕ) (∑ b ∈ Q.parts, #(interedges r x b)) (∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))
e_f₃ : Finpartition t
⊢ #(interedges r x t) = ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Tactic:
rw [card_interedges_finpartition_right]

Premises used: Rel.card_interedges_finpartition_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0

Tactic:
simp [hs₂.ne_empty, ht₂.ne_empty]

Premises used: Finset.Nonempty.ne_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0

Tactic:
have hst : (#s₂ : ℚ) * #t₂ ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0
rw :
  (↑(#(interedges r s₂ t₂)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ) ≤
    (↑(#(interedges r s₁ t₁)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) * edgeDensity r s₂ t₂ ≤
    edgeDensity r s₁ t₁

Tactic:
rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel₀ hst]

Premises used: div_mul_div_comm, Rel.edgeDensity, mul_comm, div_mul_div_cancel₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0
hab : interedges r s₂ t₂ ⊆ interedges r s₁ t₁
⊢ (↑(#(interedges r s₂ t₂)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ) ≤
    (↑(#(interedges r s₁ t₁)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0
⊢ interedges r s₂ t₂ ⊆ interedges r s₁ t₁

Tactic:
interedges_mono hs ht

Premises used: Rel.interedges_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0
⊢ interedges r s₂ t₂ ⊆ interedges r s₁ t₁

Tactic:
exact interedges_mono hs ht

Premises used: Rel.interedges_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
(sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans ?_

Premises used: Rel.mul_edgeDensity_le_edgeDensity, sub_le_sub_left, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
refine :
  edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
⊢ edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
refine (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans ?_

Premises used: Rel.mul_edgeDensity_le_edgeDensity, sub_le_sub_left, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
le_trans ?_ (mul_le_of_le_one_right ?_ (edgeDensity_le_one r s₂ t₂))

Premises used: mul_le_of_le_one_right, Rel.edgeDensity_le_one, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
refine_1 :
  edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    (1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)) *
      edgeDensity r s₂ t₂
refine_2 : 0 ≤ 1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
⊢ edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
refine le_trans ?_ (mul_le_of_le_one_right ?_ (edgeDensity_le_one r s₂ t₂))

Premises used: mul_le_of_le_one_right, Rel.edgeDensity_le_one, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
refine_1 :
  edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    1 * edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) * edgeDensity r s₂ t₂
refine_1₁ refine_1₂ :
  edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) * edgeDensity r s₂ t₂
⊢ edgeDensity r s₂ t₂ -
      HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) *
        edgeDensity r s₂ t₂ ≤
    (1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)) *
      edgeDensity r s₂ t₂

Tactic:
rw [sub_mul, one_mul]

Premises used: sub_mul, one_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ 1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)

Premises used: sub_nonneg_of_le, mul_le_one₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
refine_2 : HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) ≤ 1
refine_2₁ : 0 ≤ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
refine_2₂ : HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) ≤ 1
⊢ 0 ≤ 1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
refine sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)

Premises used: sub_nonneg_of_le, mul_le_one₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) ≤ 1

Tactic:
div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card hs)) (Nat.cast_nonneg _)

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, Finset.card_le_card, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) ≤ 1

Tactic:
exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card hs)) (Nat.cast_nonneg _)

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, Finset.card_le_card, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
refine_2 : LE.le (α := ℚ) 0 (↑(#t₂) : ℚ)
refine_2₁ : LE.le (α := ℚ) 0 (↑(#t₁) : ℚ)
⊢ 0 ≤ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
apply div_nonneg

Premises used: div_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ LE.le (α := ℚ) 0 (↑(#t₂) : ℚ)

Tactic:
mod_cast Nat.zero_le _

Premises used: Nat.zero_le, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ LE.le (α := ℚ) 0 (↑(#t₂) : ℚ)

Tactic:
exact mod_cast Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ LE.le (α := ℚ) 0 (↑(#t₁) : ℚ)

Tactic:
mod_cast Nat.zero_le _

Premises used: Nat.zero_le, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ LE.le (α := ℚ) 0 (↑(#t₁) : ℚ)

Tactic:
exact mod_cast Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) ≤ 1

Tactic:
div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card ht)) (Nat.cast_nonneg _)

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, Finset.card_le_card, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) ≤ 1

Tactic:
exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card ht)) (Nat.cast_nonneg _)

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, Finset.card_le_card, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ |edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, ?_⟩

Premises used: Iff.mpr, abs_sub_le_iff, And.intro, Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
refine :
  edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
⊢ |edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
refine abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, ?_⟩

Premises used: Iff.mpr, abs_sub_le_iff, And.intro, Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
rw :
  edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s₂ t₂ - edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s₁ t₁ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
⊢ edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
rw [← add_sub_cancel_right (edgeDensity r s₁ t₁) (edgeDensity (fun x y ↦ ¬r x y) s₁ t₁),
    ← add_sub_cancel_right (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]

Premises used: Rel.edgeDensity_add_edgeDensity_compl, Rel.edgeDensity, add_sub_cancel_right, Finset.Nonempty.mono, Not, sub_sub_sub_cancel_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s₂ t₂ - edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s₁ t₁ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂

Premises used: Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s₂ t₂ - edgeDensity (fun (x : α) (y : β) ↦ ¬r x y) s₁ t₁ ≤
    1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)

Tactic:
exact edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂

Premises used: Rel.edgeDensity_sub_edgeDensity_le_one_sub_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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
rw : δ * δ ≤ 2 * δ
⊢ 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
rw [sub_nonneg, sq]

Premises used: sq, sub_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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hbc : δ ≤ 2
⊢ δ * δ ≤ 2 * δ

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δ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) 1 2

Tactic:
simp
-- 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δ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
⊢ δ ≤ 2

Tactic:
exact hδ₁.le.trans (by simp)

Premises used: LT.lt.le, LE.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 ≤ δ
hδ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
⊢ 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
    rw [sub_nonneg, sq]
    gcongr
    exact hδ₁.le.trans (by simp)
-- 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δ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
⊢ 0 < 1 - δ

Tactic:
rw [← sub_pos] at hδ₁

Premises used: sub_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δ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hδ₂ : 0 < 1 - δ
⊢ (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)

Tactic:
rw [← sub_pos] at hδ₁

Premises used: sub_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δ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hδ₂ : 0 < 1 - δ
hs₃ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
⊢ (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)

Tactic:
rw [← sub_pos] at hδ₁

Premises used: sub_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δ₁ : δ < 1
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hδ₂ : 0 < 1 - δ
hs₃ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₃ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
⊢ 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2

Tactic:
rw [← sub_pos] at hδ₁

Premises used: sub_pos