awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
refine :
  (1 - 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) : ℝ)
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
refine this.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
simp :
  ∑ x ∈ A.product B,
    (↑(↑(#(G.interedges x.1 x.2)) : ℚ) : ℝ) /
      ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))
| (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
simp only [SimpleGraph.edgeDensity_def, sum_div, Rat.cast_div, div_div]

Premises used: SimpleGraph.edgeDensity_def, Rat.cast_div, Finset.sum_div, div_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
conv_rhs :
  (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    ∑ x ∈ A.product B,
      (↑(↑(#(G.interedges x.1 x.2)) : ℚ) : ℝ) /
        ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))
⊢ (1 - 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) : ℝ)

Tactic:
conv_rhs => -- Porting note: LHS and RHS need separate treatment to get the desired form
    simp only [SimpleGraph.edgeDensity_def, sum_div, Rat.cast_div, div_div]

Premises used: SimpleGraph.edgeDensity_def, Rat.cast_div, Finset.sum_div, div_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
rw :
  (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
    (↑((↑(∑ ab ∈ A ×ˢ B, #(interedges G.Adj ab.1 ab.2)) : ℚ) /
          HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) :
      ℝ)
| (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)

Tactic:
rw [SimpleGraph.edgeDensity_def, SimpleGraph.interedges, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl), ofSubset_parts,
      ofSubset_parts]

Premises used: Finpartition.ofSubset_parts, SimpleGraph.edgeDensity_def, Rel.card_interedges_finpartition, Finpartition.ofSubset, Finset.sup_eq_biUnion, rfl, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
simp :
  ∑ x ∈ A ×ˢ B,
    (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
      ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ))
| (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
    (↑((↑(∑ ab ∈ A ×ˢ B, #(interedges G.Adj ab.1 ab.2)) : ℚ) /
          HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) :
      ℝ)

Tactic:
simp only [cast_sum, sum_div, mul_sum, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) - _)]

Premises used: Finset.mul_sum, HSub.hSub, Rat.cast_div, Finset.sum_div, Nat.cast_sum, Rat.cast_sum, OfNat.ofNat, mul_div_left_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
rw :
  ∑ x ∈ A ×ˢ B,
    (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
      ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ))
| (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ)

Tactic:
rw [SimpleGraph.edgeDensity_def, SimpleGraph.interedges, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl), ofSubset_parts,
      ofSubset_parts]
    simp only [cast_sum, sum_div, mul_sum, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) - _)]

Premises used: Finpartition.ofSubset_parts, Finset.mul_sum, SimpleGraph.edgeDensity_def, Rel.card_interedges_finpartition, HSub.hSub, Finpartition.ofSubset, Rat.cast_div, Finset.sup_eq_biUnion, Finset.sum_div, Nat.cast_sum, Rat.cast_sum, OfNat.ofNat, mul_div_left_comm, rfl, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
conv_lhs :
  LE.le (α := ℝ)
    (∑ x ∈ A ×ˢ B,
      (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
        ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ)))
    (∑ x ∈ A.product B,
      (↑(↑(#(G.interedges x.1 x.2)) : ℚ) : ℝ) /
        ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) * (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    ∑ x ∈ A.product B,
      (↑(↑(#(G.interedges x.1 x.2)) : ℚ) : ℝ) /
        ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))

Tactic:
conv_lhs =>
    rw [SimpleGraph.edgeDensity_def, SimpleGraph.interedges, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl), ofSubset_parts,
      ofSubset_parts]
    simp only [cast_sum, sum_div, mul_sum, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) - _)]

Premises used: Finpartition.ofSubset_parts, Finset.mul_sum, SimpleGraph.edgeDensity_def, Rel.card_interedges_finpartition, HSub.hSub, Finpartition.ofSubset, Rat.cast_div, Finset.sup_eq_biUnion, Finset.sum_div, Nat.cast_sum, Rat.cast_sum, OfNat.ofNat, mul_div_left_comm, rfl, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
push_cast :
  LE.le (α := ℝ)
    (∑ x ∈ A ×ˢ B,
      (↑(#(interedges G.Adj x.1 x.2)) : ℝ) *
        ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)))
    (∑ x ∈ A.product B,
      (↑(#(G.interedges x.1 x.2)) : ℝ) /
        (HMul.hMul (α := ℝ) (↑(#x.1) : ℝ) (↑(#x.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))
⊢ LE.le (α := ℝ)
    (∑ x ∈ A ×ˢ B,
      (↑(↑(#(interedges G.Adj x.1 x.2)) : ℚ) : ℝ) *
        ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / (↑(HMul.hMul (α := ℚ) (↑(#(A.sup id)) : ℚ) (↑(#(B.sup id)) : ℚ)) : ℝ)))
    (∑ x ∈ A.product B,
      (↑(↑(#(G.interedges x.1 x.2)) : ℚ) : ℝ) /
        ((↑(HMul.hMul (α := ℚ) (↑(#x.1) : ℚ) (↑(#x.2) : ℚ)) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
h :
  ∀ i ∈ A ×ˢ B,
    (↑(#(interedges G.Adj i.1 i.2)) : ℝ) *
        ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)) ≤
      (↑(#(G.interedges i.1 i.2)) : ℝ) /
        (HMul.hMul (α := ℝ) (↑(#i.1) : ℝ) (↑(#i.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))
⊢ LE.le (α := ℝ)
    (∑ x ∈ A ×ˢ B,
      (↑(#(interedges G.Adj x.1 x.2)) : ℝ) *
        ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)))
    (∑ x ∈ A.product B,
      (↑(#(G.interedges x.1 x.2)) : ℝ) /
        (HMul.hMul (α := ℝ) (↑(#x.1) : ℝ) (↑(#x.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)))

Tactic:
apply sum_le_sum

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
h :
  ∀ (a b : Finset α),
    a ∈ A →
      b ∈ B →
        (↑(#(interedges G.Adj a b)) : ℝ) *
            ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)) ≤
          (↑(#(G.interedges a b)) : ℝ) /
            (HMul.hMul (α := ℝ) (↑(#a) : ℝ) (↑(#b) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))
⊢ ∀ i ∈ A ×ˢ B,
    (↑(#(interedges G.Adj i.1 i.2)) : ℝ) *
        ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)) ≤
      (↑(#(G.interedges i.1 i.2)) : ℝ) /
        (HMul.hMul (α := ℝ) (↑(#i.1) : ℝ) (↑(#i.2) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))

Tactic:
simp only [and_imp, Prod.forall, mem_product]

Premises used: and_imp, Prod.forall, Finset.mem_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 :
  (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))) ≤
    (↑(#(G.interedges x y)) : ℝ)
h₁ : 0 < HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)
⊢ (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)) ≤
    (↑(#(G.interedges x y)) : ℝ) /
      (HMul.hMul (α := ℝ) (↑(#x) : ℝ) (↑(#y) : ℝ) * HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ))

Tactic:
rw [mul_mul_mul_comm, mul_comm (#x : ℝ), mul_comm (#y : ℝ), le_div_iff₀, mul_assoc]

Premises used: mul_mul_mul_comm, mul_assoc, Nat.cast, mul_comm, Finset.card, le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
⊢ (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))) ≤
    (↑(#(G.interedges x y)) : ℝ)

Tactic:
mul_le_of_le_one_right (cast_nonneg _) ?_

Premises used: Nat.cast_nonneg, mul_le_of_le_one_right, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 :
  (1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    1
⊢ (↑(#(interedges G.Adj x y)) : ℝ) *
      ((1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ))) ≤
    (↑(#(G.interedges x y)) : ℝ)

Tactic:
refine mul_le_of_le_one_right (cast_nonneg _) ?_

Premises used: Nat.cast_nonneg, mul_le_of_le_one_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 :
  (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) /
      HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    1
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) / HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    1

Tactic:
rw [div_mul_eq_mul_div, ← mul_assoc, mul_assoc]

Premises used: mul_assoc, div_mul_eq_mul_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 :
  (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
      (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ)
⊢ (1 - HPow.hPow (β := ℕ) ε 5 / 50) *
        (HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#x) : ℝ) * HMul.hMul (α := ℝ) (↑(#B) : ℝ) (↑(#y) : ℝ)) /
      HMul.hMul (α := ℝ) (↑(#(A.sup id)) : ℝ) (↑(#(B.sup id)) : ℝ) ≤
    1

Tactic:
refine div_le_one_of_le₀ ?_ (by positivity)

Premises used: div_le_one_of_le₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)

Tactic:
(mul_le_mul_of_nonneg_right (one_sub_le_m_div_m_add_one_sq hPα hPε) ?_).trans ?_

Premises used: _private.0.SzemerediRegularity.one_sub_le_m_div_m_add_one_sq, mul_le_mul_of_nonneg_right, LE.le.trans