awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
⊢ edgeDensity r s ∅ = 0
have rw : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(card.{u_5} (α := β) ∅) : ℚ) = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
rw : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(card.{u_5} (α := β) ∅) : ℚ) = 0
⊢ edgeDensity r s ∅ = 0
have rw₁ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑0 : ℚ) = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
rw : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(card.{u_5} (α := β) ∅) : ℚ) = 0
rw₁ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑0 : ℚ) = 0
⊢ edgeDensity r s ∅ = 0
have rw₂ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) 0 = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
rw : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(card.{u_5} (α := β) ∅) : ℚ) = 0
rw₁ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑0 : ℚ) = 0
rw₂ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) 0 = 0
⊢ edgeDensity r s ∅ = 0
have rw₃ : HDiv.hDiv (α := ℚ) (↑(#(interedges r s ∅)) : ℚ) 0 = 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
rw : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(card.{u_5} (α := β) ∅) : ℚ) = 0
rw₁ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑0 : ℚ) = 0
rw₂ : (↑(#(interedges r s ∅)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) 0 = 0
rw₃ : HDiv.hDiv (α := ℚ) (↑(#(interedges r s ∅)) : ℚ) 0 = 0
⊢ edgeDensity r s ∅ = 0
have rw₄ : Eq (α := ℚ) 0 0
Tactic: rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)
have simp_rw : card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)
Tactic: simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
⊢ card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)
have rw : (↑P.parts : Set (Finset α)).PairwiseDisjoint (α := Finset (α × β)) fun (a : Finset α) ↦ interedges r a t
Tactic: rw [card_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)
have simp_rw : #(interedges r (P.parts.biUnion id) t) = ∑ a ∈ P.parts, #(interedges r a t)
Tactic: classical
  simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
simp_rw : #(interedges r (P.parts.biUnion id) t) = ∑ a ∈ P.parts, #(interedges r a t)
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)
have simp_rw₁ : card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r (id a) t) = ∑ a ∈ P.parts, #(interedges r a t)
Tactic: classical
  simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
simp_rw : #(interedges r (P.parts.biUnion id) t) = ∑ a ∈ P.parts, #(interedges r a t)
simp_rw₁ :
  card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r (id a) t) = ∑ a ∈ P.parts, #(interedges r a t)
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)
have simp_rw₂ : card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)
Tactic: classical
  simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
inst_1 : DecidableEq α
P : Finpartition s
t : Finset β
simp_rw : #(interedges r (P.parts.biUnion id) t) = ∑ a ∈ P.parts, #(interedges r a t)
simp_rw₁ :
  card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r (id a) t) = ∑ a ∈ P.parts, #(interedges r a t)
simp_rw₂ :
  card (α := α × β) (P.parts.biUnion fun (a : Finset α) ↦ interedges r a t) = ∑ a ∈ P.parts, #(interedges r a t)
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)
have simp_rw₃ : (↑P.parts : Set (Finset α)).PairwiseDisjoint (α := Finset (α × β)) fun (a : Finset α) ↦ interedges r a t
Tactic: classical
  simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)
have simp_rw : card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)
Tactic: simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
⊢ card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)
have rw : (↑P.parts : Set (Finset β)).PairwiseDisjoint (α := Finset (α × β)) fun (b : Finset β) ↦ interedges r s b
Tactic: rw [card_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
inst_1 : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)
have simp_rw : #(interedges r s (P.parts.biUnion id)) = ∑ 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)
have simp_rw₁ : card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s (id b)) = ∑ 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)
have simp_rw₂ : card (α := α × β) (P.parts.biUnion fun (b : Finset β) ↦ interedges r s b) = ∑ 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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)
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)
have simp_rw₃ : (↑P.parts : Set (Finset β)).PairwiseDisjoint (α := Finset (α × β)) fun (b : Finset β) ↦ 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ #(interedges r s t) = ∑ ab ∈ P.parts ×ˢ Q.parts, #(interedges r ab.1 ab.2)
have rw : Eq (α := ℕ) (∑ a ∈ P.parts, #(interedges r a t)) (∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))
Tactic: rw [card_interedges_finpartition_left _ P, sum_product]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ Eq (α := ℕ) (∑ a ∈ P.parts, #(interedges r a t)) (∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ 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)
have e_f : ∀ (x : Finset α), #(interedges r x t) = ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 α
⊢ #(interedges r x t) = ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
have e_f : Eq (α := ℕ) (∑ b ∈ Q.parts, #(interedges r x b)) (∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2))
Tactic: rw [card_interedges_finpartition_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) * edgeDensity r s₂ t₂ ≤
    edgeDensity r s₁ t₁
have hst : HMul.hMul (α := ℚ) (↑(#s₂) : ℚ) (↑(#t₂) : ℚ) ≠ 0
Tactic: have hst : (#s₂ : ℚ) * #t₂ ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) * edgeDensity r s₂ t₂ ≤
    edgeDensity r s₁ t₁
have rw : (↑(#(interedges r s₂ t₂)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ) ≤
  (↑(#(interedges r s₁ t₁)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ)
Tactic: rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel₀ hst]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₂)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ) ≤
    (↑(#(interedges r s₁ t₁)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s₁) : ℚ) (↑(#t₁) : ℚ)
have hab : interedges r s₂ t₂ ⊆ interedges r s₁ t₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)
have 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₁) : ℚ)
Tactic: refine (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)
have 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₂
Tactic: refine le_trans ?_ (mul_le_of_le_one_right ?_ (edgeDensity_le_one r s₂ t₂))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₂
⊢ 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₁) : ℚ)
have refine_2 : 0 ≤ 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₂))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)) *
      edgeDensity r s₂ t₂
have 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₂
Tactic: rw [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₂
⊢ 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₂
have 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₂
Tactic: rw [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)
have refine_2 : HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) ≤ 1
Tactic: refine sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
⊢ 0 ≤ 1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
have refine_2₁ : 0 ≤ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
Tactic: refine sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)
⊢ 0 ≤ 1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
have refine_2₂ : HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ) ≤ 1
Tactic: refine sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 ≤ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
have refine_2 : LE.le (α := ℚ) 0 (↑(#t₂) : ℚ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₂) : ℚ)
⊢ 0 ≤ HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)
have refine_2₁ : LE.le (α := ℚ) 0 (↑(#t₁) : ℚ)
Tactic: apply div_nonneg
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)
have refine : 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₂, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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₁) : ℚ)
have 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₁) : ℚ)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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
have rw : δ * δ ≤ 2 * δ
Tactic: rw [sub_nonneg, sq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
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 * δ
have hbc : δ ≤ 2
Tactic: gcongr