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
| (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
have rw : (1 + HPow.hPow (β := ℕ) ε 5 / 49) *
  (↑((↑(∑ ab ∈ ((chunk hP G ε hU).ofSubset hA sorry).parts ×ˢ ((chunk hP G ε hV).ofSubset hB sorry).parts,
              #(interedges G.Adj ab.1 ab.2)) :
          ℚ) /
        HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) :
    ℝ)
Tactic: rw [SimpleGraph.edgeDensity, edgeDensity, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl)]
-- 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
| (1 + HPow.hPow (β := ℕ) ε 5 / 49) *
    (↑((↑(∑ ab ∈ ((chunk hP G ε hU).ofSubset hA ⋯).parts ×ˢ ((chunk hP G ε hV).ofSubset hB ⋯).parts,
                #(interedges G.Adj ab.1 ab.2)) :
            ℚ) /
          HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) :
      ℝ)
have simp : ∑ x ∈ ((chunk hP G ε hU).ofSubset hA sorry).parts ×ˢ ((chunk hP G ε hV).ofSubset hB sorry).parts,
  (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
    ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ))
Tactic: simp only [cast_sum, mul_sum, sum_div, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) + _)]
-- 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
| (1 + HPow.hPow (β := ℕ) ε 5 / 49) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)
have rw : ∑ x ∈ ((chunk hP G ε hU).ofSubset hA sorry).parts ×ˢ ((chunk hP G ε hV).ofSubset hB sorry).parts,
  (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
    ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ))
Tactic: rw [SimpleGraph.edgeDensity, edgeDensity, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl)]
    simp only [cast_sum, mul_sum, sum_div, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) + _)]
-- 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 ∈ 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)) : ℝ)
have conv_rhs : LE.le (α := ℝ)
  (∑ x ∈ A.product B,
    (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) /
      ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))
  (∑ x ∈ ((chunk hP G ε hU).ofSubset hA sorry).parts ×ˢ ((chunk hP G ε hV).ofSubset hB sorry).parts,
    (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ)))
Tactic: conv_rhs =>
    rw [SimpleGraph.edgeDensity, edgeDensity, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl)]
    simp only [cast_sum, mul_sum, sum_div, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) + _)]
-- 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
⊢ LE.le (α := ℝ)
    (∑ x ∈ A.product B,
      (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) /
        ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))
    (∑ x ∈ ((chunk hP G ε hU).ofSubset hA ⋯).parts ×ˢ ((chunk hP G ε hV).ofSubset hB ⋯).parts,
      (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
        ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ)))
have push_cast : LE.le (α := ℝ)
  (∑ x ∈ A.product B,
    (↑(#(interedges G.Adj x.1 x.2)) : ℝ) /
      (HMul.hMul (α := ℝ) (↑(#x.1) : ℝ) (↑(#x.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))
  (∑ x ∈ ((chunk hP G ε hU).ofSubset hA sorry).parts ×ˢ ((chunk hP G ε hV).ofSubset hB sorry).parts,
    (↑(#(interedges G.Adj x.1 x.2)) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)))
Tactic: push_cast
-- 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
⊢ LE.le (α := ℝ)
    (∑ x ∈ A.product B,
      (↑(#(interedges G.Adj x.1 x.2)) : ℝ) /
        (HMul.hMul (α := ℝ) (↑(#x.1) : ℝ) (↑(#x.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))
    (∑ x ∈ ((chunk hP G ε hU).ofSubset hA ⋯).parts ×ˢ ((chunk hP G ε hV).ofSubset hB ⋯).parts,
      (↑(#(interedges G.Adj x.1 x.2)) : ℝ) *
        ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)))
have h : ∀ i ∈ A.product B,
  (↑(#(interedges G.Adj i.1 i.2)) : ℝ) /
      (HMul.hMul (α := ℝ) (↑(#i.1) : ℝ) (↑(#i.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)) ≤
    (↑(#(interedges G.Adj i.1 i.2)) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ))
Tactic: apply sum_le_sum
-- 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
⊢ ∀ i ∈ A.product B,
    (↑(#(interedges G.Adj i.1 i.2)) : ℝ) /
        (HMul.hMul (α := ℝ) (↑(#i.1) : ℝ) (↑(#i.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)) ≤
      (↑(#(interedges G.Adj i.1 i.2)) : ℝ) *
        ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ))
have h : ∀ (a b : Finset α),
  a ∈ A →
    b ∈ B →
      (↑(#(interedges G.Adj a b)) : ℝ) /
          (HMul.hMul (α := ℝ) (↑(#a) : ℝ) (↑(#b) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)) ≤
        (↑(#(interedges G.Adj a b)) : ℝ) *
          ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ))
Tactic: simp only [and_imp, Prod.forall, mem_product, show A.product B = A ×ˢ B by rfl]
-- 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
⊢ (↑(#(interedges G.Adj x y)) : ℝ) /
      (HMul.hMul (α := ℝ) (↑(#x) : ℝ) (↑(#y) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)) ≤
    (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ))
have h : (↑(#(interedges G.Adj x y)) : ℝ) ≤
  (↑(#(interedges G.Adj x y)) : ℝ) *
    ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)))
Tactic: rw [mul_mul_mul_comm, mul_comm (#x : ℝ), mul_comm (#y : ℝ), div_le_iff₀, 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
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 :
  (↑(#(interedges G.Adj x y)) : ℝ) ≤
    (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)))
⊢ (↑(#(interedges G.Adj x y)) : ℝ) /
      (HMul.hMul (α := ℝ) (↑(#x) : ℝ) (↑(#y) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)) ≤
    (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ))
have h₁ : 0 < HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
Tactic: rw [mul_mul_mul_comm, mul_comm (#x : ℝ), mul_comm (#y : ℝ), div_le_iff₀, 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
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
⊢ (↑(#(interedges G.Adj x y)) : ℝ) ≤
    (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)))
have h : 1 ≤
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
    (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
Tactic: refine le_mul_of_one_le_right (cast_nonneg _) ?_
-- 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
⊢ 1 ≤
    (1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
have h : HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
  (1 + HPow.hPow (β := ℕ) ε 5 / 49) *
    (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
Tactic: rw [div_mul_eq_mul_div, one_le_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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
h :
  HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    (1 + HPow.hPow (β := ℕ) ε 5 / 49) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
⊢ 1 ≤
    (1 + HPow.hPow (β := ℕ) ε 5 / 49) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
have h₁ : 0 < HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
Tactic: rw [div_mul_eq_mul_div, one_le_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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    (1 + HPow.hPow (β := ℕ) ε 5 / 49) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
have h : HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) 2 *
    (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) ?_)
-- 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 :
  HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) 2 *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    (1 + HPow.hPow (β := ℕ) ε 5 / 49) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
have h₁ : 0 ≤ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) ?_)
-- 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
⊢ HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) 2 *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))
have h : HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
  HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) *
    (HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)))
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
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
⊢ HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) *
      (HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)))
have h : (↑(#(A.sup id)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
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 :
  (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 : (↑(#(A.sup id)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) *
      (HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)))
have h₁ : (↑(#(B.sup id)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
Tactic: gcongr