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

Goal state before:
pp: case pos
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∈ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

pp: case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
· exact Or.inl ⟨hadj, Or.inr ⟨hw, hv⟩⟩

Goal state after:
case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ G.edgeSet.encard ≤ s.encard * t.encard

Tactic:
hG.edgeSetEmbeddingCompleteBipartiteGraph.encard_le

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ (completeBipartiteGraph ↑s ↑t).edgeSet.encard ≤ s.encard * t.encard
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G✝ : SimpleGraph V
s t : Set V
G : SimpleGraph V
x✝¹ x✝ : V ⊕ V
⊢ (match x✝¹, x✝ with
    | Sum.inl v', Sum.inr w' => G.Adj v' w'
    | Sum.inr v', Sum.inl w' => G.Adj v' w'
    | x, x_1 => False) →
    match x✝, x✝¹ with
    | Sum.inl v', Sum.inr w' => G.Adj v' w'
    | Sum.inr v', Sum.inl w' => G.Adj v' w'
    | x, x_1 => False

Tactic:
by grind [adj_symm]

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u : V
⊢ ∀ {v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
v

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
⊢ u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n✝ n : ℕ
u : Fin (n + 2)
⊢ ∀ ⦃w : Fin (n + 2)⦄, (pathGraph (n + 2)).Adj u w → (cycleGraph (n + 2)).Adj u w

Tactic:
v

Goal state after:
n✝ n : ℕ
u v : Fin (n + 2)
⊢ (pathGraph (n + 2)).Adj u v → (cycleGraph (n + 2)).Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ {p | p.length = n + 1} ↔ p ∈ ⋃ w, ⋃ (h : G.Adj u w), cons h '' {p' | p'.length = n}

Tactic:
cases p with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
have : Fintype α := .ofFinite α
  have : Fintype β := .ofFinite β
  simp_rw [completeBipartiteGraph_isContained_iff]
  refine ⟨fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_,
    fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_⟩
  · simp_rw [← card_left, ← card_right]
    obtain ⟨l, hl⟩ : left.Nonempty := card_pos.mp <| card_pos.trans_le card_left.ge
    obtain ⟨r, hr⟩ : right.Nonempty := card_pos.mp <| card_pos.trans_le card_right.ge
    have hmem_left {l'} (hl' : l' ∈ left) :
        (l.isLeft → l'.isLeft) ∧ (l.isRight → l'.isRight) := by
      rcases l with l | l <;> rcases r with r | r <;> rcases l' with l' | l'
      all_goals solve | simp | simpa using h hl hr | simpa using h hl' hr
    have hmem_right {r'} (hr' : r' ∈ right) :
        (r.isLeft → r'.isLeft) ∧ (r.isRight → r'.isRight) := by
      rcases l with l | l <;> rcases r with r | r <;> rcases r' with r' | r'
      all_goals solve | simp | simpa using h hl hr | simpa using h hl hr'
    rcases l with l | l <;> rcases r with r | r
    · simpa using h hl hr
    · refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩
      · exact card_bij (fun i _ ↦ .inl i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getLeft <| (hmem_left hi).left Sum.isLeft_inl, by simp [hi]⟩)
      · exact card_bij (fun j hj ↦ .inr j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getRight <| (hmem_right hj).right Sum.isRight_inr, by simp [hj]⟩)
      · rw [mem_coe, mem_toLeft] at hi
        rw [mem_coe, mem_toRight] at hj
        simpa using h hi hj
    · refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
      · exact card_bij (fun i _ ↦ .inr i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getRight <| (hmem_left hi).right Sum.isRight_inr, by simp [hi]⟩)
      · exact card_bij (fun j hj ↦ .inl j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getLeft <| (hmem_right hj).left Sum.isLeft_inl, by simp [hj]⟩)
      · rw [mem_coe, mem_toRight] at hi
        rw [mem_coe, mem_toLeft] at hj
        simpa using h hi hj
    · simpa using h hl hr
  · simp_rw [← card_left, ← card_right]
    refine ⟨left.map .inl, right.map .inr, card_map _, card_map _, fun i hi j hj ↦ ?_⟩
    simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj
    obtain ⟨i', hi', hi⟩ := hi
    obtain ⟨j', hj', hj⟩ := hj
    simpa [← hi, ← hj] using h hi' hj'

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i✝ j✝ : V
⊢ A.compl.compl i✝ j✝ = A i✝ j✝

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
  as we are relying on seeing through the definition of `Matrix`, and `of`. The original proof was:
  `grind [of, compl, IsAdjMatrix]` -/

Goal state after:
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i✝ j✝ : V
⊢ A.compl.compl i✝ j✝ = A i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
u : Fin n
⊢ ∀ {w : Fin n}, (pathGraph n).Adj u w → decide (↑u % 2 = 0) ≠ decide (↑w % 2 = 0)

Tactic:
v

Goal state after:
n : ℕ
u v : Fin n
⊢ (pathGraph n).Adj u v → decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : Even n
u : Fin n
⊢ ∀ {w : Fin n}, (cycleGraph n).Adj u w → decide (↑u % 2 = 0) ≠ decide (↑w % 2 = 0)

Tactic:
v

Goal state after:
n : ℕ
h : Even n
u v : Fin n
⊢ (cycleGraph n).Adj u v → decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
u : Fin n
⊢ ∀ {w : Fin n},
    (cycleGraph n).Adj u w → (if ↑u = n - 1 then 2 else ⟨↑u % 2, ⋯⟩) ≠ if ↑w = n - 1 then 2 else ⟨↑w % 2, ⋯⟩

Tactic:
v

Goal state after:
n : ℕ
h : 2 ≤ n
u v : Fin n
⊢ (cycleGraph n).Adj u v → (if ↑u = n - 1 then 2 else ⟨↑u % 2, ⋯⟩) ≠ if ↑v = n - 1 then 2 else ⟨↑v % 2, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩

Tactic:
simp only [ne_eq, Fin.ext_iff]

Goal state after:
case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ¬↑u % 2 = ↑v % 2
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u : V
⊢ ∀ {b : V},
    G.Adj u b →
      (completeGraph (Fin 2)).Adj
        (let u_1 := verts (G.connectedComponentMk u);
        ⟨G.dist u_1 u % 2, ⋯⟩)
        (let u := verts (G.connectedComponentMk b);
        ⟨G.dist u b % 2, ⋯⟩)

Tactic:
v

Goal state after:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
⊢ G.Adj u v →
    (completeGraph (Fin 2)).Adj
      (let u_1 := verts (G.connectedComponentMk u);
      ⟨G.dist u_1 u % 2, ⋯⟩)
      (let u := verts (G.connectedComponentMk v);
      ⟨G.dist u v % 2, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
| fun x ↦ ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

Tactic:
v

Goal state after:
n r : ℕ
v : Fin (n + r)
| ∑ i, if ↑v % r ≠ ↑i % r then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

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

Tactic:
v

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
⊢ u ≠ v → G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
Cinf : C.supp.Infinite
L : Finset V
h : K ⊆ L
⊢ ∃ D, hom h D = C

Tactic:
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.sdiff Cinf L.finite_toSet)

Goal state after:
case mp
V : Type u
G : SimpleGraph V
K L : Finset V
h : K ⊆ L
v : V
vL : v ∉ ↑L
vK : v ∉ ↑K
Cinf : (G.componentComplMk vK).supp.Infinite
⊢ ∃ D, hom h D = G.componentComplMk vK
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
this : Subsingleton G.ConnectedComponent
⊢ Finite (induce Set.univ G).ConnectedComponent

Tactic:
exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ ↑(#K.verts) * (↑G.minDegree - ↑(#K.verts)) ≤ ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset)

Tactic:
← isBipartiteWith_sum_degrees_eq_card_edges (between_verts_isBipartiteWith K),

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ ↑(#K.verts) * (↑G.minDegree - ↑(#K.verts)) ≤ ↑(∑ v ∈ K.verts, (between (↑K.verts) (↑K.verts)ᶜ G).degree v)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM : v ∈ M.verts
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
exact aux hM hd hmM

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

Goal state before:
pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
let ε' := 1 / (↑(r - 1) * r) + ε

Goal state after:
case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x : α
hp : nil.IsHamiltonianCycle
__IsCycle✝ : (Walk.map f nil).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (Walk.map f nil).tail.support = 1

pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
__IsCycle✝ : (Walk.map f (cons y p)).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (Walk.map f (cons y p)).tail.support = 1

Tactic:
· cases hp.ne_nil rfl

Goal state after:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
__IsCycle✝ : (Walk.map f (cons y p)).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (Walk.map f (cons y p)).tail.support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ Even M.verts.toFinset.card

Tactic:
use M.coe.edgeFinset.card

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
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 : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
h1_le_rε : 1 ≤ 1 - (1 / ↑r - ε)
⊢ ↑n ≤ ↑G.minDegree

Tactic:
← sub_add

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
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 : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
h1_le_rε : 1 ≤ 1 - 1 / ↑r + ε
⊢ ↑n ≤ ↑G.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case refine_1
α : 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
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ v ≠ x

Tactic:
by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax

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

Goal state before:
pp: 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)
⊢ ↑(G.neighborSet (p.getVert n)).ncard = ↑(p.toSubgraph.neighborSet (p.getVert n)).ncard

Tactic:
hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),

Goal state after:
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)
⊢ ↑(G.neighborSet (p.getVert n)).ncard = ↑2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ c'.supp

Tactic:
rw [← hc', Walk.mem_verts_toSubgraph]

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u : V
⊢ ∀ (v : V), G.edist u v ≤ 2

Tactic:
v

Goal state after:
case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
⊢ G.edist u v ≤ 2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w ∩ G.neighborFinset v) = ℓ

Tactic:
simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw,
        ← Set.toFinset_card]

Goal state after:
case convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
this : ↑n ≤ ((fun x ↦ (Quot.out x).1) '' G.edgeSet).encard
⊢ ↑n ≤ G.edgeSet.encard

Tactic:
grind [Set.encard_image_le]

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

Goal state before:
pp: case refine_2
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
hadj : p.toSubgraph.Adj x a
⊢ False

Tactic:
simp [← hp.snd_of_toSubgraph_adj hadj.symm, hp.snd_of_toSubgraph_adj hpac] at hnxc

Goal state after:
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
⊢ ∃ M, M.IsPerfectMatching

Tactic:
simp only [not_not] at hM1xb hM2ac

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
⊢ ∃ M, M.IsPerfectMatching
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case none
m n : ℕ
s : m.psub n = none
⊢ none = none ↔ m < n

pp: case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ some val✝ = none ↔ m < n

Tactic:
· simp only [true_iff]
    refine lt_of_not_ge fun h => ?_
    obtain ⟨k, e⟩ := le.dest h
    injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)

Goal state after:
case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ some val✝ = none ↔ m < n
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case true
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = true
⊢ { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }

Tactic:
exact ⟨m, ⟨_, e⟩, al⟩

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
⊢ n ∈ rfind p

Tactic:
let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
    rcases lt_trichotomy m n with (h | h | h)
    · injection mem_unique (h₂ h) (rfind_spec hm)
    · rwa [← h]
    · injection mem_unique h₁ (rfind_min hm h)

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
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
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' b

Tactic:
rw [hw _ hM1xb, ← hw _ hl.1.symm]
      exact hadj.symm

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
a₂ : α
am₂ :
  Sum.inr a₂ ∈
    Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s) m
fa₂ : Sum.inr a' ∈ f a₂
⊢ b ∈ f.fix a

Tactic:
exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))

Goal state after: