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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ p.support

Tactic:
rw [Subtype.mk.inj <| hG.subsingleton_path u v |>.elim ⟨p, hp⟩ ⟨_, hq.concat hv hadj.symm⟩]

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∉ q.support
⊢ w ∈ (q.concat ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v w : V
q : G.Path v w := ⋯
⊢ (fun p ↦ p.IsPath) ↑q ∧ ∀ (y : G.Walk v w), (fun p ↦ p.IsPath) y → y = ↑q

Tactic:
simp only [true_and, Path.isPath]

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ ∀ (y : G.Walk v w), y.IsPath → y = ↑q
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ ¬tail.Nil

Tactic:
simp [not_nil_iff_lt_length, h']

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

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂

pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
on_goal 2 =>
    replace e := e.symm

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂

case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
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 v w₁
⊢ G.Adj
      (match a✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match b✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a✝ = b✝ ∧ ¬↑a✝ + 1 = ↑b✝ ∧ ¬↑b✝ + 1 = ↑a✝

Tactic:
have h2 := h.not_adj_snd

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 v w₁
h2 : ¬G.Adj v w₂
⊢ G.Adj
      (match a✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match b✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a✝ = b✝ ∧ ¬↑a✝ + 1 = ↑b✝ ∧ ¬↑b✝ + 1 = ↑a✝
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 (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔ Odd (Nat.card ↑c'.supp)

Tactic:
cases nonempty_fintype V
  rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
  simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
  rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
  congr! 2
  ext c
  simp_rw [Set.toFinset_ofPred, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]

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

Goal state before:
pp: case neg
α : 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)
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
let fᵣ : Fin r ↪ K.parts := Classical.arbitrary (Fin r ↪ K.parts)

Goal state after:
case neg
α : 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)
⊢ (completeEquipartiteGraph r t).Copy G
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
use u, v

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.dist u v = G.diam
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
⊢ G.ediam ≤ 2 * G.radius

Tactic:
obtain ⟨_, _, h⟩ := G.exists_edist_eq_ediam_of_ne_top hdiam

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.ediam ≤ 2 * G.radius
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_5
α : 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
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
h₂ : ∃ y, map { toFun := fun j ↦ f (y, j), inj' := ⋯ } univ = x✝²
w✝ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝³
⊢ G.Adj x✝¹ x✝

Tactic:
replace ⟨_, h₂⟩ := h₂

Goal state after:
case neg.refine_5
α : 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
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: 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 : ↑Kᶜ
p : (induce Kᶜ G).Walk v w
⊢ p.IsPath → f ⋯ = f ⋯

Tactic:
by
    induction p with
    | nil => rintro _; rfl
    | cons a q ih => rename_i u v w; rintro h'; exact (h u.prop v.prop a).trans (ih h'.of_cons)

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

Goal state before:
pp: case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ Nonempty (G →g F)

Tactic:
refine ⟨⟨fun v => ?_, ?_⟩⟩

Goal state after:
case intro.refine_1
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ W

case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ ∀ {a b : V}, G.Adj a b → F.Adj ?intro.refine_1 ?intro.refine_1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
x✝¹ x✝ : Fin m ⊕ Fin n
hadj : G.Adj x✝¹ x✝
h_le : (completeBipartiteGraph V W).Adj (e₁.toEmbedding x✝¹) (e₁.toEmbedding x✝)
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph V W)).Adj x✝¹ x✝

Tactic:
← comap_adj

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
x✝¹ x✝ : Fin m ⊕ Fin n
hadj : G.Adj x✝¹ x✝
h_le : (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph V W)).Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph V W)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_free : (completeBipartiteGraph α β).Free G
x✝¹ x✝ : V ⊕ W
hadj : G.Adj x✝¹ x✝
h_le : (completeBipartiteGraph (Fin m) (Fin n)).Adj (e₁.toEmbedding x✝¹) (e₁.toEmbedding x✝)
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝

Tactic:
← comap_adj

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_free : (completeBipartiteGraph α β).Free G
x✝¹ x✝ : V ⊕ W
hadj : G.Adj x✝¹ x✝
h_le : (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
by_cases! h : ∀ i ∈ t, (s i).Finite

Goal state after:
case pos
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∃ i ∈ t, (s i).Infinite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
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 ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ ∃ M, p₁ ⊆ M.verts ∧ M.IsMatching

Tactic:
by
  classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)

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
⊢ ¬G.Colorable (r + 1)

Tactic:
by
  intro ⟨C⟩
  have h := C.surjOn_of_card_le_isClique hw.isNClique_fst_left.1 (by simp [hw.isNClique_fst_left.2])
  have := C.surjOn_of_card_le_isClique hw.isNClique_snd_right.1 (by simp [hw.isNClique_snd_right.2])
  -- Since `C` is an `r + 1`-coloring and `insert w₁ s` is an `r + 1`-clique, it contains a vertex
  -- `x` which shares its color with `v`
  obtain ⟨x, hx, hcx⟩ := h (a := C v) trivial
  -- Similarly there is a vertex `y` in `insert w₂ t` which shares its color with `v`.
  obtain ⟨y, hy, hcy⟩ := this (a := C v) trivial
  rw [coe_insert] at *
  -- However since `insert v s` and `insert v t` are cliques, we must have `x = w₁` and `y = w₂`.
  cases hx with
  | inl hx =>
    cases hy with
    | inl hy =>
    -- But this is a contradiction since `w₁` and `w₂` are adjacent.
      subst_vars; exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)
    | inr hy =>
      apply (C.valid _ hcy.symm).elim
      exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)
  | inr hx =>
    apply (C.valid _ hcx.symm).elim
    exact hw.isNClique_left.1 (by simp) (by simp [hx]) fun h ↦ hw.notMem_left (h ▸ hx)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G.subgraphOfAdj h).IsMatching

Tactic:
intro _ hv
  rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv
  cases hv with
  | inl => use w; aesop
  | inr => use v; aesop

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
h : M.IsMatching
v : V
hv : v ∈ M.verts
u : V
he : (fun w ↦ M.Adj v w) u
right✝ : ∀ (y : V), (fun w ↦ M.Adj v w) y → y = u
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i

Tactic:
exact ⟨s(v, u), he, Sym2.mem_mk_left ..⟩

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)
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)))
hca : c = a
hdb : d = b
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))

Tactic:
simp_rw [hca, hdb, mem_insert] at *

Goal state after:
α : 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 : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i : V
| fun x_2 ↦ if G.Adj i x_2 then x i * x i - x i * x x_2 else 0

Tactic:
j

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i j : V
| if G.Adj i j then x i * x i - x i * x j else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i : V
⊢ ∀ (j : V), G.Reachable i j → x i = x j

Tactic:
j

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
⊢ G.Reachable i j → x i = x j
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n → G.Colorable n

pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → G.Partitionable n

Tactic:
· rintro ⟨P, hf, hc⟩
    have : Fintype P.parts := hf.fintype
    rw [Set.Finite.card_toFinset hf] at hc
    apply P.colorable.mono hc

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → G.Partitionable n
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ (fun w ↦ ⊤.Adj v w) w ∧ ∀ (y : V), (fun w ↦ ⊤.Adj v w) y → y = w

Tactic:
simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hw.1, h,
      not_false_eq_true, and_self, not_true_eq_false, or_false, true_and]

Goal state after:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

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

Tactic:
by_contra! hnotcol

Goal state after:
α : Type u_1
G : SimpleGraph α
r✝ : ℕ
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun H ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
have hM1sub := Subgraph.spanningCoe_le M1

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n k : ℕ
⊢ (∃ a, m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m

Tactic:
simp only [psub_eq_some, ppred_eq_some]

Goal state after:
m n k : ℕ
⊢ (∃ a, a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f

Tactic:
by simp [Partrec, map_id']

Goal state after: