awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∀
    (x :
      ↥({x ∈ P.parts.attach |
          ¬#(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})),
    Membership.mem (γ :=
        Finset
          ↥({x ∈ P.parts.attach |
              ¬#(↑x : Finset α) =
                  m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}))
        univ x →
      #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)) =
        HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1)

Tactic:
exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

Premises used: LT.lt.ne', Finpartition.card_parts_equitabilise, Nat.div_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∀
    (x :
      ↥({x ∈ P.parts.attach |
          #(↑x : Finset α) =
            m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})),
    Membership.mem (γ :=
        Finset
          ↥({x ∈ P.parts.attach |
              #(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}))
        univ x →
      #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)) =
        HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)

Tactic:
fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

Premises used: Finset.sum_apply_dite._proof_1, LT.lt.ne', Finpartition.card_parts_equitabilise, Finpartition.atomise, Finpartition.nonuniformWitnesses, Subtype.val, Nat.div_pos, SzemerediRegularity.card_aux₁
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∀
    (x :
      ↥({x ∈ P.parts.attach |
          #(↑x : Finset α) =
            m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})),
    Membership.mem (γ :=
        Finset
          ↥({x ∈ P.parts.attach |
              #(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}))
        univ x →
      #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)) =
        HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)

Tactic:
exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

Premises used: LT.lt.ne', Finpartition.card_parts_equitabilise, Nat.div_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
rw :
  (#({x ∈ P.parts.attach |
            #(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) +
        #({x ∈ P.parts.attach |
            ¬#(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})) *
      HPow.hPow (α := ℕ) 4 #P.parts =
    stepBound #P.parts
⊢ #({x ∈ P.parts.attach |
            #(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) *
        (HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)) +
      #({x ∈ P.parts.attach |
            ¬#(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) *
        (HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1)) =
    stepBound #P.parts

Tactic:
rw [Nat.sub_add_cancel a_add_one_le_four_pow_parts_card,
    Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), ← add_mul]

Premises used: add_mul, SzemerediRegularity.a_add_one_le_four_pow_parts_card, Nat.le_succ, Nat.sub_add_cancel, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
e_a :
  #({x ∈ P.parts.attach |
          #(↑x : Finset α) =
            m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) +
      #({x ∈ P.parts.attach |
          ¬#(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) =
    #P.parts
⊢ (#({x ∈ P.parts.attach |
            #(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) +
        #({x ∈ P.parts.attach |
            ¬#(↑x : Finset α) =
                m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})) *
      HPow.hPow (α := ℕ) 4 #P.parts =
    stepBound #P.parts

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
e_a : #P.parts.attach = #P.parts
e_a₁ e_a₂ : #P.parts = #P.parts
⊢ #({x ∈ P.parts.attach |
          #(↑x : Finset α) =
            m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) +
      #({x ∈ P.parts.attach |
          ¬#(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}) =
    #P.parts

Tactic:
rw [card_filter_add_card_filter_not, card_attach]

Premises used: Finset.card_filter_add_card_filter_not, Finset.card_attach
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
simp_rw : ∃ (b : ℕ), ∀ a ∈ (↑(increment hP G ε).parts : Set (Finset α)), #a = b ∨ #a = b + 1
⊢ (increment hP G ε).IsEquipartition

Tactic:
simp_rw [IsEquipartition, Set.equitableOn_iff_exists_eq_eq_add_one]

Premises used: Set.equitableOn_iff_exists_eq_eq_add_one, Finpartition.IsEquipartition
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
⊢ ∃ (b : ℕ), ∀ a ∈ (↑(increment hP G ε).parts : Set (Finset α)), #a = b ∨ #a = b + 1

Tactic:
⟨m, fun A hA => ?_⟩

Premises used: SzemerediRegularity.stepBound, Fintype.card, HDiv.hDiv, Finpartition.parts, Exists.intro, Finset.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
refine : ∀ (A : Finset α) (hA : A ∈ (↑(increment hP G ε).parts : Set (Finset α))), #A = m ∨ #A = m + 1
⊢ ∃ (b : ℕ), ∀ a ∈ (↑(increment hP G ε).parts : Set (Finset α)), #a = b ∨ #a = b + 1

