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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
obtain heP | heP := em' <| s(x, y) ∈ P.edges

Goal state after:
case inr.inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

case inr.inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ (completeBipartiteGraph V W).chromaticNumber = ↑2

Tactic:
chromaticNumber_eq_iff_forall_surjective
    (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)

Goal state after:
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ ∀ (C : (completeBipartiteGraph V W).Coloring (Fin 2)), Surjective ⇑C
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case pos
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : C (Sum.inl v) = b
⊢ ∃ a, C a = b

Tactic:
exact ⟨_, he⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
not_nil_iff_lt_length

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
⊢ ∀ {a b : V ⊕ W}, (H ⊕g G).Adj ((Equiv.sumComm V W) a) ((Equiv.sumComm V W) b) ↔ (G ⊕g H).Adj a b

Tactic:
rintro (u | u) (v | v) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y ∈ (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯ ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x

Tactic:
by
      simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset,
        mem_neighborSet, Equiv.refl_apply, boxProd_adj]
      simp only [eq_comm, and_comm]

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

Goal state before:
pp: case inl.inr.inl
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
r' : V
hr' : Sum.inl r' ∈ right
⊢ ((Sum.inr r).isLeft = true → (Sum.inl r').isLeft = true) ∧ ((Sum.inr r).isRight = true → (Sum.inl r').isRight = true)

Tactic:
simpa using h hl hr'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).degree x = G.degree x.1 + H.degree x.2

Tactic:
by
  rw [degree, degree, degree, neighborFinset_boxProd, Finset.card_disjUnion]
  simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]

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

Goal state before:
pp: case inr.inl.inr
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
r' : V
hr' : Sum.inr r' ∈ right
⊢ ((Sum.inl r).isLeft = true → (Sum.inr r').isLeft = true) ∧ ((Sum.inl r).isRight = true → (Sum.inr r').isRight = true)

Tactic:
simpa using h hl hr'

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y

Tactic:
· have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
      rw [← hw, Walk.length_boxProd]
      exact add_le_add (edist_le w.ofBoxProdLeft) (edist_le w.ofBoxProdRight)

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

pp: case mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s

Tactic:
· intro h1
    cases h1 with
      | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
      | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Preconnected

Tactic:
intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp [neighborFinset_eq_filter, dotProduct, sum_filter]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ vec ⬝ᵥ adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp [neighborFinset_eq_filter, dotProduct, sum_filter]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : AddCommMonoid α
inst✝ : One α
⊢ (adjMatrix α G).trace = 0

Tactic:
by
  simp [Matrix.trace]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ s(u, v) ∈ (G ⊔ edge u v).edgeSet

Tactic:
by simp [huv]

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
⊢ False

Tactic:
have ⟨e, heH, heF⟩ := Set.exists_of_ssubset <| edgeSet_strict_mono hFH

Goal state after:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : ¬2 ≤ G.minDegree
⊢ G.minDegree = 1

Tactic:
· have := h.preconnected.minDegree_pos_of_nontrivial
    lia

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

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (⊤.Free G ∧ ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], ⊤.Free G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    G.CliqueFree (Fintype.card α) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj],
        G'.CliqueFree (Fintype.card α) → #G'.edgeFinset ≤ #G.edgeFinset

Tactic:
cliqueFree_iff_top_free

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

Goal state before:
pp: n r : ℕ
⊢ ∑ x, #{x_1 | ↑x % r ≠ ↑x_1 % r} = ∑ x, #{x_1 | ↑x % r ≠ ↑x_1 % r} + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
card_filter

