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
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)
have sz_positivity : 0 < m → LT.lt (α := ℝ) 0 (↑m : ℝ)
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
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)
have sz_positivity₄ : 0 < m → 0 < ε → LT.lt (α := ℝ) 0 (↑m : ℝ)
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
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
have h : 0 < #(A.sup id) * #(B.sup id)
Tactic: rw [← cast_mul, cast_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
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id) * #(B.sup id)
have h : 0 < #(A.sup id)
Tactic: apply 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
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h : 0 < #(A.sup id)
⊢ 0 < #(A.sup id) * #(B.sup id)
have h₁ : 0 < #(B.sup id)
Tactic: apply 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
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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id)
have h : ∃ x ∈ A, (id x).Nonempty
Tactic: rw [Finset.card_pos, sup_eq_biUnion, biUnion_nonempty]
-- 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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(B.sup id)
have h : ∃ x ∈ B, (id x).Nonempty
Tactic: rw [Finset.card_pos, sup_eq_biUnion, biUnion_nonempty]
-- 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
⊢ |(∑ 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 rw : (∑ 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 ∧
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 49
Tactic: rw [abs_sub_le_iff]
-- 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
⊢ (∑ 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 ∧
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
        (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
      HPow.hPow (β := ℕ) ε 5 / 49
have left : (∑ 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
Tactic: constructor
-- 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
left :
  (∑ 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
⊢ (∑ 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 ∧
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
        (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
      HPow.hPow (β := ℕ) ε 5 / 49
have right : (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
    (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
  HPow.hPow (β := ℕ) ε 5 / 49
Tactic: constructor
-- 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
⊢ (∑ 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 left : (∑ 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
Tactic: rw [sub_le_iff_le_add']
-- 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 :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 49
have apply : HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
Tactic: apply this.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
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 :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have hc : 0 ≤ HPow.hPow (β := ℕ) ε 5
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
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 :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
hc : 0 ≤ HPow.hPow (β := ℕ) ε 5
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have hdb : LE.le (α := ℝ) 49 50
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
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 :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5
have hc : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5
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
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
hc hc₁ hc₂ hc₃ : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5
have hc₄ : 0 < m → 0 < ε → 0 ≤ HPow.hPow (β := ℕ) ε 5
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
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have hc : 0 ≤ HPow.hPow (β := ℕ) ε 5
Tactic: gcongr <;> [sz_positivity; norm_num]