awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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₂) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
Tactic: have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
    rw [sub_nonneg, sq]
    gcongr
    exact hδ₁.le.trans (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have hδ₂ : 0 < 1 - δ
Tactic: rw [← sub_pos] at hδ₁
Cleared hypotheses: hδ₁, hs₂, ht₂, hδ'
-- 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δ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have inl : ∀ (hs : ∅ ⊆ s₁) (hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(card.{u_4} (α := α) ∅) : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(edgeDensity r ∅ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
Tactic: obtain rfl | hs₂' := s₂.eq_empty_or_nonempty
Cleared hypotheses: s₂, hs, hs₂
-- 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δ₁ : 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
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have inr : ∀ (hs₂' : s₂.Nonempty),
  |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
Tactic: obtain rfl | hs₂' := s₂.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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} (α := α) ∅) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r ∅ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have hs₃ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ 0
Tactic: rw [Finset.card_empty, Nat.cast_zero] at hs₂
Cleared hypotheses: hs₂
-- 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δ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
hδ' : 0 ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
hs₂' : s₂.Nonempty
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have inr : ∀ (ht : ∅ ⊆ t₁) (ht₂ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(card.{u_5} (α := β) ∅) : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ ∅) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
Tactic: obtain rfl | ht₂' := t₂.eq_empty_or_nonempty
Cleared hypotheses: t₂, ht, ht₂
-- 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δ₁ : 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
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have inr₁ : ∀ (ht₂' : t₂.Nonempty),
  |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
Tactic: obtain rfl | ht₂' := t₂.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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} (α := β) ∅) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ ∅) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have ht₃ : (1 - δ) * (↑(#t₁) : 𝕜) ≤ 0
Tactic: rw [Finset.card_empty, Nat.cast_zero] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have hr : 2 * δ - HPow.hPow (β := ℕ) δ 2 = 1 - (1 - δ) * (1 - δ)
Tactic: have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by ring
-- 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δ₁ : 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 - δ)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ - HPow.hPow (β := ℕ) δ 2
have inr : |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 1 - (1 - δ) * (1 - δ)
Tactic: rw [hr]
-- 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δ₁ : 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 - δ)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 1 - (1 - δ) * (1 - δ)
have inr : (↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| : 𝕜) ≤ 1 - (1 - δ) * (1 - δ)
Tactic: norm_cast
-- 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δ₁ : 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 - δ)
have inr : (↑(1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)) : 𝕜) ≤
  1 - (1 - δ) * (1 - δ)
Tactic: refine
    (Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans ?_
-- 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δ₁ : 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 - δ)
⊢ (↑(1 - HDiv.hDiv (α := ℚ) (↑(#s₂) : ℚ) (↑(#s₁) : ℚ) * HDiv.hDiv (α := ℚ) (↑(#t₂) : ℚ) (↑(#t₁) : ℚ)) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
have inr : 1 - HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤ 1 - (1 - δ) * (1 - δ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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 - δ)
⊢ 1 - HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
have h₁ : s₁.Nonempty
Tactic: have h₁ := hs₂'.mono hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (hypothesis)
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
⊢ 1 - HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
have h₂ : t₁.Nonempty
Tactic: have h₂ := ht₂'.mono ht
-- 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δ₁ : 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₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
have inr : 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜)
Tactic: gcongr
-- 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δ₁ : 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₁) : 𝕜)
⊢ 1 - HDiv.hDiv (α := 𝕜) (↑(#s₂) : 𝕜) (↑(#s₁) : 𝕜) * HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜) ≤
    1 - (1 - δ) * (1 - δ)
have inr₁ : 1 - δ ≤ HDiv.hDiv (α := 𝕜) (↑(#t₂) : 𝕜) (↑(#t₁) : 𝕜)
Tactic: gcongr
-- 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δ₁ : 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₁) : 𝕜)
have inr : LT.lt.{u_1} (α := 𝕜) 0 (↑(#s₁) : 𝕜)
Tactic: refine (le_div_iff₀ ?_).2 hs₂
-- 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δ₁ : 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₁) : 𝕜)
have inr : LT.lt.{u_1} (α := 𝕜) 0 (↑(#t₁) : 𝕜)
Tactic: refine (le_div_iff₀ ?_).2 ht₂
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
have inl : ∀ (h : δ < 1), |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
Tactic: rcases lt_or_ge δ 1 with h | h
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
inl : ∀ (h : δ < 1), |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
have inr : ∀ (h : 1 ≤ δ), |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
Tactic: rcases lt_or_ge δ 1 with h | h
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ 2 * δ
have inr : |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ δ + δ
Tactic: rw [two_mul]
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ δ + δ
have inr : LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₂ t₂) : 𝕜)| 1
Tactic: refine (abs_sub _ _).trans (add_le_add (le_trans ?_ h) (le_trans ?_ h))
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₂ t₂) : 𝕜)| 1
⊢ |HSub.hSub (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜)| ≤ δ + δ
have inr₁ : LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₁ t₁) : 𝕜)| 1
Tactic: refine (abs_sub _ _).trans (add_le_add (le_trans ?_ h) (le_trans ?_ h))
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₂ t₂) : 𝕜)| 1
have inr : LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) 1
Tactic: rw [abs_of_nonneg]
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₂ t₂) : 𝕜) 1
⊢ LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₂ t₂) : 𝕜)| 1
have inr₁ : LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₂ t₂) : 𝕜)
Tactic: rw [abs_of_nonneg]
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
⊢ LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₁ t₁) : 𝕜)| 1
have inr : LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜) 1
Tactic: rw [abs_of_nonneg]
-- 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 ≤ δ
hscard : (1 - δ) * (↑(#s₁) : 𝕜) ≤ (↑(#s₂) : 𝕜)
htcard : (1 - δ) * (↑(#t₁) : 𝕜) ≤ (↑(#t₂) : 𝕜)
h : 1 ≤ δ
inr : LE.le.{u_1} (α := 𝕜) (↑(edgeDensity r s₁ t₁) : 𝕜) 1
⊢ LE.le.{u_1} (α := 𝕜) |(↑(edgeDensity r s₁ t₁) : 𝕜)| 1
have inr₁ : LE.le.{u_1} (α := 𝕜) 0 (↑(edgeDensity r s₁ t₁) : 𝕜)
Tactic: rw [abs_of_nonneg]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
⊢ x.swap ∈ interedges r s t ↔ x ∈ interedges r t s
have rw : x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2
Tactic: rw [mem_interedges_iff, mem_interedges_iff, hr.iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
hr : Symmetric r
s t : Finset α
⊢ edgeDensity r s t = edgeDensity r t s
have rw : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) = edgeDensity r t s
Tactic: rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
hr : Symmetric r
s t : Finset α
rw : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) = edgeDensity r t s
⊢ edgeDensity r s t = edgeDensity r t s
have rw₁ : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
Tactic: rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
hr : Symmetric r
s t : Finset α
rw : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) = edgeDensity r t s
rw₁ : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
⊢ edgeDensity r s t = edgeDensity r t s
have rw₂ : (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
Tactic: rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
r : α → α → Prop
inst : DecidableRel r
hr : Symmetric r
s t : Finset α
rw : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑(#t) : ℚ) = edgeDensity r t s
rw₁ : (↑(#(interedges r s t)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
rw₂ : (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) = edgeDensity r t s
⊢ edgeDensity r s t = edgeDensity r t s
have rw₃ : (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ) =
  (↑(#(interedges r t s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#t) : ℚ) (↑(#s) : ℚ)
Tactic: rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Density (goal)
Goal:
α : Type u_4
G : SimpleGraph α
inst : DecidableRel G.Adj
s t : Finset α
inst_1 : DecidableEq α
h : Disjoint s t
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t
have rw : #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #({e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2}) = #(s ×ˢ t)
Tactic: rw [← card_product, interedges_def, interedges_def]