-- Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean
theorem distinctPairs_increment :
    P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) ⊆ (increment hP G ε).parts.offDiag

Proof state:
case mk.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : 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)

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : 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, ∃ (h : a ∈ P.parts), Ui ∈ (chunk hP G ε ⋯).parts) ∧
          (∃ a, ∃ (h : a ∈ P.parts), Vj ∈ (chunk hP G ε ⋯).parts) ∧ ¬Ui = Vj

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

Result:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
Ui Vj 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

Proof state:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
⊢ (Ui, Vj) ∈ P.parts.offDiag.attach.biUnion (SzemerediRegularity.distinctPairs hP G ε) →
    (Ui, Vj) ∈ (increment hP G ε).parts.offDiag

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

Result:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : 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, ∃ (h : a ∈ P.parts), Ui ∈ (chunk hP G ε ⋯).parts) ∧
          (∃ a, ∃ (h : a ∈ P.parts), Vj ∈ (chunk hP G ε ⋯).parts) ∧ ¬Ui = Vj

Proof state:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : 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
⊢ False

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

Result:
case mk.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : 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

Proof state:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
Ui Vj 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

Tactic:
rintro rfl

Result:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : 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
⊢ False

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ P.parts.offDiag.attach.biUnion (SzemerediRegularity.distinctPairs hP G ε) ⊆ (increment hP G ε).parts.offDiag

Tactic:
rintro ⟨Ui, Vj⟩

Result:
case mk
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
⊢ (Ui, Vj) ∈ P.parts.offDiag.attach.biUnion (SzemerediRegularity.distinctPairs hP G ε) →
    (Ui, Vj) ∈ (increment hP G ε).parts.offDiag