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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ ∃ x, True

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ ∃ x, True
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ ¬z = v

Tactic:
]

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ ¬z = v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
K : Type u_3
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : Fintype K
⊢ Fintype.card K ^ (Fintype.card V).choose 2 = Fintype.card K ^ (Fintype.card V).choose 2

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), C ⟨e, h⟩ = k}).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), C ⟨e, h⟩ = k}).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i✝ j✝ : K
h : i✝ ≠ j✝
⊢ ∀ (x y : V), (C.labelGraph i✝).Adj x y → ¬(C.labelGraph j✝).Adj x y

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i✝ j✝ : K
h : i✝ ≠ j✝
⊢ ∀ (x y : V), (C.labelGraph i✝).Adj x y → ¬(C.labelGraph j✝).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail

Tactic:
]

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ ∃ w, G.Adj u w

Tactic:
]

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ ∃ w, G.Adj u w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ fp.part s = fp.part t ↔ fp.part s = fp.part t

Tactic:
]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
x✝ y✝ : α
h' : ¬G.Adj y✝ x✝
⊢ ¬G.Adj y✝ x✝

Tactic:
]

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
x✝ y✝ : α
h' : ¬G.Adj y✝ x✝
⊢ ¬G.Adj y✝ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ a✝ ∈ h.finpartition.part s

Tactic:
]

Goal state after:
case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ a✝ ∈ h.finpartition.part s
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this✝ : 1 ≤ List.count u pwz.support
this : 1 ≤ List.count u pzx.support.tail
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail

Tactic:
]

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this✝ : 1 ≤ List.count u pwz.support
this : 1 ≤ List.count u pzx.support.tail
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
hn : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
hn : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
a✝ b✝ : α
⊢ G.Adj a✝ b✝ ↔ G.Adj a✝ b✝

Tactic:
]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case mpr
α : Type u
G : SimpleGraph α
w✝² : Type u
w✝¹ : w✝² → Type u
w✝ : ∀ (i : w✝²), Nonempty (w✝¹ i)
e : G ≃g completeMultipartiteGraph w✝¹
x✝² x✝¹ x✝ : α
h1 : ¬(completeMultipartiteGraph w✝¹).Adj (e x✝²) (e x✝¹)
h2 : ¬(completeMultipartiteGraph w✝¹).Adj (e x✝¹) (e x✝)
⊢ ¬(completeMultipartiteGraph w✝¹).Adj (e x✝²) (e x✝)

Tactic:
]

Goal state after:
case mpr
α : Type u
G : SimpleGraph α
w✝² : Type u
w✝¹ : w✝² → Type u
w✝ : ∀ (i : w✝²), Nonempty (w✝¹ i)
e : G ≃g completeMultipartiteGraph w✝¹
x✝² x✝¹ x✝ : α
h1 : ¬(completeMultipartiteGraph w✝¹).Adj (e x✝²) (e x✝¹)
h2 : ¬(completeMultipartiteGraph w✝¹).Adj (e x✝¹) (e x✝)
⊢ ¬(completeMultipartiteGraph w✝¹).Adj (e x✝²) (e x✝)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #large + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #large + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
hn : small = large
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
⊢ p.length ≠ q.length

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
⊢ p.length ≠ q.length
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
w✝² w✝¹ w✝ : α
h1 : ¬G.Adj w✝¹ w✝²
h2 : ¬G.Adj w✝¹ w✝
h3 : G.Adj w✝² w✝
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂

Tactic:
]

Goal state after:
α : Type u
G : SimpleGraph α
w✝² w✝¹ w✝ : α
h1 : ¬G.Adj w✝¹ w✝²
h2 : ¬G.Adj w✝¹ w✝
h3 : G.Adj w✝² w✝
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∈ p.support
⊢ q.length + 1 ≠ q.length

Tactic:
]

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∈ p.support
⊢ q.length + 1 ≠ q.length
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
x✝ : ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
w✝² w✝¹ w✝ : α
h1 : G.Adj w✝¹ w✝
h2 : ¬G.Adj w✝¹ w✝²
h3 : ¬G.Adj w✝² w✝
h : G.IsCompleteMultipartite
⊢ ¬G.Adj w✝¹ w✝²

Tactic:
]

Goal state after:
α : Type u
G : SimpleGraph α
x✝ : ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
w✝² w✝¹ w✝ : α
h1 : G.Adj w✝¹ w✝
h2 : ¬G.Adj w✝¹ w✝²
h3 : ¬G.Adj w✝² w✝
h : G.IsCompleteMultipartite
⊢ ¬G.Adj w✝¹ w✝²
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1

Tactic:
]

Goal state after:
case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
this✝ : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj w₁ v
h2 : ¬G.Adj w₂ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v

Tactic:
]

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
this✝ : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj w₁ v
h2 : ¬G.Adj w₂ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ ∀ {a b : Fin 3},
    G.Adj
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          b) ↔
      (pathGraph 3)ᶜ.Adj a b

Tactic:
by
    intro _ _
    simp_rw [Embedding.coeFn_mk, compl_adj, ne_eq, pathGraph_adj, not_or]
    have := h.adj
    have := h.adj.symm
    have h1 := h.not_adj_fst
    have h2 := h.not_adj_snd
    have ⟨_, _⟩ : ¬ G.Adj w₁ v ∧ ¬ G.Adj w₂ v := by rw [adj_comm] at h1 h2; exact ⟨h1, h2⟩
    aesop

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ ¬G.Adj v w

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ ¬G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #h.finpartition.parts
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #h.finpartition.parts
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ p.length + 1

Tactic:
]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ p.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
⊢ False

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Preconnected ∧ univ.Nonempty

Tactic:
]

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

Goal state before:
pp: case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩ ≤ ↑v.2 * r + (r - 1)

Tactic:
]

Goal state after:
case refine_2.a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩ ≤ ↑v.2 * r + (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 * r ≤ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩

Tactic:
]

Goal state after:
case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 * r ≤ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).Adj v w ↔ (completeEquipartiteGraph r t).Adj v w

Tactic:
]

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

Tactic:
]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
h : Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔
    Odd #({c | c.supp ⊆ c'.supp}.disjiUnion (fun c ↦ c.supp.toFinset) ⋯)

Tactic:
]

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔
    Odd #({c | c.supp ⊆ c'.supp}.disjiUnion (fun c ↦ c.supp.toFinset) ⋯)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔ Odd (Nat.card ↑c'.supp)

Tactic:
rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔
    Odd #({c | c.supp ⊆ c'.supp}.disjiUnion (fun c ↦ c.supp.toFinset) ⋯)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
]

Goal state after:
r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : v₁.1 ≠ v₂.1
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
]

Goal state after:
case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : v₁.1 ≠ v₂.1
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)