Goal state after:
n r : ℕ
⊢ (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
h✝ : ∀ (v : α), ∃ w, ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ ⊤ ≤ G.eccent u

Tactic:
← edist_eq_top_of_not_reachable h

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
h✝ : ∀ (v : α), ∃ w, ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.edist u v ≤ G.eccent u
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2
α : 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
i₁ i₂ : Fin r
h :
  (fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ) i₁ =
    (fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ) i₂
⊢ i₁ = i₂

Tactic:
simp_rw [Finset.ext_iff] at h

Goal state after:
case neg.refine_2
α : 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
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    a ∈ map { toFun := fun j ↦ f (i₁, j), inj' := ⋯ } univ ↔ a ∈ map { toFun := fun j ↦ f (i₂, j), inj' := ⋯ } univ
⊢ i₁ = i₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n / 2 * (↑(#G.edgeFinset) * (↑n - 1)) ≤ (↑n + 1) * ↑n / 2 * ↑(extremalNumber n H)

Tactic:
← mul_div (n + 1 : ℝ),

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑n / 2 * (↑(#G.edgeFinset) * (↑n - 1)) ≤ (↑n + 1) * (↑n / 2) * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs✝ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs' : s ∈ powersetCard t p
w : Fin n
hw : w ∈ s
⊢ G.Adj v w

Tactic:
obtain ⟨_, hadj, _⟩ := by
      rw [mem_powersetCard] at hs
      apply hs.1 at hw
      rwa [mem_filter, between_adj] at hw

Goal state after:
case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs✝ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs' : s ∈ powersetCard t p
w : Fin n
hw : w ∈ s
left✝ : w ∈ id p
hadj : G.Adj w v
right✝ : w ∈ ↑K.verts ∧ v ∈ (↑K.verts)ᶜ ∨ w ∈ (↑K.verts)ᶜ ∧ v ∈ ↑K.verts
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
⊢ ⟨s(v, w), ha⟩ = h.toEdge ⟨w, ⋯⟩

Tactic:
h.toEdge_eq_of_adj ha.symm,

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
⊢ ⟨s(v, w), ha⟩ = ⟨s(w, v), ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Hall

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

Tactic:
have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]

Goal state after:
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₂
⊢ ∃ h, Bijective h ∧ ∀ (a : ↑p₁), G.Adj ↑a ↑(h a)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

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

Tactic:
← Nat.pos_iff_ne_zero

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

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

Tactic:
simp_rw [← union_compl X, sum_union disjoint_compl_right (s₁ := X), neighborFinset_eq_filter,
             filter_inter, univ_inter, card_eq_sum_ones X, card_eq_sum_ones Xᶜ, sum_mul, one_mul]

Goal state after:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ x ∈ X, #({w ∈ W | G.Adj x w}) + ∑ x ∈ Xᶜ, #({w ∈ W | G.Adj x w}) ≤ ∑ x ∈ X, (#W - i) + ∑ x ∈ Xᶜ, (#W - j)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
b_mem : b ∈ p.support
⊢ G.Reachable a b

Tactic:
exact ((p.takeUntil a a_mem).reverse.append <| p.takeUntil b b_mem).reachable

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type v
C : G.Coloring α
c : V
⊢ IsAntichain G.Adj {x | (Setoid.ker ⇑C) x c}

Tactic:
apply C.isIndepSet_colorClass

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

Goal state before:
pp: case refine_2
ε : ℝ
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'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
⊢ #(Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ) = r ∨ t = 0

Tactic:
simp_rw [card_map, card_univ, card_coe]
        exact .inl (K.card_parts.resolve_right ht'_pos.ne')

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : ↑(⊤.deleteVerts u).coe.oddComponents → V
hf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), f c ∈ u
g : ↑(⊤.deleteVerts u).coe.oddComponents → ↑(⊤.deleteVerts u).verts
hgf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), M.Adj (↑(g c)) (f c)
hg : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), g c ∈ (↑c).supp
⊢ ¬G.IsTutteViolator u

Tactic:
have hfinj : f.Injective := fun c d hcd ↦ by
    replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
    exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : ↑(⊤.deleteVerts u).coe.oddComponents → V
hf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), f c ∈ u
g : ↑(⊤.deleteVerts u).coe.oddComponents → ↑(⊤.deleteVerts u).verts
hgf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), M.Adj (↑(g c)) (f c)
hg : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), g c ∈ (↑c).supp
hfinj : Function.Injective f
⊢ ¬G.IsTutteViolator u
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ (i1, μ.rowLen i1) ∈ μ

Tactic:
exact μ.up_left_mem hi (by rfl) h_lt

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

Goal state before:
pp: μ : YoungDiagram
⊢ ofRowLens μ.rowLens ⋯ = μ

Tactic:
by
  ext ⟨i, j⟩
  simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]
  simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt

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 : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
⊢ f = g

Tactic:
by funext a b; apply H

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr.inl
p : ℕ →. Bool
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
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
⊢ (p n).Dom

Tactic:
exact h₁.fst

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
⊢ let 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, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a

Tactic:
intro F

Goal state after:
α : 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, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
⊢ (List.Vector.ofFn fun i ↦ f a i).get = f a

Tactic:
by funext i; simp

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
| n + 4

Tactic:
rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]

Goal state after:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
| bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).1) n < n + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).1) n ≤ n
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).2) n < n + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n ↦ (unpair n).2) n ≤ n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ Tendsto (r i) atTop atTop

Tactic:
rw [tendsto_atTop]
  intro b
  have := R.eventually_r_ge b
  rw [Filter.eventually_all] at this
  exact_mod_cast this i

Goal state after: