mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ ¬{a} ⊆ v
hsv : s ∩ v = {a}
⊢ False

Tactic:
← hsv

Goal state after:
case refine_3.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ ¬s ∩ v ⊆ v
hsv : s ∩ v = {a}
⊢ False
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r₁ r₂ : Setoid α
h : r₁.classes = r₂.classes
a b : α
⊢ r₁ a b ↔ r₂ a b

Tactic:
by simp only [rel_iff_exists_classes, h]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)

Tactic:
← Iso.reachable_iff,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ Reachable ?m.15 (?m.16 (φ.symm v)) (?m.16 u) ↔ G'.Reachable v (φ u)

V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ Type ?u.26

V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ SimpleGraph ?m.13

V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G ≃g ?m.15
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case succ
n n✝ : ℕ
ih : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))}, Set.Sized r ↑𝒜 → #𝒞 ≤ #𝒜 → IsInitSeg 𝒞 r → #(∂^[n✝] 𝒞) ≤ #(∂^[n✝] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[n✝ + 1] 𝒞) ≤ #(∂^[n✝ + 1] 𝒜)

Tactic:
| succ _ ih =>

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

Tactic:
ext v

Goal state after:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp ↔ v ∈ c'.supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
w : V
⊢ supp (Quot.mk ⊤.Reachable w) = Set.univ

Tactic:
ext v

Goal state after:
V : Type u
w v : V
⊢ v ∈ supp (Quot.mk ⊤.Reachable w) ↔ v ∈ Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring α
⊢ (G.recolorOfEmbedding f.symm.toEmbedding) ((G.recolorOfEmbedding f.toEmbedding) C) = C

Tactic:
ext v

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring α
v : V
⊢ ((G.recolorOfEmbedding f.symm.toEmbedding) ((G.recolorOfEmbedding f.toEmbedding) C)) v = C v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
⊢ (G.recolorOfEmbedding f.toEmbedding) ((G.recolorOfEmbedding f.symm.toEmbedding) C) = C

Tactic:
ext v

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
v : V
⊢ ((G.recolorOfEmbedding f.toEmbedding) ((G.recolorOfEmbedding f.symm.toEmbedding) C)) v = C v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
deleteEdges,

Goal state after:
case inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ (G \ fromEdgeSet {s(x, y)}).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ G.neighborSet w = {v | v ∈ s ∧ G.Adj v w}

Tactic:
ext v

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ v ∈ G.neighborSet w ↔ v ∈ {v | v ∈ s ∧ G.Adj v w}
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.neighborFinset w = {v ∈ s | G.Adj v w}

Tactic:
ext v

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
v : V
⊢ v ∈ G.neighborFinset w ↔ v ∈ {v ∈ s | G.Adj v w}
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v ⊆ t

Tactic:
rw [isBipartiteWith_neighborFinset h hv]

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} ⊆ t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
hk : k ≠ 0
⊢ G.IsEdgeConnected (k + 1) ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeConnected k

Tactic:
simp [IsEdgeConnected, isEdgeReachable_add_one hk, forall_comm (α := Sym2 _)]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected

Tactic:
exact subgraphOfAdj_connected huv

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
hadj1 : p.toSubgraph.Adj u p.snd
⊢ p.toSubgraph.neighborSet u = {p.snd}

Tactic:
ext v

Goal state after:
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
hadj1 : p.toSubgraph.Adj u p.snd
v : V
⊢ v ∈ p.toSubgraph.neighborSet u ↔ v ∈ {p.snd}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
ext v

Goal state after:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
v : V
⊢ v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ v ∈ {p.getVert (i - 1), p.getVert (i + 1)}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

Tactic:
rw [hp.neighborSet_toSubgraph_internal h h']
  have : p.getVert (i - 1) ≠ p.getVert (i + 1) := by
    intro h
    have := hp.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia) (by rw [Set.mem_ofPred_eq]; lia) h
    lia
  simp_all

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 2 = insert c (G.neighborSet c)

Tactic:
ext v

Goal state after:
V : Type u_1
G : SimpleGraph V
c v : V
⊢ v ∈ G.ball c 2 ↔ v ∈ insert c (G.neighborSet c)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
⊢ p.toSubgraph.neighborSet u = {p.snd, p.penultimate}

Tactic:
ext v

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
v : V
⊢ v ∈ p.toSubgraph.neighborSet u ↔ v ∈ {p.snd, p.penultimate}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
ext v

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
v : V
⊢ v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ v ∈ {p.getVert (i - 1), p.getVert (i + 1)}
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case coe
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
hG : G.chromaticNumber ≤ ↑n
hH : H.chromaticNumber ≤ ↑n
⊢ (G ⊕g H).chromaticNumber ≤ ↑n

Tactic:
let cG : G.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hG).some
    let cH : H.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hH).some
    exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))

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

Goal state before:
pp: V : Type u
G H : SimpleGraph V
h : H ≤ G
hconn : H.Connected
⊢ (toSubgraph H h).verts.Nonempty

Tactic:
simp [hconn.nonempty]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
⊢ (Subgraph.map f G'').coe.Preconnected

Tactic:
intro ⟨u', u, hu, hfu⟩

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
⊢ ∀ (v : ↑(Subgraph.map f G'').verts), (Subgraph.map f G'').coe.Reachable ⟨u', ⋯⟩ v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hconn : G''.Connected
⊢ (Subgraph.map f G'').verts.Nonempty

Tactic:
simp [hconn.nonempty]

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (insert 1 s) = mulCayley s

