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

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).neighborSet v = {v.1}ᶜ ×ˢ Set.univ

Tactic:
by

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
⊢ #h.finpartition.parts = min (Fintype.card V) r

Tactic:
by

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

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).neighborFinset v = {v.1}ᶜ ×ˢ univ

Tactic:
by

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

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd {c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
by

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

Goal state before:
pp: r t : ℕ
⊢ #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * t ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
⊢ {c' | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
c : Fin n
⊢ Nonempty (↑(C.colorClass c) ↪ Fin t)

Tactic:
by

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
⊢ ↑v₁ ∈ C.colorClass c₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard

Tactic:
by

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⟨↑v₁, ⋯⟩
⊢ (F c₁) v₁ = (F c₂) v₁'

Tactic:
by

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
⊢ ↑v₁ = ↑v₂

Tactic:
by

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
⊢ G ⊑ completeEquipartiteGraph n t

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
hr : r = 0
⊢ #∅ = r ∨ t = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
ht : t = 0
⊢ #∅ = r ∨ t = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
⊢ ∀ {p : Finset V}, p ∈ ∅ → #p = t

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
⊢ (↑∅).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ K.verts = K.parts.biUnion id

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.verts = r * t

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ IsEmpty (Fin r × Fin t)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
⊢ Set.MapsTo G.connectedComponentMk (Quot.out '' C) C

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ Nonempty (Fin r ↪ ↥K.parts)

Tactic:
by

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
⊢ Nonempty (G ≃g turanGraph (Fintype.card V) r)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
⊢ Set.InjOn G.connectedComponentMk (Quot.out '' C)

Tactic:
by

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
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
⊢ G.IsTuranMaximal r

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x✝¹ : G.ConnectedComponent
x✝ : x✝¹ ∈ C
⊢ x✝¹ ∈ G.connectedComponentMk '' Quot.out '' C

Tactic:
by

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
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ G.IsExtremal ⊤.Free ↔ G.IsTuranMaximal (Fintype.card α - 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsExtremal ⊤.Free

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
⊢ Nonempty (Fin t ↪ ↥↑p)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃! x, x ∈ s ∩ c.supp

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ extremalNumber n ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ x, s ∩ c.supp = {x}

Tactic:
by

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
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ ⊤.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) ⊤ ↔
    Nonempty (G ≃g turanGraph (Fintype.card V) (Fintype.card α - 1))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ Disjoint s c.supp

Tactic:
by

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

Goal state before:
pp: n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (s ∩ c.supp).ncard = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ (c.supp \ s).ncard = c.supp.ncard

Tactic:
by

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

Goal state before:
pp: n r c : ℕ
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : Even K.supp.ncard
⊢ ?m.31 ∉ G.oddComponents

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
this : K.supp.ncard ≠ 0
⊢ 1 ≤ K.supp.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
⊢ Even (K.supp \ s).ncard

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
⊢ Fin r × Fin t ↪ V

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
u : α
⊢ G.eccent u = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ G.eccent u = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
⊢ G.eccent u ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u = 0 ↔ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ 0 < G.eccent u ↔ Nontrivial α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ⊤.eccent u = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : t = 0
⊢ ∀ {p : Finset V}, p ∈ ∅ → #p = t

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : t = 0
⊢ (↑∅).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G = ⊤ ↔ ∀ (u : α), G.eccent u = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⨆ p, G.edist p.1 p.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ u v, b < G.edist u v

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.ediam ≠ 0
⊢ Nontrivial α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
⊢ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.Connected
⊢ G.ediam = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
⊢ G.ediam = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.ediam = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist v u + G.edist u w = G.edist u v + G.edist u w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.ediam ≤ 2 * G.eccent u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.diam = (⨆ p, G.edist p.1 p.2).toNat

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ Nontrivial α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
⊢ G.diam = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
⊢ G.diam = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
this : NeZero t
⊢ ∃ j, f (i₁, j) = f (i₂, 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.diam = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.diam = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.diam = 1 ↔ G = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.diam = 0 ↔ G.ediam = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Finite α
inst✝ : Nontrivial α
⊢ G.Connected ↔ G.diam ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
⊢ ∃ u v, G.edist u v = G.radius

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
⊢ G.radius = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
⊢ G.radius ≠ ⊤ ↔ G.Connected

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.radius ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α

Tactic:
by

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

Goal state before:
pp: n r : ℕ
⊢ #(turanGraph (n + r) r).edgeFinset = #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.ediam = ⊤ ↔ G.radius = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam ≤ 2 * G.radius

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.radius = G.ediam ↔ ∃ e, ∀ (u : α), G.eccent u = e

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.radius = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.center = Set.univ ↔ G.radius = G.ediam

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ G.center = Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.center = Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ ⊤.center = Set.univ

Tactic:
by

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

Goal state before:
pp: n✝ r : ℕ
hr : r > 0
n : ℕ
⊢ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property✝ : s ∈ G.end
val✝ : Fintype V
v : V
h : v ∈ ↑(s (Opposite.op Finset.univ))
⊢ v ∈ ↑(Opposite.unop (Opposite.op Finset.univ))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝ : Finite V
⊢ ∀ (a : ↑G.end), False

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (↑e K)).Infinite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝² : G.LocallyFinite
inst✝¹ : Fact G.Preconnected
inst✝ : Infinite V
⊢ G.end.Nonempty

Tactic:
by

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

Goal state before:
pp: n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
⊢ n = n' + r

Tactic:
by

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
r' : ℕ
⊢ IsEmpty (Fin r' × Fin t)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
by

Goal state after: