awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
calc_2 :
  ∀ x ∈ P.parts.offDiag, (fun (i : Finset α × Finset α) ↦ #i.1 * #i.2) x ≤ HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2
⊢ ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 2
have calc_2₁ : #P.parts.offDiag • HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
  HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2
Tactic: calc
    (_ : ℕ) ≤ _ := sum_le_card_nsmul P.parts.offDiag (fun i ↦ #i.1 * #i.2)
            ((#A / #P.parts + 1) ^ 2 : ℕ) ?_
    _ ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 := ?_
    _ ≤ _ := by gcongr; apply Nat.mul_div_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∀ x ∈ P.parts.offDiag, (fun (i : Finset α × Finset α) ↦ #i.1 * #i.2) x ≤ HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2
have calc_2 : ∀ (a b : Finset α), a ∈ P.parts → b ∈ P.parts → a ≠ b → #a * #b ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)
Tactic: simp only [Prod.forall, and_imp, mem_offDiag, sq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts.offDiag • HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2
have calc_2 : HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2 - #P.parts * HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
  HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2
Tactic: rw [smul_eq_mul, offDiag_card, Nat.mul_sub_right_distrib, ← sq, ← mul_pow, mul_add_one (α := ℕ)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
have hbc : #P.parts ≤ #A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (↑(card (α := α × α)
          ((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => G.interedges U V)) :
      𝕜) ≤
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have _ : ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
Tactic: calc
    _ ≤ _ := hP.card_interedges_sparsePairs_le' hε
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
_ :
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
⊢ (↑(card (α := α × α)
          ((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => G.interedges U V)) :
      𝕜) ≤
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have _₁ : ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2 =
  4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
Tactic: calc
    _ ≤ _ := hP.card_interedges_sparsePairs_le' hε
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < HPow.hPow (β := ℕ) j 2
have rw : j * (j - 1) < j * j
Tactic: rw [sq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) * HPow.hPow (β := ℕ) (i / j + 1) 2 < HPow.hPow (β := ℕ) (i + j) 2
have this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
Tactic: have : j * (j - 1) < j ^ 2 := by
    rw [sq]; exact Nat.mul_lt_mul_of_pos_left (Nat.sub_lt hj zero_lt_one) hj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
⊢ j * (j - 1) * HPow.hPow (β := ℕ) (i / j + 1) 2 < HPow.hPow (β := ℕ) (i + j) 2
have apply : HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (i / j).succ 2 ≤ HPow.hPow (β := ℕ) (i + j) 2
Tactic: apply (Nat.mul_lt_mul_of_pos_right this <| pow_pos Nat.succ_pos' _).trans_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
⊢ HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (i / j).succ 2 ≤ HPow.hPow (β := ℕ) (i + j) 2
have rw : HPow.hPow (β := ℕ) (j * (i / j) + j) 2 ≤ HPow.hPow (β := ℕ) (i + j) 2
Tactic: rw [← mul_pow, Nat.mul_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
⊢ HPow.hPow (β := ℕ) (j * (i / j) + j) 2 ≤ HPow.hPow (β := ℕ) (i + j) 2
have hab : j * (i / j) ≤ i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
have inl : ∀ (h : P.parts = ∅),
  (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
Tactic: obtain h | h := P.parts.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
inl :
  ∀ (h : P.parts = ∅),
    (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
      (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
have inr : ∀ (h : P.parts.Nonempty),
  (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
Tactic: obtain h | h := P.parts.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ (↑(#P.parts) : 𝕜) * HMul.hMul (α := 𝕜) (↑(#A / #P.parts) : 𝕜) (↑(#A / #P.parts + 1) : 𝕜) =
    HMul.hMul (α := 𝕜) (↑(#P.parts) : 𝕜) (↑(#A / #P.parts) : 𝕜) * (↑(#A / #P.parts + 1) : 𝕜)
have rw : (↑(#P.parts) : 𝕜) * HMul.hMul (α := 𝕜) (↑(#A / #P.parts) : 𝕜) (↑(#A / #P.parts + 1) : 𝕜) =
  (↑(#P.parts) : 𝕜) * HMul.hMul (α := 𝕜) (↑(#A / #P.parts) : 𝕜) (↑(#A / #P.parts + 1) : 𝕜)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ (↑(#A) : 𝕜) * (HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1) =
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
have rw : (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)) =
  (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
Tactic: rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
rw :
  (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)) =
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
⊢ (↑(#A) : 𝕜) * (HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1) =
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
have rw₁ : (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)) =
  (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜))
Tactic: rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
have inr : (↑(#A / #P.parts + 1) : 𝕜) ≤ HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1
Tactic: calc
    _ ≤ (#P.parts : 𝕜) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) :=
        mod_cast card_biUnion_le_card_mul _ _ _ fun U hU ↦ ?_
    _ = #P.parts * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1) := by rw [mul_assoc]
    _ ≤ #A * (#A / #P.parts + 1) :=
        mul_le_mul (mod_cast Nat.mul_div_le _ _) ?_ (by positivity) (by positivity)
    _ = _ := by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
inr : (↑(#A / #P.parts + 1) : 𝕜) ≤ HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
have inr₁ : ∀ (U : Finset α) (hU : U ∈ P.parts), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
Tactic: calc
    _ ≤ (#P.parts : 𝕜) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) :=
        mod_cast card_biUnion_le_card_mul _ _ _ fun U hU ↦ ?_
    _ = #P.parts * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1) := by rw [mul_assoc]
    _ ≤ #A * (#A / #P.parts + 1) :=
        mul_le_mul (mod_cast Nat.mul_div_le _ _) ?_ (by positivity) (by positivity)
    _ = _ := by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
have rwa : ∀ (this : #U * #U - 1 * #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
Tactic: rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
rwa :
  ∀ (this : #U * #U - 1 * #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
have rwa₁ : ∀ (this : #U * #U - #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
Tactic: rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
rwa :
  ∀ (this : #U * #U - 1 * #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
rwa₁ : ∀ (this : #U * #U - #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
have rwa₂ : ∀ (this : #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
Tactic: rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
have inr : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
Tactic: suffices (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1) by
    rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
have this : #U ≤ #A / #P.parts + 1
Tactic: have := hP.card_part_le_average_add_one hU
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U ≤ #A / #P.parts + 1
⊢ (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
have inr : #A / #P.parts + 1 - 1 ≤ #A / #P.parts
Tactic: refine Nat.mul_le_mul ((Nat.sub_le_sub_right this 1).trans ?_) this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have inl : ∀ {P : Finpartition (α := Finset α) ⊥} (hP : P.IsEquipartition) (hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)),
  (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(card.{u_1} (α := α) ⊥) : 𝕜) 2
Tactic: obtain rfl | hA : A = ⊥ ∨ _ := A.eq_empty_or_nonempty
Cleared hypotheses: A, P, hP, hP'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
inl :
  ∀ {P : Finpartition (α := Finset α) ⊥} (hP : P.IsEquipartition) (hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)),
    (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(card.{u_1} (α := α) ⊥) : 𝕜) 2
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have inr : ∀ (hA : A.Nonempty), (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
Tactic: obtain rfl | hA : A = ⊥ ∨ _ := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have inr : (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜) ≤
  ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
Tactic: apply hP.card_biUnion_offDiag_le'.trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
have inr : (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤
  ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
Tactic: rw [div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
have rw : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)
have bc : #P.parts ≤ #A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
have this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
Tactic: have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
    rw [two_mul]; gcongr; exact P.card_parts_le_card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
⊢ (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
have inr : (↑(#A) : 𝕜) * HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
Tactic: refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
⊢ (↑(#A) : 𝕜) * HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
have rw : 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
Tactic: rw [mul_left_comm, ← sq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
⊢ 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
have h : 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 = 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * 1
Tactic: convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
h : 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 = 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * 1
⊢ 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
have h₁ : ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜) =
  2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (ε / 4 * (↑(#P.parts) : 𝕜))
Tactic: convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
⊢ (↑(#A) : 𝕜) * HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
have inr : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
Tactic: suffices 1 ≤ ε / 4 * #P.parts by
    rw [mul_left_comm, ← sq]
    convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> ring