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

Goal state before:
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
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
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
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
left✝ : ∀ 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
ha : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False

Tactic:
;

Goal state after:
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
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
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
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
left✝ : ∀ 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
ha : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ #P.parts * 4 ^ #P.parts ≤ #P.parts * 16 ^ #P.parts

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ #P.parts * 4 ^ #P.parts ≤ #P.parts * 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hab
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ 4 ≤ 16

Tactic:
;

Goal state after:
case hab
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ 4 ≤ 16
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 α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 1 = 4 / 4

Tactic:
;

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 α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 1 = 4 / 4
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case hbc
α : 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 : ℕ := ⋯
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 4 / ε ^ 5 < ↑⌊4 / ε ^ 5⌋₊ + 1

Tactic:
;

Goal state after:
case hbc
α : 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 : ℕ := ⋯
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 4 / ε ^ 5 < ↑⌊4 / ε ^ 5⌋₊ + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 + ((if G.IsUniform ε (↑x).1 (↑x).2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤
    (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
distinctPairs,

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 + ((if G.IsUniform ε (↑x).1 (↑x).2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case ha
α : 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.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts) ^ 2 ≠ 0

Tactic:
;

Goal state after:
case ha
α : 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.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts) ^ 2 ≠ 0
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.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ i ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε i, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / (4 ^ 2) ^ #P.parts /
      ↑(#P.parts) ^ 2

Tactic:
;

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.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ i ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε i, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / (4 ^ 2) ^ #P.parts /
      ↑(#P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x✝¹ x✝ : V
⊢ (G.deleteEdges G'.edgeSet).Adj x✝¹ x✝ ↔ (G \ G').Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
G G' : SimpleGraph V
x✝¹ x✝ : V
⊢ (G.deleteEdges G'.edgeSet).Adj x✝¹ x✝ ↔ (G \ G').Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
u v : V
⊢ (G.deleteEdges s).Adj u v ↔ G.Adj u v

Tactic:
;

Goal state after:
V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
u v : V
⊢ (G.deleteEdges s).Adj u v ↔ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
s t : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((fromEdgeSet s).deleteEdges t).Adj x✝¹ x✝ ↔ (fromEdgeSet (s \ t)).Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
s t : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((fromEdgeSet s).deleteEdges t).Adj x✝¹ x✝ ↔ (fromEdgeSet (s \ t)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x x✝ : V
⊢ (∃ w, G.Adj x✝ w ∧ x✝ ≠ x ∧ w ≠ x) → x✝ ∈ G.support \ {x}

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
x x✝ : V
⊢ (∃ w, G.Adj x✝ w ∧ x✝ ≠ x ∧ w ≠ x) → x✝ ∈ G.support \ {x}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ y✝ : ↑G'.verts
⊢ s(x✝, y✝) ∈ G'.coe.edgeSet ↔ s(x✝, y✝) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
;

Goal state after:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ y✝ : ↑G'.verts
⊢ s(x✝, y✝) ∈ G'.coe.edgeSet ↔ s(x✝, y✝) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → G.Subgraph
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝

Tactic:
;

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → G.Subgraph
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝
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 γ
g : A.Copy B
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, A.Adj a b → B.Adj (toFun✝ a) (toFun✝ b)
injective'✝ : Injective ⇑{ toFun := toFun✝, map_rel' := map_rel'✝ }
h :
  (fun f ↦ ⇑f.toHom) { toHom := { toFun := toFun✝, map_rel' := map_rel'✝ }, injective' := injective'✝ } =
    (fun f ↦ ⇑f.toHom) g
⊢ { toHom := { toFun := toFun✝, map_rel' := map_rel'✝ }, injective' := injective'✝ } = g

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 γ
g : A.Copy B
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, A.Adj a b → B.Adj (toFun✝ a) (toFun✝ b)
injective'✝ : Injective ⇑{ toFun := toFun✝, map_rel' := map_rel'✝ }
h :
  (fun f ↦ ⇑f.toHom) { toHom := { toFun := toFun✝, map_rel' := map_rel'✝ }, injective' := injective'✝ } =
    (fun f ↦ ⇑f.toHom) g
⊢ { toHom := { toFun := toFun✝, map_rel' := map_rel'✝ }, injective' := injective'✝ } = g
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
x✝ : α
⊢ (g.comp f) x✝ = (⇑g ∘ ⇑f) x✝

Tactic:
;

Goal state after:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
x✝ : α
⊢ (g.comp f) x✝ = (⇑g ∘ ⇑f) x✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a✝ : V
⊢ (ofLE G G ⋯) a✝ = (id G) a✝

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
a✝ : V
⊢ (ofLE G G ⋯) a✝ = (id G) a✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
a✝ : V
⊢ ((ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂)) a✝ = (ofLE G₁ G₃ ⋯) a✝

Tactic:
;

Goal state after:
V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
a✝ : V
⊢ ((ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂)) a✝ = (ofLE G₁ G₃ ⋯) 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
⊢ G.minDegree ≤ H.minDegree

Tactic:
refine H.le_minDegree_of_forall_le_degree _ fun w ↦ ?_

Goal state after:
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
w : W
⊢ G.minDegree ≤ H.degree w
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ ∃ H' _e, H'.IsInduced

Tactic:
refine ⟨f.toCopy.toSubgraph, f.toCopy.isoToSubgraph, ?_⟩

Goal state after:
case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ f.toCopy.toSubgraph.IsInduced
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
⊢ 0 < G.copyCount H ↔ H ⊑ G

Tactic:
simp [copyCount, -nonempty_subtype, isContained_iff_exists_iso_subgraph, card_pos,
    filter_nonempty_iff]

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
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.Regularity.Equitabilise

Goal state before:
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
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
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False

Tactic:
;

Goal state after:
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
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
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False
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: case pos
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h✝ : H = ⊥
⊢ G ≤ G

pp: case neg
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h✝ : ¬H = ⊥
⊢ G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some}) ≤ G

Tactic:
;

Goal state after:
case pos
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h✝ : H = ⊥
⊢ G ≤ G

case neg
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h✝ : ¬H = ⊥
⊢ 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.Subgraph

Goal state before:
pp: case intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝ : Finite V
val✝ : Fintype V
⊢ Finite G.Subgraph

Tactic:
;

Goal state after:
case intro
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝ : Finite V
val✝ : Fintype V
⊢ Finite G.Subgraph
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ (G.replaceVertex s s).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ (G.replaceVertex s s).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ { Adj := fun v w ↦ if v = s then if w = s then False else G.Adj s w else if w = s then G.Adj v s else G.Adj v w,
          symm := ⋯, loopless := ⋯ }.Adj
      x✝¹ x✝ ↔
    G.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ { Adj := fun v w ↦ if v = s then if w = s then False else G.Adj s w else if w = s then G.Adj v s else G.Adj v w,
          symm := ⋯, loopless := ⋯ }.Adj
      x✝¹ x✝ ↔
    G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
⊢ (if x✝ = t then if y✝ = t then False else G.Adj s y✝ else if y✝ = t then G.Adj x✝ s else G.Adj x✝ y✝) ↔
    G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
⊢ (if x✝ = t then if y✝ = t then False else G.Adj s y✝ else if y✝ = t then G.Adj x✝ s else G.Adj x✝ y✝) ↔
    G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s