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

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

Tactic:
rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]

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

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · use G.radius
    intro u
    exact le_antisymm (h ▸ eccent_le_ediam) radius_le_eccent
  · obtain ⟨e, h⟩ := h
    have ediam_eq : G.ediam = e :=
      le_antisymm (iSup_le fun u ↦ (h u).le) ((h Classical.ofNonempty) ▸ eccent_le_ediam)
    rw [ediam_eq]
    exact le_antisymm ((h Classical.ofNonempty) ▸ radius_le_eccent) (le_iInf fun u ↦ (h u).ge)

Goal state after:
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✝²
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✝

Tactic:
rw [← h₁] at 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✝¹ x✝ : V
h₂' : x✝ ∈ ↑x✝²
w✝¹ : Fin r
h₁' : x✝¹ ∈ ↑(map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ)
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.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).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
rw [n'r, card_edgeFinset_turanGraph_add, card_edgeFinset_turanGraph, ring₁, ring₁,
        add_rotate, ← add_assoc, Nat.add_mod_right, Nat.add_div_right _ hr]

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
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2) + (n' % r).choose 2 =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * (n' / r + 1) ^ 2 / 2 + (n' % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ K.vertsᶜ \ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) +
      ∑ v ∈ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤
    ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts)

Tactic:
apply add_le_add <;> refine sum_le_sum (fun v hv ↦ ?_)

Goal state after:
case h₁
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
v : Fin n
hv : v ∈ K.vertsᶜ \ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts) - ↑t' + ↑t

case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
v : Fin n
hv : v ∈ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t u : Finset α
hdtu : Disjoint t u
hctu : #t = #u
⊢ Even #(t ∪ u)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ Nonempty (↑s ≃ ↑s ⊕ ↑s)

Tactic:
← Cardinal.eq,

Goal state after:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ #↑s = #(↑s ⊕ ↑s)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑r * ↑t' * ε - ↑t' + (↑t' - ↑t)) - ↑r * ↑t' * (↑t' - ↑t)

Tactic:
sub_add_sub_cancel

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)
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
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v : V
h' : v ∈ p₁
⊢ (fun w ↦ if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False) (f ⟨v, h'⟩) ∧
    ∀ (y : V),
      (fun w ↦ if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False) y → y = f ⟨v, h'⟩

Tactic:
simp_all

Goal state after:
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:
| inl hmM =>

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

Goal state before:
pp: case refine_3
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, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

pp: case refine_4
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, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b

Tactic:
· exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)

Goal state after:
case refine_4
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, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ Nonempty (↑t ≃ ↑u)

Tactic:
← Cardinal.eq,

Goal state after:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ Cardinal.mk ↑t = Cardinal.mk ↑u
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
← Cardinal.eq,

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ Cardinal.mk ↑(G.neighborSet v) = Cardinal.mk ↑(p.toSubgraph.neighborSet v)
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)
⊢ Nonempty (↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n)))

Tactic:
← Cardinal.eq,

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)
⊢ Cardinal.mk ↑(G.neighborSet (p.getVert n)) = Cardinal.mk ↑(p.toSubgraph.neighborSet (p.getVert n))
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
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ (Walk.cons ⋯ p).IsPath

Tactic:
Walk.cons_isPath_iff

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
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ p.IsPath ∧ w' ∉ p.support
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
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
← Cardinal.eq,

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
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ Cardinal.mk ↑(G.neighborSet v) = Cardinal.mk ↑(p.toSubgraph.neighborSet v)
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
this : v ∈ c'.supp
⊢ c'.supp = c.supp

Tactic:
simp_all

Goal state after:
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
hc : 2 < G.edist u v
⊢ False

Tactic:
obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc

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
hc : 2 < G.edist u v
hn : u ≠ v
ha : ¬G.Adj u v
he : G.commonNeighbors u v = ∅
⊢ False
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
hc : 2 < G.edist u v
hn : u ≠ v
ha : ¬G.Adj u v
he : G.commonNeighbors u v = ∅
h : Fintype.card ↑(G.commonNeighbors u v) = μ
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case neg.inl.inr.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
h2r1 : v = x
h2r2 : w' = u
⊢ G'.Adj v w

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
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
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
by
      simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add,
               ← hw.card_inter, card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
      gcongr with i <;> exact minDegree_le_degree ..

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
he : e ∈ G.edgeSet
⊢ e ∈ p.edges

Tactic:
simpa [Nat.succ_le_iff] using (h e he).ge

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ Nonempty (↑s ≃ ↑t)

Tactic:
← Cardinal.eq,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ Cardinal.mk ↑s = Cardinal.mk ↑t
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover ∅ ↔ G = ⊥

Tactic:
simp [IsVertexCover, eq_bot_iff_forall_not_adj]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G = ⊥ → G.vertexCoverNum = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i₁ : ιₚ
g₁ g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ }.groupElts}
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts

Tactic:
· exact heq_of_eq (Set.singleton_eq_singleton_iff.1
        ((Set.preimage_eq_preimage Quotient.mk''_surjective).1 hq))

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case cons.zero
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
snd✝ : ℕ
⊢ (0, snd✝) ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : (0, snd✝).1 < (head✝ :: tail✝).length), (0, snd✝).2 < (head✝ :: tail✝)[(0, snd✝).1]

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case cons.succ
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
snd✝ n✝ : ℕ
⊢ (n✝ + 1, snd✝) ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : (n✝ + 1, snd✝).1 < (head✝ :: tail✝).length), (n✝ + 1, snd✝).2 < (head✝ :: tail✝)[(n✝ + 1, snd✝).1]

Tactic:
simp_all

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

Goal state before:
pp: case h
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
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∉ (cycles.connectedComponentMk c).supp
⊢ ¬(x ∈ (cycles.connectedComponentMk c).supp ∧ cycles.Adj x b)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k

Tactic:
le_antisymm_iff,

Goal state after:
this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q ≤ a / k ∧ a / k ≤ q
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif n.bodd then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match n.bodd, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))

Tactic:
cases Nat.bodd n

Goal state after:
case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif false then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match false, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))

case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif true then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match true, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons.zero.nil
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
a : α
⊢ [a][0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) [])

Tactic:
simp_all

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons.zero.cons
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
a head✝ : α
tail✝ : List α
tail_ih✝ :
  (a :: tail✝)[0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) tail✝)
⊢ (a :: head✝ :: tail✝)[0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) (head✝ :: tail✝))

Tactic:
simp_all

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some.zero
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ ((Part.map encode (Part.some 0)).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) 0)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
n✝ : ℕ
a✝ :
  ((Part.map encode (Part.some n✝)).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) n✝)
⊢ ((Part.map encode (Part.some (n✝ + 1))).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (n✝ + 1))

Tactic:
simp_all

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 0 n = n + 1

Tactic:
by rw [ack]

Goal state after: