awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 ε
⊢ stepBound #P.parts ≤ Fintype.card α
have grw : #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts
Tactic: grw [← hPα, stepBound]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 ε
⊢ #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts
have bc : LE.le (α := ℕ) 4 16
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (hypothesis)
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 ε
⊢ #(increment hP G ε).parts = stepBound #P.parts
have hPα' : stepBound #P.parts ≤ Fintype.card α
Tactic: have hPα' : stepBound #P.parts ≤ card α := by grw [← hPα, stepBound]; gcongr; simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (hypothesis)
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 α
⊢ #(increment hP G ε).parts = stepBound #P.parts
have hPpos : 0 < stepBound #P.parts
Tactic: have hPpos : 0 < stepBound #P.parts := stepBound_pos (nonempty_of_not_uniform hPG).card_pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ #(increment hP G ε).parts = stepBound #P.parts
have rw : ∑ A ∈ P.parts.attach, #(chunk hP G ε sorry).parts = stepBound #P.parts
Tactic: rw [increment, card_bind]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ ∑ A ∈ P.parts.attach, #(chunk hP G ε ⋯).parts = stepBound #P.parts
have simp_rw : HAdd.hAdd (α := ℕ)
    (∑ x :
      ↥({x ∈ P.parts.attach | #(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
      #(parts
          (equitabilise (P :=
            atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) sorry)))
    (∑ x :
      ↥({x ∈ P.parts.attach | ¬#(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
      #(parts
          (equitabilise (P :=
            atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) sorry))) =
  stepBound #P.parts
Tactic: simp_rw [chunk, apply_dite Finpartition.parts, apply_dite card, sum_dite]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ HAdd.hAdd (α := ℕ)
      (∑ x :
        ↥({x ∈ P.parts.attach | #(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)))
      (∑ x :
        ↥({x ∈ P.parts.attach | ¬#(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯))) =
    stepBound #P.parts
have rw : #({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 [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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)}) *
        (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
⊢ HAdd.hAdd (α := ℕ)
      (∑ x :
        ↥({x ∈ P.parts.attach | #(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)))
      (∑ x :
        ↥({x ∈ P.parts.attach | ¬#(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯))) =
    stepBound #P.parts
have rw₁ : ∀
  (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 α))) sorry)) =
      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: rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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)}) *
        (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
rw₁ :
  ∀
    (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)
⊢ HAdd.hAdd (α := ℕ)
      (∑ x :
        ↥({x ∈ P.parts.attach | #(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)))
      (∑ x :
        ↥({x ∈ P.parts.attach | ¬#(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯))) =
    stepBound #P.parts
have rw₂ : ℕ
Tactic: rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 ∈ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 ∈ 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
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 ∈ 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
have e_a : #P.parts.attach = #P.parts
Tactic: rw [card_filter_add_card_filter_not, card_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ #({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
have e_a₁ : #P.parts = #P.parts
Tactic: rw [card_filter_add_card_filter_not, card_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
⊢ (increment hP G ε).IsEquipartition
have simp_rw : ∃ (b : ℕ), ∀ a ∈ (↑(increment hP G ε).parts : Set (Finset α)), #a = b ∨ #a = b + 1
Tactic: simp_rw [IsEquipartition, Set.equitableOn_iff_exists_eq_eq_add_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
have refine : ∀ (A : Finset α) (hA : A ∈ (↑(increment hP G ε).parts : Set (Finset α))), #A = m ∨ #A = m + 1
Tactic: refine ⟨m, fun A hA => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (hypothesis)
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 = m ∨ #A = m + 1
have hA₁ : ∃ (A_1 : Finset α) (hA : A_1 ∈ P.parts), A ∈ (chunk hP G ε hA).parts
Tactic: rw [mem_coe, increment, mem_bind] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ #A = m ∨ #A = m + 1
have obtain : ∀ (U : Finset α) (hU : U ∈ P.parts) (hA : A ∈ (chunk hP G ε hU).parts), #A = m ∨ #A = m + 1
Tactic: obtain ⟨U, hU, hA⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 α
⊢ (Ui, Vj) ∈ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) → (Ui, Vj) ∈ (increment hP G ε).parts.offDiag
have simp : ∀ (x x_1 : Finset α) (x_2 : x ∈ P.parts ∧ x_1 ∈ P.parts ∧ ¬x = x_1),
  Ui ∈ (chunk hP G ε sorry).parts →
    Vj ∈ (chunk hP G ε sorry).parts →
      (∃ (a : Finset α) (h : a ∈ P.parts), Ui ∈ parts (a := a) (chunk hP G ε sorry : Finpartition a)) ∧
        (∃ (a : Finset α) (h : a ∈ P.parts), Vj ∈ parts (a := a) (chunk hP G ε sorry : Finpartition a)) ∧ ¬Ui = Vj
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
have refine : ∀ (U V : Finset α) (hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V) (hUi : Ui ∈ (chunk hP G ε sorry).parts)
  (hVj : Vj ∈ (chunk hP G ε sorry).parts), ¬Ui = Vj
Tactic: refine fun U V hUV hUi hVj => ⟨⟨_, hUV.1, hUi⟩, ⟨_, hUV.2.1, hVj⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ False
have obtain : ∀ (i : α) (hi : i ∈ Ui), False
Tactic: obtain ⟨i, hi⟩ := nonempty_of_mem_parts _ hUi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
⊢ (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag).PairwiseDisjoint (distinctPairs hP G ε)
have simp : (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag).Pairwise fun (x y : ↥P.parts.offDiag) ↦
  ∀ ⦃a : Finset α × Finset α⦄,
    a.1 ∈ (chunk hP G ε sorry).parts ∧ a.2 ∈ (chunk hP G ε sorry).parts →
      ¬(a.1 ∈ (chunk hP G ε sorry).parts ∧ a.2 ∈ (chunk hP G ε sorry).parts)
Tactic: simp +unfoldPartialApp only [distinctPairs, Set.PairwiseDisjoint,
    Function.onFun, Finset.disjoint_left, mem_product]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ False
have 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 ε sorry).parts ∧ (u, v).2 ∈ (chunk hP G ε sorry).parts)
          (huv₂ : (u, v).1 ∈ (chunk hP G ε sorry).parts ∧ (u, v).2 ∈ (chunk hP G ε sorry).parts), False
Tactic: rw [mem_offDiag] at hs ht
Cleared hypotheses: h, t₁, t₂, ht, h_1, hst, u, v, huv₁, huv₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ False
have obtain : ∀ (a : α) (ha : a ∈ (u, v).1), False
Tactic: obtain ⟨a, ha⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.1