mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ (a - 1) * m + b * (m + 1) = a * m + b * (m + 1) - m

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧ m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b - 1) * (m + 1) = a * m + b * (m + 1) - (m + 1)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : 0 < a
⊢ 0 < m ∧ m ≤ m + 1 ∧ m ≤ a * m + b * (m + 1) ∧ (a - 1) * m + b * (m + 1) = a * m + b * (m + 1) - m

case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧ m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b - 1) * (m + 1) = a * m + b * (m + 1) - (m + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case refine_2.refine_2.ha
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₂)

pp: case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₁)

Tactic:
<;>

Goal state after:
case refine_2.refine_2.ha
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₂)

case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₁)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X) ≫ (t.eTruncGE.map (φ.app 0)).app X) ≫
        (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)

Tactic:
NatTrans.naturality,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map
          ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
            (t.eTruncGE.obj a').map ((t.eTruncLTι b).app X)) ≫
        (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
rw [nonuniformWitnesses, dif_pos h]
  exact (not_isUniform_iff.1 h).choose_spec.1

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case inr.refine_1
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : 1 ≤ δ
⊢ |↑(edgeDensity r s₂ t₂)| ≤ 1

pp: case inr.refine_2
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : 1 ≤ δ
⊢ |↑(edgeDensity r s₁ t₁)| ≤ 1

Tactic:
<;>

Goal state after:
case inr.refine_1
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : 1 ≤ δ
⊢ |↑(edgeDensity r s₂ t₂)| ≤ 1

case inr.refine_2
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ : 0 ≤ δ
hscard : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
htcard : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
h : 1 ≤ δ
⊢ |↑(edgeDensity r s₁ t₁)| ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case e'_3
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 = 2 * ↑(#A) ^ 2 * 1

pp: case e'_4
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts) = 2 * ↑(#A) ^ 2 * (ε / 4 * ↑(#P.parts))

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 = 2 * ↑(#A) ^ 2 * 1

case e'_4
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts) = 2 * ↑(#A) ^ 2 * (ε / 4 * ↑(#P.parts))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
⊢ bound ε l ≤ #univ

Tactic:
rwa [Finset.card_univ]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ε ^ 5 / 4 * ↑i ≤ 1
⊢ ↑i ≤ 4 / ε ^ 5

Tactic:
rw [div_mul_eq_mul_div, div_le_iff₀ (show (0 : ℝ) < 4 by simp)] at hi

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 1 * 4
⊢ ↑i ≤ 4 / ε ^ 5
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#({x ∈ P.parts.offDiag | ¬G.IsUniform ε x.1 x.2})) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25))

Tactic:
← Finpartition.nonUniforms,

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25))
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
⊢ #(G.deleteIncidenceSet x).edgeFinset = #(G.edgeFinset \ G.incidenceFinset x)

Tactic:
edgeFinset_deleteIncidenceSet_eq_sdiff

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a b : V
h : s(v, w) = s(a, b)
⊢ a ∈ {v, w}

Tactic:
apply_fun fun e ↦ a ∈ e at h
    simp only [Sym2.mem_iff, true_or, eq_iff_iff, iff_true] at h
    exact h

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  x ∈ {u ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}.biUnion id ∧
    x ∉ {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id

Tactic:
mem_biUnion

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  (∃ a ∈ {u ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}, x ∈ id a) ∧
    x ∉ {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ M'.verts ⊆ M.verts

pp: case right
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w

Tactic:
<;>

Goal state after:
case left
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ M'.verts ⊆ M.verts

case right
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ 2 ^ (#P.parts - 1) * m

Tactic:
apply (card_le_card q).trans (card_biUnion_le.trans _)

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ ∑ a ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id) ≤
    2 ^ (#P.parts - 1) * m
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.map Hom.id H).verts ↔ x✝ ∈ H.verts

pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.map Hom.id H).Adj x✝¹ x✝ ↔ H.Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.map Hom.id H).verts ↔ x✝ ∈ H.verts

case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.map Hom.id H).Adj x✝¹ x✝ ↔ H.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x✝ : U
⊢ x✝ ∈ (Subgraph.map (g.comp f) H).verts ↔ x✝ ∈ (Subgraph.map g (Subgraph.map f H)).verts

pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x✝¹ x✝ : U
⊢ (Subgraph.map (g.comp f) H).Adj x✝¹ x✝ ↔ (Subgraph.map g (Subgraph.map f H)).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x✝ : U
⊢ x✝ ∈ (Subgraph.map (g.comp f) H).verts ↔ x✝ ∈ (Subgraph.map g (Subgraph.map f H)).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x✝¹ x✝ : U
⊢ (Subgraph.map (g.comp f) H).Adj x✝¹ x✝ ↔ (Subgraph.map g (Subgraph.map f H)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x✝ ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts

pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝¹ x✝ : W
⊢ (Subgraph.map f (H₁ ⊔ H₂)).Adj x✝¹ x✝ ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x✝ ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝¹ x✝ : W
⊢ (Subgraph.map f (H₁ ⊔ H₂)).Adj x✝¹ x✝ ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x✝ : W
⊢ x✝ ∈ (Subgraph.map e.toHom ⊤).verts ↔ x✝ ∈ ⊤.verts

pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x✝¹ x✝ : W
⊢ (Subgraph.map e.toHom ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x✝ : W
⊢ x✝ ∈ (Subgraph.map e.toHom ⊤).verts ↔ x✝ ∈ ⊤.verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x✝¹ x✝ : W
⊢ (Subgraph.map e.toHom ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝ : V
⊢ x✝ ∈ (Subgraph.comap f ⊤).verts ↔ x✝ ∈ ⊤.verts

pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝¹ x✝ : V
⊢ (Subgraph.comap f ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝ : V
⊢ x✝ ∈ (Subgraph.comap f ⊤).verts ↔ x✝ ∈ ⊤.verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝¹ x✝ : V
⊢ (Subgraph.comap f ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case ha
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 1 ≤ 2

pp: case ha
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 1 ≤ 2

Tactic:
<;>

Goal state after:
case ha
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 1 ≤ 2

case ha
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ 1 ≤ 2
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : v = t
h✝ : w = t
⊢ False → False

pp: case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : v = t
h✝ : ¬w = t
⊢ G.Adj s w → G.Adj w s

pp: case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : ¬v = t
h✝ : w = t
⊢ G.Adj v s → G.Adj s v

pp: case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : ¬v = t
h✝ : ¬w = t
⊢ G.Adj v w → G.Adj w v

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : v = t
h✝ : w = t
⊢ False → False

case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : v = t
h✝ : ¬w = t
⊢ G.Adj s w → G.Adj w s

case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : ¬v = t
h✝ : w = t
⊢ G.Adj v s → G.Adj s v

case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
h✝¹ : ¬v = t
h✝ : ¬w = t
⊢ G.Adj v w → G.Adj w v