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

Goal state before:
pp: case inl.mk
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 V
u v : V
h : Quot.mk (Sym2.Rel V) (u, v) ∈ G.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩)) =
    Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩

Tactic:
rfl

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

Goal state before:
pp: case inr.mk
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 W
u v : W
h : Quot.mk (Sym2.Rel W) (u, v) ∈ H.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩)) =
    Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩

Tactic:
rfl

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

Goal state before:
pp: case inl
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : V
⊢ (c.sumLeft.sum c.sumRight) (Sum.inl u) = c (Sum.inl u)

Tactic:
rfl

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

Goal state before:
pp: case inr
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : W
⊢ (c.sumLeft.sum c.sumRight) (Sum.inr u) = c (Sum.inr u)

Tactic:
rfl

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

Goal state before:
pp: u v : Fin 1
⊢ ¬(cycleGraph 1).Adj u v

Tactic:
simp [cycleGraph_one_eq_bot]

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

Goal state before:
pp: n : ℕ
h : 0 < n + 3
⊢ nil.length = ↑⟨0, h⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v✝ : V
h✝¹ : G.Adj u v✝
h✝ : G.Adj v✝ v
hp : (Walk.cons h✝¹ (Walk.cons h✝ Walk.nil)).length = 2
⊢ (fun w ↦ ⟨(Adj.toWalk ⋯).concat ⋯, ⋯⟩) ((fun p ↦ ⟨(↑p).snd, ⋯⟩) ⟨Walk.cons h✝¹ (Walk.cons h✝ Walk.nil), hp⟩) =
    ⟨Walk.cons h✝¹ (Walk.cons h✝ Walk.nil), hp⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: case succ.f.e'_4
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v x✝¹ : V
h_congr_thm✝ :
  ∀ {α : Type u} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q),
    (∀ (x : q), f₁ ⋯ = f₂ x) → Set.iUnion f₁ = Set.iUnion f₂
x✝ : G.Adj u x✝¹
⊢ ↑(G.finsetWalkLength n x✝¹ v) = {p' | p'.length = n}

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
hlen : p.tail.support.length = n
m : Fin n
⊢ ↑m.succ < p.support.length

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
x✝¹ x✝ : G
⊢ ¬x✝¹ = x✝ ∧ (x✝¹ - x✝ ∈ s ∨ x✝ - x✝¹ ∈ s) ↔ ¬x✝¹ = x✝ ∧ ((x✝¹ - x✝ ∈ s ∨ x✝ - x✝¹ ∈ s) ∨ x✝ - x✝¹ ∈ s ∨ x✝¹ - x✝ ∈ s)

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
hHG : H ≤ G
hH : H.IsAcyclic
c : Set (SimpleGraph V)
hcs : c ⊆ {H | H ≤ G ∧ H.IsAcyclic}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : SimpleGraph V
hy : y ∈ c
⊢ ∀ H ∈ c, H.IsAcyclic

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i : V
⊢ ¬A i i = 1

Tactic:
by simp [h.apply_diag i]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
x✝ : ∃ G x, H.Free G ∧ m < #G.edgeFinset
w✝¹ : SimpleGraph V
w✝ : DecidableRel w✝¹.Adj
h : H.Free w✝¹
h' : m < #w✝¹.edgeFinset
⊢ m < #w✝¹.edgeFinset

Tactic:
by convert!
    h'

Goal state after:
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✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (¬i = j → A i j = 0 → 1 = 0) ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1

Tactic:
grind

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

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ (↑univ).PairwiseDisjoint fun w ↦
    Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)

Tactic:
rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy

Goal state after:
case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
⊢ Function.onFun Disjoint
    (fun w ↦ Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)) ⟨x, hx⟩ ⟨y, hy⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
x✝ : G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
hacyc : G.IsAcyclic
hreach : G.Reachable u v → u = v ∨ G.Adj u v
⊢ ¬G.Reachable u v

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
⊢ {e} \ Sym2.diagSet ⊆ H.edgeSet

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hF : ⊥ ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
⊢ ¬p.Nil

Tactic:
grind

Goal state after:
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))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
⊢ 3 ≤ (cycleGraph n).chromaticNumber

Tactic:
have hOdd' : Odd w.length := by
      rw [cycleGraph.length_cycle, hn3]
      exact hOdd

Goal state after:
case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
hOdd' : Odd w.length
⊢ 3 ≤ (cycleGraph n).chromaticNumber
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
⊢ C = C'

Tactic:
by
  funext ⟨e, he⟩
  induction e using Sym2.inductionOn
  exact h _ _ he

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
a b : V
⊢ ∀ (a_1 : G.Adj a b) (a' : G.Adj b a), a_1 ≍ a' → f a b a_1 ≍ f b a a'

Tactic:
grind

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
x y : V
⊢ (∃ i, ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = i) ↔ G.Adj x y

Tactic:
grind

Goal state after:
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
⊢ p.length ≠ q.length

Tactic:
rw [hG.path_concat hq hp hadj.symm hw, q.length_concat]
    exact q.length.ne_add_one.symm

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

Goal state before:
pp: r t : ℕ
v w : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1

Tactic:
rfl

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

Goal state before:
pp: case map_rel_iff'.inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : r ≤ Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r

Tactic:
rfl

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

Goal state before:
pp: case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩)

Tactic:
← Nat.mod_eq_of_lt ((lc b).trans c)

Goal state after:
case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r

Tactic:
rfl

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:
rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]

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

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ ENat.toNat 0 = 0

Tactic:
rfl

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

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

Tactic:
grind

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, ∀ p ∈ K.parts, ∀ ⦃v₁ : V⦄, v₁ ∈ p → ∀ ⦃v₂ : V⦄, True

Tactic:
implies_true,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, True
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
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ ∃ s ∉ K.parts, insert s K.parts = K'.parts

Tactic:
refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩
        rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]

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'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2

Tactic:
grind

Goal state after:
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ᶜ
a✝ : Walk.nil.IsPath
⊢ f ⋯ = f ⋯

Tactic:
rfl

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x✝ : V
xnL : x✝ ∉ L
x : V
w✝¹ : x ∉ L
e₁ : G.componentComplMk w✝¹ = G.componentComplMk xnL
w✝ : x ∉ K
⊢ hom h (G.componentComplMk w✝¹) = G.componentComplMk w✝

Tactic:
rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C = ConnectedComponent.map (induceHom (Hom.id.comp Hom.id) ⋯) C

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
⊢ ∀ {v w : V}, (if h : v ∈ p then f ⟨v, h⟩ = w else if h : w ∈ p then f ⟨w, h⟩ = v else False) → v ∈ p ∪ Set.range f

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
⊢ ∀ (a b : V),
    (if h : a ∈ p then f ⟨a, h⟩ = b else if h : b ∈ p then f ⟨b, h⟩ = a else False) →
      if h : b ∈ p then f ⟨b, h⟩ = a else if h : a ∈ p then f ⟨a, h⟩ = b else False

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
left✝ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
x : V
this : x ∈ p₁ ∧ f x ∈ p₂ ∨ x ∈ p₂ ∧ f x ∈ p₁
⊢ x ∈ p₁ ∪ p₂

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
x : ↑p₁
⊢ f ↑x ∈ p₂

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
x : ↑p₂
⊢ f ↑x ∈ p₁

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : G.CliqueFree (r + 2)
⊢ k < r

Tactic:
by
  contrapose! h
  -- If `r ≤ k` then `s = t` and so `s ∪ {w₁, w₂}` is an `r + 2`-clique, a contradiction.
  have hs := eq_of_subset_of_card_le inter_subset_left (hw.card_inter ▸ hw.card_left ▸ h)
  have := eq_of_subset_of_card_le inter_subset_right (hw.card_inter ▸ hw.card_right ▸ h)
  exact (hw.isNClique_fst_left.insert_insert (hs ▸ this.symm ▸ hw.isNClique_snd_right)
    hw.snd_notMem_left hw.isPathGraph3Compl.adj).not_cliqueFree

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ w ∈ W, G.degree w = ∑ v, #(G.neighborFinset v ∩ W)

Tactic:
by
    simp_rw [degree, card_eq_sum_ones]
    exact sum_comm' (by simp [and_comm, adj_comm])

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
this : (p₁ ∪ Set.range fun v ↦ ↑(b v)) = Set.univ
v : V
x✝ : v ∈ (hall_subgraph (fun v ↦ ↑(b v)) ⋯ hb₂).verts
h✝ : v ∉ p₁
⊢ v ∈ p₂

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
this : (p₁ ∪ Set.range fun v ↦ ↑(b v)) = Set.univ
v : V
x✝ : v ∈ (hall_subgraph (fun v ↦ ↑(b v)) ⋯ hb₂).verts
h✝¹ : v ∉ p₁
x : ↑p₁
h✝ : (fun a ↦ b a = ⟨v, ⋯⟩) x ∧ ∀ (y : ↑p₁), (fun a ↦ b a = ⟨v, ⋯⟩) y → y = x
⊢ (fun w ↦ ∃ (h : w ∈ p₁), ↑(b ⟨w, ⋯⟩) = v) ↑x ∧ ∀ (y : V), (fun w ↦ ∃ (h : w ∈ p₁), ↑(b ⟨w, ⋯⟩) = v) y → y = ↑x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
c : α
hc : c ∈ insert v s
hcj : ¬G.Adj x c
d : α
hd : d ∈ insert v t
hdj : ¬G.Adj x d
⊢ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s

Tactic:
grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ {v w : V}, ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → v ∈ s ∪ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.support = 1

Tactic:
← cons_support_tail hp.1.not_nil,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b (a :: p.tail.support) = 1
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : c = a → d ≠ b
h : a = c
⊢ a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
    b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      d ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ d ∧ b ≠ d

Tactic:
grind

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a

Tactic:
rfl

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

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ↑(f ⟨v, ⋯⟩) = ↑(f ⟨v, hl⟩)

Tactic:
rfl

Goal state after: