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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ G.edgeSet
⊢ e ∈ p.edges

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ Nonempty (↑s ≃ ↑t)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set ↑G.deleteUniversalVerts.verts
⊢ Disjoint (Subtype.val '' s) G.universalVerts

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
t : Set V
s : Set ↑G.deleteUniversalVerts.verts
K : G.deleteUniversalVerts.coe.ConnectedComponent
h : t ⊆ G.universalVerts
hrep : ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents
⊢ Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) =
    #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1))

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
hp : p.IsTrail
h : p.edgeSet = G.edgeSet
⊢ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.edgeSet = G.edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ ⋯.edgesFinset = G.edgeFinset

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : s ∩ t = ∅
x✝ : α
⊢ x✝ ∈ X

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : k = 0
⊢ X = univ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
s : Finset V
h : s = {v | Odd (G.degree v)}
⊢ s.card = 0 ∨ s.card = 2

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
E : Type u_3
inst✝ : MetricSpace E
p : V ↪ E
⊢ ∀ {u v : V}, ⊥.Adj u v → dist (p u) (p v) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
E : Type u_3
inst✝¹ : MetricSpace E
inst✝ : Subsingleton V
x : E
u v : V
ha : G.Adj u v
⊢ dist ({ toFun := fun x_1 ↦ x, inj' := ⋯ } u) ({ toFun := fun x_1 ↦ x, inj' := ⋯ } v) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
⊢ w₁ ∈ W

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
⊢ w₂ ∈ W

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
w3 : 3 ≤ #W
⊢ #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w✝⁴ w✝³ w✝² : α
w✝¹ w✝ : Finset α
hw : H.IsFiveWheelLike (r + 1) k w✝⁴ w✝³ w✝² w✝¹ w✝
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hf : G.CliqueFree (r + 1)
hd : (3 * r - 4) * ‖α‖ / (3 * r - 1) < G.minDegree
⊢ G.Colorable r

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover ∅ ↔ G = ⊥

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover Set.univ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
c : Set V
⊢ ⊥.IsVertexCover c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c d : Set V
hcd : c ⊆ d
hc : G.IsVertexCover c
⊢ G.IsVertexCover d

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsVertexCover c → G.IsIndepSet cᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsIndepSet cᶜ ↔ G.IsVertexCover c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsVertexCover cᶜ ↔ G.IsIndepSet c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ≃g H
c : Set W
h : G.IsVertexCover (⇑f ⁻¹' c)
⊢ H.IsVertexCover c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ≃g H
c : Set V
⊢ H.IsVertexCover (⇑f '' c) ↔ G.IsVertexCover c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ∞
⊢ G.vertexCoverNum ≤ n ↔ ∀ (m : ℕ∞), (∀ (s : Set V), G.IsVertexCover s → m ≤ s.encard) → m ≤ n

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∃ s, s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
⊢ s ⊆ Set.univ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
⊢ ∃ s, s.encard = ↑n ∧ G.IsVertexCover s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
⊢ ⊥.IsVertexCover ∅

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.vertexCoverNum = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G = ⊥ → G.vertexCoverNum = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum = 0 ↔ G = ⊥

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
⊢ G.IsVertexCover (Set.univ \ {x})

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ ENat.card V - 1 ≠ ⊤

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ G.vertexCoverNum < ENat.card V

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
v w : V
x✝ : G.Adj v w
⊢ v ∈ (fun x ↦ (Quot.out x).1) '' G.edgeSet ∨ w ∈ (fun x ↦ (Quot.out x).1) '' G.edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
by

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
⊢ ↑n - 1 ≤ ENat.card V

Tactic:
by

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ 1 ≠ ⊤

Tactic:
by

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t ⊆ Set.univ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard ≠ ⊤

Tactic:
by

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ 1 < (Set.univ \ t).encard

Tactic:
by

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this✝ : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
a b : V
left✝¹ : a ∈ Set.univ \ t
left✝ : b ∈ Set.univ \ t
hne : a ≠ b
⊢ (completeGraph V).Adj a b

Tactic:
by

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

Goal state before:
pp: V : Type u_1
⊢ (completeGraph V).vertexCoverNum = ENat.card V - 1

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ¬M.spanningCoe.Adj x a

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝¹ : IsAntichain H.Adj sᶜ
this✝ : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
this : G.IsVertexCover (⇑f ⁻¹' s)
⊢ ∀ ⦃x : V⦄, x ∈ ⇑f ⁻¹' s → { toFun := ⇑f, inj' := hf } x ∈ s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).Adj a c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ∃ G', G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
inst✝ : Finite V
u : Set V
h : G ≤ G'
ht : G'.IsTutteViolator u
⊢ G.IsTutteViolator u

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
⊢ (Subtype.val '' ?m.40).ncard ≤ (universalVerts ?m.39).ncard

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
K : G.deleteUniversalVerts.coe.ConnectedComponent
⊢ ∃ M, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
⊢ M2.IsMatching

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
by

Goal state after: