awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    1
have h : (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) /
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
  1
Tactic: rw [div_mul_eq_mul_div, ← mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) /
      HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    1
have h : (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
    (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
  HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
Tactic: refine div_le_one_of_le₀ ?_ (by positivity)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
have h : 0 ≤ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
Tactic: refine (mul_le_mul_of_nonneg_right (one_sub_le_m_div_m_add_one_sq hPα hPε) ?_).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h : 0 ≤ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
have h₁ : HPow.hPow (β := ℕ) ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2 *
    (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
  HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
Tactic: refine (mul_le_mul_of_nonneg_right (one_sub_le_m_div_m_add_one_sq hPα hPε) ?_).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ HPow.hPow (β := ℕ) ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) 2 *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
have h : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) *
    (HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)) ≤
  HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
Tactic: rw [sq, mul_mul_mul_comm, mul_comm ((m : ℝ) / _), mul_comm ((m : ℝ) / _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) *
      (HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)) ≤
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
have h : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) ≤ (↑(#(A.sup id)) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) ≤ (↑(#(A.sup id)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) *
      (HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)) ≤
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
have h₁ : HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * ((↑m : ℝ) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) ≤ (↑(#(B.sup id)) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
have h : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
Tactic: refine mul_pos (mul_pos ?_ ?_) (mul_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
have h₁ : LT.lt (α := ℝ) 0 (↑(#x) : ℝ)
Tactic: refine mul_pos (mul_pos ?_ ?_) (mul_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
h₁ : LT.lt (α := ℝ) 0 (↑(#x) : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
have h₂ : LT.lt (α := ℝ) 0 (↑(#B) : ℝ)
Tactic: refine mul_pos (mul_pos ?_ ?_) (mul_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
h₁ : LT.lt (α := ℝ) 0 (↑(#x) : ℝ)
h₂ : LT.lt (α := ℝ) 0 (↑(#B) : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
have h₃ : LT.lt (α := ℝ) 0 (↑(#y) : ℝ)
Tactic: refine mul_pos (mul_pos ?_ ?_) (mul_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
have h : A.Nonempty
Tactic: rw [cast_pos, Finset.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ LT.lt (α := ℝ) 0 (↑(#x) : ℝ)
have h : x.Nonempty
Tactic: rw [cast_pos, Finset.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ LT.lt (α := ℝ) 0 (↑(#B) : ℝ)
have h : B.Nonempty
Tactic: rw [cast_pos, Finset.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ LT.lt (α := ℝ) 0 (↑(#y) : ℝ)
have h : y.Nonempty
Tactic: rw [cast_pos, Finset.card_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
have rw : HPow.hPow (β := ℕ) ε 5 / 49 * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 49
Tactic: rw [add_mul, one_mul, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have sz_positivity : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5 / 49
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5 / 49
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have sz_positivity₄ : 0 < m → 0 < ε → 0 ≤ HPow.hPow (β := ℕ) ε 5 / 49
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ HPow.hPow (β := ℕ) ε 5 / 49 * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 49
have refine : LE.le (α := ℝ) (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) 1
Tactic: refine mul_le_of_le_one_right (by sz_positivity) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
have this : (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
Tactic: have : (↑1 + ε ^ 5 / ↑49) * G.edgeDensity (A.biUnion id) (B.biUnion id) ≤
      G.edgeDensity (A.biUnion id) (B.biUnion id) + ε ^ 5 / 49 := by
    rw [add_mul, one_mul, add_le_add_iff_left]
    refine mul_le_of_le_one_right (by sz_positivity) ?_
    exact mod_cast G.edgeDensity_le_one _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
⊢ (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
have refine : (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
Tactic: refine le_trans ?_ this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
| (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
have simp : ∑ x ∈ A.product B,
  (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) /
    ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))
Tactic: simp only [SimpleGraph.edgeDensity, edgeDensity, sum_div, Rat.cast_div, div_div]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
⊢ (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
have conv_lhs : ∑ x ∈ A.product B,
    (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) /
      ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)) ≤
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
Tactic: conv_lhs => -- Porting note: LHS and RHS need separate treatment to get the desired form
    simp only [SimpleGraph.edgeDensity, edgeDensity, sum_div, Rat.cast_div, div_div]