Tactic:
simp [← Set.union_singleton, ← mulCayley_erase_one]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ (A ⊙ A) i j = A i j

Tactic:
have := hA.zero_or_one i j

Goal state after:
α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
this : A i j = 0 ∨ A i j = 1
⊢ (A ⊙ A) i j = A i j
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
v w : V
⊢ ⋯.toGraph.Adj v w ↔ h.toGraphᶜ.Adj v w

Tactic:
rcases h.zero_or_one v w with h | h <;> by_cases hvw : v = w

Goal state after:
case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.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 : ℕ
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
⊢ (G.replaceVertex s t).neighborFinset s = G.neighborFinset s

Tactic:
ext v

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
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset s ↔ v ∈ G.neighborFinset s
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ (cycleGraph n).chromaticNumber ≤ 2

Tactic:
apply hc.chromaticNumber_le

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 : ℕ
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
⊢ (G.replaceVertex s t).neighborFinset u = G.neighborFinset u \ {t}

Tactic:
ext v

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
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ (cycleGraph n).chromaticNumber ≤ 3

Tactic:
apply hc.chromaticNumber_le

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
hOdd : Odd 2
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
h2 : 2 = n
⊢ False

Tactic:
exact (Nat.not_odd_iff.mpr rfl) hOdd

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'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty
f : ↑G'.oddComponents → ↑G.oddComponents :=
  fun x ↦
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
c c' : ↑G'.oddComponents
fcc' : Exists.choose ⋯ = Exists.choose ⋯
⊢ c = c'

Tactic:
exact Subtype.val_injective (ConnectedComponent.eq_of_common_vertex
    ((fcc' ▸ (aux c.1 c.2).choose_spec.2) (ConnectedComponent.nonempty_supp _).some_mem)
      ((aux c'.1 c'.2).choose_spec.2 (ConnectedComponent.nonempty_supp _).some_mem))

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 rw [verts, disjiUnion_eq_biUnion]

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

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

Tactic:
apply le_antisymm ((h u).symm ▸ edist_le_eccent)

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : ⊤.Adj u v
⊢ 1 ≤ G.edist u v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩
  rw [eq_top_iff_forall_eccent_eq_one]
  intro u
  apply le_antisymm (h ▸ eccent_le_ediam)
  rw [Order.one_le_iff_pos, pos_iff_ne_zero]
  exact eccent_ne_zero u

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

Goal state before:
pp: case inr.inr
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'r : n = n' + r
⊢ #(turanGraph (n' + r) r).edgeFinset =
    ((n' + r) ^ 2 - ((n' + r) % r) ^ 2) * (r - 1) / (2 * r) + ((n' + r) % r).choose 2

Tactic:
card_edgeFinset_turanGraph_add,

Goal state after:
case inr.inr
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'r : n = n' + r
⊢ #(turanGraph n' r).edgeFinset + n' * (r - 1) + r.choose 2 =
    ((n' + r) ^ 2 - ((n' + r) % r) ^ 2) * (r - 1) / (2 * r) + ((n' + r) % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a
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'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) / 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) / 2 * (n' / r + 1) ^ 2

Tactic:
← Nat.choose_two_right

Goal state after:
case inr.inr.e_a
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'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w u✝ : ↑Kᶜ
⊢ Walk.nil.IsPath → f ⋯ = f ⋯

Tactic:
rintro _; rfl

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

Goal state before:
pp: n r : ℕ
⊢ 2 * (r * (n % r * (n % r - 1))) / 2 ≤ (n % r) ^ 2 * (r - 1)

Tactic:
mul_div_cancel_left₀ _ two_ne_zero,

Goal state after:
n r : ℕ
⊢ r * (n % r * (n % r - 1)) ≤ (n % r) ^ 2 * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)

Tactic:
have hπ := tendsto_turanDensity H

Goal state after:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
obtain hs | hs := s.infinite_or_finite
  · exact hs.exists_union_disjoint_cardinal_eq_of_infinite
  classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t, u
  simp [← Finset.coe_union, *]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching → ∀ (v : V), ∃! w, M.Adj v w

pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts

Tactic:
· rintro ⟨hm, hs⟩ v
    exact hm (hs v)

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ (c.toSimpleGraph.spanningCoe.neighborSet v).ncard = 2

Tactic:
← h ⟨w, hw.2⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ (c.toSimpleGraph.spanningCoe.neighborSet v).ncard = (G.neighborSet v).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj v (p.getVert n)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := ⋯
hε' : 0 < ε'
t' : ℕ := ⋯
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := ⋯
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'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ t' ≤ N

Tactic:
exact_mod_cast calc (t' : ℝ)
          _ ≤ r * t' := le_mul_of_one_le_left (by positivity) (mod_cast hr_pos)
          _ ≤ t'.choose t ^ r * t + r * t' := le_add_of_nonneg_left (by positivity)
          _ ≤ (t'.choose t ^ r * t + r * t') * (t' - t) / (r * t' * ε - t) := by
            rw [mul_div_assoc, le_mul_iff_one_le_right (by positivity),
              one_le_div (sub_pos.mpr ht_lt_rt'ε), sub_le_sub_iff_right,
              mul_comm (r : ℝ) (t' : ℝ),  mul_assoc, mul_le_iff_le_one_right (by positivity)]
            exact hrε_lt_1.le
          _ ≤ ⌈(t'.choose t ^ r * t + r * t') * (t' - t) / (r * t' * ε - t)⌉₊ := Nat.le_ceil _
          _ ≤ N := Nat.cast_le.mpr (le_max_right _ _)

Goal state after: