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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
⊢ G.Colorable (card V - 1)

Tactic:
suffices G.Coloring (Finset.univ.erase b) by simpa using Coloring.colorable this

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
⊢ G.Coloring ↥(Finset.univ.erase b)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ¬G.CliqueFree m
⊢ False

Tactic:
simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h

Goal state after:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ∃ x, G.IsClique ↑x ∧ x.card = m
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x✝ : Set (Sym2 V)
hk : x✝.encard < ↑k
⊢ x✝.encard < ↑l

Tactic:
← hkl

Goal state after:
V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x✝ : Set (Sym2 V)
hk : x✝.encard < ↑k
⊢ x✝.encard < ↑k
Module: Mathlib.Combinatorics.SimpleGraph.Metric

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

Tactic:
simp [one_add_one_eq_two.symm, ENat.lt_add_one_iff ENat.one_ne_top,
    edist_le_one_iff_adj_or_eq, adj_comm, or_comm]

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

Goal state before:
pp: case inr.e_a.e_3
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ c.1 = a₁

Tactic:
simp [h₂.2.symm]

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

Goal state before:
pp: case inr.e_a.e_5
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft ≍ if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft else ⋯ ▸ w'.ofBoxProdLeft

Tactic:
simp [h₂.2.symm]

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 β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toLeft
⊢ Sum.inl i ∈ left

Tactic:
simpa using hi

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

Goal state before:
pp: case refine_2.refine_1
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✝
n : Fin n✝
⊢ ↑n.succ < p.support.length

Tactic:
grind [hp₁.three_le_length, length_tail_add_one, not_nil_iff_lt_length]

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 β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toRight
⊢ Sum.inr i ∈ left

Tactic:
simpa using hi

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

Goal state before:
pp: case refine_1.inr.inl.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ ↑left.toRight
j : V
hj : j ∈ ↑right.toLeft
⊢ G.Adj i j

Tactic:
· rw [mem_coe, mem_toRight] at hi
        rw [mem_coe, mem_toLeft] at hj
        simpa using h hi hj

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : Finset.univ.card • 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1

Tactic:
Finset.card_univ,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : Fintype.card V • 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
have ⟨hT, _⟩ := T_isTree

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic✝ : T.IsAcyclic
⊢ ∃ v, (induce {v}ᶜ G).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < min (#univ) r
⊢ False

Tactic:
rw [lt_min_iff] at l

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
by
  by_cases h : G.diam = 0
  · simp [h]
  · obtain ⟨u, v, huv⟩ := exists_edist_eq_ediam_of_ne_top <| ediam_ne_top_of_diam_ne_zero h
    use u, v
    rw [diam, dist, congrArg ENat.toNat huv]

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

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

Tactic:
Nat.mod_eq_of_lt h,

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

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

Tactic:
Nat.mod_le

Goal state after:
n r : ℕ
⊢ n ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)

case ha
n r : ℕ
⊢ 0 ≤ n % r
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)
| ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n) - ↑(#K.verts) * (↑t' - ↑t) - ↑n * (↑(#K.verts) - (↑t' - ↑t))

Tactic:
sub_right_comm,

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)
| ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n) - ↑n * (↑(#K.verts) - (↑t' - ↑t)) - ↑(#K.verts) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
⊢ A.IsHermitian

Tactic:
ext i j
  rcases h.zero_or_one i j with heq | heq
    <;> simp [heq, h.symm.apply]

Goal state after:
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
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ↑(∑ c, ⟨g c • fun i ↦ if G.connectedComponentMk i = c then 1 else 0, ⋯⟩) = fun i ↦ g (G.connectedComponentMk i)

Tactic:
rw [AddSubmonoid.coe_finsetSum]

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i, ↑⟨g i • fun i_1 ↦ if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i ↦ g (G.connectedComponentMk i)
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
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i, ↑⟨g i • fun i_1 ↦ if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i ↦ g (G.connectedComponentMk i)

Tactic:
rw [AddSubmonoid.coe_finsetSum]

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
⊢ ∑ i, ↑⟨g i • fun i_1 ↦ if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩ = fun i ↦ g (G.connectedComponentMk i)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case pos
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
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
· subst hvw
    use .nil

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
j : V
⊢ ↑(∑ x_1, Quot.lift ↑x ⋯ x_1 • ⟨fun i ↦ if G.connectedComponentMk i = x_1 then 1 else 0, ⋯⟩) j = ↑x j

Tactic:
rw [AddSubmonoid.coe_finsetSum]

Goal state after:
case h
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
j : V
⊢ (∑ i, ↑(Quot.lift ↑x ⋯ i • ⟨fun i_1 ↦ if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩)) j = ↑x j
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 : α
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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(insert x (s ∩ t)) = k + 1

Tactic:
card_insert_of_notMem (fun h ↦ G.irrefl (hW h)),

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
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(s ∩ t) + 1 = k + 1
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)
x : α
hx : x ∈ Xᶜ
⊢ 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})

Tactic:
apply card_pos.2

Goal state after:
α : 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 α := ⋯
W : Finset α := ⋯
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)
x : α
hx : x ∈ Xᶜ
⊢ {z ∈ s ∩ t | ¬G.Adj x z}.Nonempty
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' : ℕ
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)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
⊢ ?m.1089

Tactic:
apply ErdosStone.filter.pi.exists_le_card_fiber K hr_pos ht'_pos ht_lt_t' hδ
      rw [← div_le_iff₀ (sub_pos_of_lt ht_lt_rt'ε)]
      trans (N : ℝ)
      · exact (Nat.le_ceil _).trans (Nat.cast_le.mpr <| le_max_right _ _)
      · exact_mod_cast hn

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
this : Nonempty { s // G.IsVertexCover s }
⊢ ∃ s, s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

Tactic:
obtain ⟨s, hs⟩ := @ENat.exists_eq_iInf _ this (·.val.encard)

Goal state after:
V : Type u_1
G : SimpleGraph V
this : Nonempty { s // G.IsVertexCover s }
s : { s // G.IsVertexCover s }
hs : (↑s).encard = ⨅ x, (↑x).encard
⊢ ∃ s, s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i : ℕ
⊢ μ.rowLen i = (μ.row i).card

Tactic:
simp [row_eq_prod]

Goal state after:
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: n : ℕ
⊢ (n + 1).ppred = none ↔ n + 1 = 0

Tactic:
constructor <;> intro <;> contradiction

Goal state after:
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case none
m n : ℕ
s : m.psub n = none
h : n ≤ m
⊢ False

Tactic:
obtain ⟨k, e⟩ := le.dest h

Goal state after:
case none
m n : ℕ
s : m.psub n = none
h : n ≤ m
k : ℕ
e : n + k = m
⊢ False
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode (decode (n + 2))

Tactic:
decode_ge_two

Goal state after:
n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x ↦ Nat.casesOn x 2 fun x ↦ 0) = encode none

case h
n✝ n : ℕ
⊢ 2 ≤ n + 2
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (decode n))

Tactic:
cases @decode α _ n <;> simp [encodek]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (decode n))

Tactic:
by
    cases @decode α _ n <;> simp [encodek]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) (decode n))

Tactic:
cases @decode α _ n <;> simp [encodek]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn (f a) none (g a) = (f a).bind (g a)

Tactic:
cases f a

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn none none (g a) = none.bind (g a)

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
val✝ : β
⊢ Option.casesOn (some val✝) none (g a) = (some val✝).bind (g a)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
IH :
  Nat.rec (some [])
      (fun n IH ↦
        (a, n, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      n =
    some (List.map (f a) (List.range n))
⊢ Nat.rec (some [])
      (fun n IH ↦
        (a, n, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      (n + 1) =
    some (List.map (f a) (List.range (n + 1)))

Tactic:
simp [IH, H, List.range_succ]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode (f a)).ppred = map encode ↑(f a)

Tactic:
cases f a

Goal state after:
case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode Option.none).ppred = map encode ↑Option.none

case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
val✝ : β
⊢ ↑(encode (Option.some val✝)).ppred = map encode ↑(Option.some val✝)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec fun a ↦ Vector.mOfFn fun i ↦ f i a

Tactic:
by
    simp only [Vector.mOfFn, pure_eq_some, bind_eq_bind]
    exact
      (hf 0).bind
        (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
          (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn (f a) Option.none (g a) = (f a).bind (g a)

Tactic:
cases f a

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn Option.none Option.none (g a) = Option.none.bind (g a)

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ Option.casesOn (Option.some val✝) Option.none (g a) = (Option.some val✝).bind (g a)