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

Goal state before:
pp: case neg.refine_3
α : 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 : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑i + ε ^ 5 / 4 ≤ ↑(P.energy G) + ε ^ 5 / 4

Tactic:
]

Goal state after:
case neg.refine_3
α : 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 : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑i + ε ^ 5 / 4 ≤ ↑(P.energy G) + ε ^ 5 / 4
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G ≤ fromEdgeSet s ⊔ G' ↔ G ≤ fromEdgeSet s ⊔ G'

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet s ↔ Disjoint G.edgeSet s

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
h : H ≤ G
⊢ H = H

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x : V
⊢ G.incidenceSet x ⊆ Sym2.diagSetᶜ

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
x : V
⊢ G.incidenceSet x ⊆ Sym2.diagSetᶜ
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
h_notMem : x ∉ {x}ᶜ
⊢ G.support \ {x} ⊆ Set.univ \ {x}

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ G.support \ {x} ⊆ Set.univ \ {x}
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.parts.offDiag) * (ε ^ 5 / 25) +
      ↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) =
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 - ↑(#P.parts.offDiag) * (ε ^ 5 / 25) +
      ↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3)

Tactic:
]

Goal state after:
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
⊢ {x_1 ∈ G.edgeFinset | x_1 ∉ G.incidenceFinset x} = {x_1 ∈ G.edgeFinset | x ∉ x_1}

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
⊢ {x_1 ∈ G.edgeFinset | x_1 ∉ G.incidenceFinset x} = {x_1 ∈ G.edgeFinset | x ∉ x_1}
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
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∈ G.edgeSet ∨ x ∉ x✝

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∈ G.edgeSet ∨ x ∉ x✝
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
x✝ : Sym2 V
h : x✝ ∈ G.edgeSet
⊢ x✝ ∈ G.edgeSet

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeSet
⊢ x✝ ∈ G.edgeSet
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
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1
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
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ (G.deleteIncidenceSet x).support ⊆ G.support \ {x}

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
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
⊢ ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) = 6 / 7 * ↑(#P.parts) ^ 2 * ε ^ 5 * (7 / 24)

Tactic:
by ring

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
v✝ w✝ : V
h : s(v, w) = s(v✝, w✝)
⊢ s(v, w) ∈ G.edgeSet

Tactic:
]

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
v✝ w✝ : V
h : s(v, w) = s(v✝, w✝)
⊢ s(v, w) ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj w x ↔ H.Adj w x

Tactic:
]

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj w x ↔ H.Adj w x

Tactic:
]

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

Goal state before:
pp: case hbc
α : 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
⊢ 6 * ↑(#P.parts) ^ 2 ≤ ↑(#P.parts * #P.parts - #P.parts) * 7

Tactic:
]

Goal state after:
case hbc
α : 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
⊢ 6 * ↑(#P.parts) ^ 2 ≤ ↑(#P.parts * #P.parts - #P.parts) * 7
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)

Tactic:
]

Goal state after:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hbc
α : 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
⊢ 6 * #P.parts ^ 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7

Tactic:
]

Goal state after:
case hbc
α : 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
⊢ 6 * #P.parts ^ 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7
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
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
h : 0 < a
⊢ b = b

Tactic:
]

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

Goal state before:
pp: ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (∀ G' ∈ Set.range fun i ↦ f i, G'.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
]

Goal state after:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (∀ G' ∈ Set.range fun i ↦ f i, G'.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₁).1 = ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
    ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₁).2 = ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₁).1 = ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
    ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₁).2 = ((fun G' ↦ (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂
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 :
  (∃ 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

Tactic:
]

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.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
⊢ ↑(#P.parts.offDiag) * ε ^ 5 * (22 / 75) = ↑(#P.parts.offDiag) * ε * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)

Tactic:
by ring

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' = ⊥

Tactic:
]

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
a : α
x✝¹ x✝ : ↑(A.neighborSet a)
h : f ↑x✝¹ = f ↑x✝
⊢ ↑x✝¹ = ↑x✝

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
a : α
x✝¹ x✝ : ↑(A.neighborSet a)
h : f ↑x✝¹ = f ↑x✝
⊢ ↑x✝¹ = ↑x✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective (⇑g.toHom ∘ ⇑f.toHom)

Tactic:
]

Goal state after:
case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective (⇑g.toHom ∘ ⇑f.toHom)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

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

Tactic:
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]

Goal state after:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a✝ : W
⊢ ∀ x ∈ H₁.verts, f x = a✝ → ∃ x ∈ H₂.verts, f x = a✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
hf : Surjective ⇑f
h✝ : Nonempty W
v : V
⊢ G.minDegree ≤ G.minDegree

Tactic:
]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
hv : ¬G.IsIsolated v
⊢ G.degree v ≤ G.degree ↑⟨v, ⋯⟩

Tactic:
]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
⊢ A.Free ⊥

Tactic:
]

Goal state after:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
⊢ A.Free ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : A →g ⊥
hf : Injective ⇑f
⊢ Sym2.map (⇑f) (Exists.choose h) ∉ ∅

Tactic:
]

Goal state after:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A.edgeSet.Nonempty
f : A →g ⊥
hf : Injective ⇑f
⊢ Sym2.map (⇑f) (Exists.choose h) ∉ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case refine_3
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts

Tactic:
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]

Goal state after:
case refine_3
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ ∀ x ∈ H.verts, f x = v → v ∈ H'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ #{G' | Nonempty (H ≃g G'.coe)} = #(image Copy.toSubgraph univ)

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ #{G' | Nonempty (H ≃g G'.coe)} = #(image Copy.toSubgraph univ)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ #(image Copy.toSubgraph univ) ≤ G.labelledCopyCount H

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ #(image Copy.toSubgraph univ) ≤ G.labelledCopyCount H
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ #{G' | Nonempty (⊥ ≃g G'.coe)} = 1

Tactic:
]

Goal state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ #{G' | Nonempty (⊥ ≃g G'.coe)} = 1
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
⊢ Nonempty (H ≃g G'.coe) → (Sym2.map Subtype.val '' G'.coe.edgeSet).Nonempty

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
⊢ Nonempty (H ≃g G'.coe) → (Sym2.map Subtype.val '' G'.coe.edgeSet).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ (if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) ≤ G

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ (if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) ≤ G
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
⊢ (if hH : ⊥ = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (⊥ ≃g G'.coe)), {⋯.some})) = G

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
⊢ (if hH : ⊥ = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (⊥ ≃g G'.coe)), {⋯.some})) = G
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
H : SimpleGraph W
hH : H ≠ ⊥
G : SimpleGraph V
⊢ (if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) =
    G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
H : SimpleGraph W
hH : H ≠ ⊥
G : SimpleGraph V
⊢ (if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) =
    G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
H : SimpleGraph W
hH : H ≠ ⊥
G : SimpleGraph V
⊢ G.killCopies H = G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})

Tactic:
rw [killCopies]; exact dif_neg hH

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ ¬∃ B', Nonempty (H ≃g B'.coe)

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ ¬∃ B', Nonempty (H ≃g B'.coe)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' G'.edgeSet).Nonempty

Tactic:
]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' G'.edgeSet).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i