Tactic:
refine ⟨m, fun A hA => ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : A ∈ (↑(increment hP G ε).parts : Set (Finset α))
⊢ ∃ (A_1 : Finset α) (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts

Tactic:
rw [mem_coe, increment, mem_bind] at hA

Premises used: SzemerediRegularity.increment, Finpartition.mem_bind, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
A : Finset α
hA : ∃ (A_1 : Finset α) (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts
obtain : ∀ (U : Finset α) (hU : U ∈ P.parts) (hA : A ∈ (chunk hP G ε hU).parts), #A = m ∨ #A = m + 1
⊢ #A = m ∨ #A = m + 1

Tactic:
obtain ⟨U, hU, hA⟩ := hA
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
A U : Finset α
hU : U ∈ P.parts
hA : A ∈ (chunk hP G ε hU).parts
⊢ #A = m ∨ #A = m + 1

Tactic:
card_eq_of_mem_parts_chunk hA

Premises used: SzemerediRegularity.card_eq_of_mem_parts_chunk
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
A U : Finset α
hU : U ∈ P.parts
hA : A ∈ (chunk hP G ε hU).parts
⊢ #A = m ∨ #A = m + 1

Tactic:
exact card_eq_of_mem_parts_chunk hA

Premises used: SzemerediRegularity.card_eq_of_mem_parts_chunk
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
simp :
  ∀ (x x_1 : Finset α) (x_2 : x ∈ P.parts ∧ x_1 ∈ P.parts ∧ ¬x = x_1),
    Ui ∈ (chunk hP G ε ⋯).parts →
      Vj ∈ (chunk hP G ε ⋯).parts →
        (∃ (a : Finset α) (h : a ∈ P.parts), Ui ∈ parts (a := a) (chunk hP G ε ⋯ : Finpartition a)) ∧
          (∃ (a : Finset α) (h : a ∈ P.parts), Vj ∈ parts (a := a) (chunk hP G ε ⋯ : Finpartition a)) ∧ ¬Ui = Vj
⊢ (Ui, Vj) ∈ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) → (Ui, Vj) ∈ (increment hP G ε).parts.offDiag

Tactic:
simp only [distinctPairs, increment, mem_offDiag, bind_parts, mem_biUnion, Prod.exists,
    mem_product, mem_attach, true_and, Subtype.exists, and_imp,
    mem_offDiag, forall_exists_index, Ne]

Premises used: and_imp, Finset.mem_attach, Subtype.exists, forall_exists_index, Finpartition.bind_parts, Ne, SzemerediRegularity.increment, Finset.mem_offDiag, _private.0.SzemerediRegularity.distinctPairs, Prod.exists, Finset.mem_product, Finset.mem_biUnion, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
⊢ ∀ (x x_1 : Finset α) (x_2 : x ∈ P.parts ∧ x_1 ∈ P.parts ∧ ¬x = x_1),
    Ui ∈ (chunk hP G ε ⋯).parts →
      Vj ∈ (chunk hP G ε ⋯).parts →
        (∃ (a : Finset α) (h : a ∈ P.parts), Ui ∈ parts (a := a) (chunk hP G ε ⋯ : Finpartition a)) ∧
          (∃ (a : Finset α) (h : a ∈ P.parts), Vj ∈ parts (a := a) (chunk hP G ε ⋯ : Finpartition a)) ∧ ¬Ui = Vj

Tactic:
fun U V hUV hUi hVj => ⟨⟨_, hUV.1, hUi⟩, ⟨_, hUV.2.1, hVj⟩, ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
refine :
  ∀ (U V : Finset α) (hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V) (hUi : Ui ∈ (chunk hP G ε ⋯).parts)
    (hVj : Vj ∈ (chunk hP G ε ⋯).parts), ¬Ui = Vj
⊢ ∀ (x x_1 : Finset α) (x_2 : x ∈ P.parts ∧ x_1 ∈ P.parts ∧ ¬x = x_1),
    Ui ∈ (chunk hP G ε ⋯).parts →
      Vj ∈ (chunk hP G ε ⋯).parts →
        (∃ (a : Finset α) (h : a ∈ P.parts), Ui ∈ parts (a := a) (chunk hP G ε ⋯ : Finpartition a)) ∧
          (∃ (a : Finset α) (h : a ∈ P.parts), Vj ∈ parts (a := a) (chunk hP G ε ⋯ : Finpartition a)) ∧ ¬Ui = Vj

Tactic:
refine fun U V hUV hUi hVj => ⟨⟨_, hUV.1, hUi⟩, ⟨_, hUV.2.1, hVj⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
Ui U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V
hUi : Ui ∈ (chunk hP G ε ⋯).parts
hVj : Ui ∈ (chunk hP G ε ⋯).parts
obtain : ∀ (i : α) (hi : i ∈ Ui), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := nonempty_of_mem_parts _ hUi

Premises used: Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
Ui U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V
hUi : Ui ∈ (chunk hP G ε ⋯).parts
hVj : Ui ∈ (chunk hP G ε ⋯).parts
i : α
hi : i ∈ Ui
⊢ False

Tactic:
hUV.2.2 (P.disjoint.elim_finset hUV.1 hUV.2.1 i (Finpartition.le _ hUi hi) <|
    Finpartition.le _ hVj hi)

Premises used: Finpartition.disjoint, And.right, And.left, Finpartition.le, Set.PairwiseDisjoint.elim_finset
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
Ui U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V
hUi : Ui ∈ (chunk hP G ε ⋯).parts
hVj : Ui ∈ (chunk hP G ε ⋯).parts
i : α
hi : i ∈ Ui
⊢ False

Tactic:
exact hUV.2.2 (P.disjoint.elim_finset hUV.1 hUV.2.1 i (Finpartition.le _ hUi hi) <|
    Finpartition.le _ hVj hi)

Premises used: Finpartition.disjoint, And.right, And.left, Finpartition.le, Set.PairwiseDisjoint.elim_finset
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
simp :
  (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag).Pairwise fun (x y : ↥P.parts.offDiag) ↦
    ∀ ⦃a : Finset α × Finset α⦄,
      a.1 ∈ (chunk hP G ε ⋯).parts ∧ a.2 ∈ (chunk hP G ε ⋯).parts →
        ¬(a.1 ∈ (chunk hP G ε ⋯).parts ∧ a.2 ∈ (chunk hP G ε ⋯).parts)
⊢ (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag).PairwiseDisjoint (distinctPairs hP G ε)

Tactic:
simp +unfoldPartialApp only [distinctPairs, Set.PairwiseDisjoint,
    Function.onFun, Finset.disjoint_left, mem_product]

Premises used: Function.onFun, Set.PairwiseDisjoint, Finset.disjoint_left, _private.0.SzemerediRegularity.distinctPairs, Finset.mem_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs : (s₁, s₂) ∈ P.parts.offDiag
h :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
t₁ t₂ : Finset α
ht : (t₁, t₂) ∈ P.parts.offDiag
h_1 :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
hst :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs ≠
    Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
rw :
  ∀ (hs_1 : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2),
    Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs ∈
        (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag) →
      ∀ (t₁ t₂ : Finset α) (ht : (t₁, t₂) ∈ P.parts.offDiag)
        (ht_1 : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2),
        Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht ∈
            (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag) →
          ∀
            (hst :
              Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs ≠
                Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht)
            (u v : Finset α) (huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts)
            (huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts), False
⊢ False

Tactic:
rw [mem_offDiag] at hs ht

Premises used: Finset.mem_offDiag
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs_1 : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
h :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
t₁ t₂ : Finset α
ht_1 : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
h_1 :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
hst :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ≠
    Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
obtain : ∀ (a : α) (ha : a ∈ (u, v).1), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.1

Premises used: And.left, Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs_1 : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
h :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
t₁ t₂ : Finset α
ht_1 : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
h_1 :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
hst :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ≠
    Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
a : α
ha : a ∈ (u, v).1
obtain : ∀ (b : α) (hb : b ∈ (u, v).2), False
⊢ False

Tactic:
obtain ⟨b, hb⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.2

Premises used: And.right, Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs_1 : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
h :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
t₁ t₂ : Finset α
ht_1 : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
h_1 :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
hst :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ≠
    Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
a : α
ha : a ∈ (u, v).1
b : α
hb : b ∈ (u, v).2
⊢ False

Tactic:
hst <| Subtype.ext <| Prod.ext
    (P.disjoint.elim_finset hs.1 ht.1 a (Finpartition.le _ huv₁.1 ha) <|
      Finpartition.le _ huv₂.1 ha) <|
        P.disjoint.elim_finset hs.2.1 ht.2.1 b (Finpartition.le _ huv₁.2 hb) <|
          Finpartition.le _ huv₂.2 hb

Premises used: Finpartition.disjoint, And.right, And.left, Prod.ext, Finpartition.le, Set.PairwiseDisjoint.elim_finset, Subtype.ext