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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < G.chromaticNumber

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]
  apply le_csInf (colorable_set_nonempty_of_colorable hc)
  intro m hm
  by_contra h'
  simp only [not_le] at h'
  obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)
  have h₁ : i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')
  exact Nat.not_lt_zero _ h₁

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

Goal state before:
pp: 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

Tactic:
have hyP := P.snd_mem_support_of_mem_edges heP

Goal state after:
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
hyP : y ∈ P.support
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber

Tactic:
obtain ⟨_, _, h⟩ := ne_bot_iff_exists_adj.mp h

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
h✝ : G ≠ ⊥
w✝¹ w✝ : V
h : G.Adj w✝¹ w✝
⊢ 2 ≤ G.chromaticNumber
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset

Tactic:
← Nat.mul_left_cancel_iff zero_lt_two,

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
⊢ 2 * ∑ v ∈ s, G.degree v = 2 * #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset

Tactic:
classical
  rw [← Nat.mul_left_cancel_iff zero_lt_two, ← isBipartiteWith_sum_degrees_eq_twice_card_edges h,
    sum_union (disjoint_coe.mp h.disjoint), two_mul, add_right_inj]
  exact isBipartiteWith_sum_degrees_eq h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → (completeGraph (Fin 2)).Adj (c a) (c b)
⊢ ∀ ⦃v w : V⦄, G.Adj v w → v ∈ {v | c v = 0} ∧ w ∈ {v | c v = 1} ∨ v ∈ {v | c v = 1} ∧ w ∈ {v | c v = 0}

Tactic:
rintro v w hvw

Goal state after:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → (completeGraph (Fin 2)).Adj (c a) (c b)
v w : V
hvw : G.Adj v w
⊢ v ∈ {v | c v = 0} ∧ w ∈ {v | c v = 1} ∨ v ∈ {v | c v = 1} ∧ w ∈ {v | c v = 0}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w).Finite

Tactic:
refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ {u✝, v✝}.Finite
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #G.bipartiteDoubleCover.edgeFinset = 2 * #G.edgeFinset

Tactic:
two_mul_card_edgeFinset,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #G.bipartiteDoubleCover.edgeFinset =
    #{x |
        match x with
        | (x, y) => G.Adj x y}
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : Fintype α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
⊢ (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a

Tactic:
simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
· apply hpc.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hr2
    aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
⊢ cycleGraph n ⊑ G ↔ ∃ v p, p.IsCycle ∧ p.length = n

Tactic:
by
  refine ⟨fun ⟨h⟩ ↦ ?_, fun h' ↦ ?_⟩
  · have : n = n - 3 + 3 := by lia
    rw [this] at h
    refine ⟨h.toHom ⟨0, by lia⟩, Walk.map h.toHom <| cycleGraph.cycle (n - 3), ?_, ?_⟩
    · exact (isCycle_map_iff_of_injective h.injective).mpr cycleGraph.isCycle_cycle
    · simp [cycleGraph.length_cycle, ← this]
  · obtain ⟨a, p, hp₁, hp₂⟩ := h'
    refine ⟨⟨⟨fun n ↦ p.support[n.succ]'(?_), ?_⟩, ?_⟩⟩
    · grind [hp₁.three_le_length, length_tail_add_one, not_nil_iff_lt_length]
    · intro ⟨x, hx⟩ ⟨y, hy⟩ hab
      have hne : x ≠ y := fun _ ↦ by simp_all
      wlog hle : x > y
      · exact this hn a p hp₁ hp₂ y hy x hx hab.symm hne.symm (by lia) |>.symm
      rcases cycleGraph_adj'.mp hab with hab | hab
      · simp_rw [show x = y + 1 by grind [Fin.sub_val_of_le]]
        exact p.isChain_adj_support.getElem _ _ |>.symm
      · rw [Fin.coe_sub_iff_lt.mpr hle] at hab
        simp_rw [show x = n - 1 by lia, show y = 0 by lia, Fin.succ_mk, show n - 1 + 1 = n by lia]
        simp [← hp₂, p.adj_snd hp₁.not_nil]
    · have hlen : p.tail.support.length = n := by
        grind [length_tail_add_one, not_nil_iff_lt_length]
      have (m : Fin n) : p.support[m.succ]'(by grind) = p.tail.support[m] := by
        simp [p.support_tail_of_not_nil hp₁.not_nil]
      simp_rw [this]
      have := IsPath.mk' <| (support_tail_of_not_nil _ hp₁.not_nil) ▸ hp₁.support_nodup
      exact hlen ▸ (isPath_iff_injective_get_support _ |>.mp this)

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

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
f : W → V
hf : Function.Surjective f
⊢ (A.submatrix f f).IsAdjMatrix ↔ A.IsAdjMatrix

Tactic:
refine ⟨fun h ↦ ?_, (·.submatrix f)⟩
  rw [← A.submatrix_id_id, ← f.comp_surjInv hf]
  apply h.submatrix

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
classical
  have : Finset.card ({default} : Finset V)ᶜ + 1 = Fintype.card V := by
    rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
  rw [← this, add_left_inj]
  choose f hf hf' using (hG.existsUnique_path · default)
  refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
  case notNil => exact not_nil_of_ne (by simpa using hw)
  case memEdges => simp
  case inj =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))
    rw [dart_edge_eq_iff] at h
    obtain (h | h) := h
    · exact (congrArg (·.fst) h)
    · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
      have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
      · rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro x y h
    wlog h' : (f x).length ≤ (f y).length generalizing x y
    · rw [Sym2.eq_swap]
      exact this y x h.symm (le_of_not_ge h')
    refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
    · rintro rfl
      rw [← hf' _ nil IsPath.nil, length_nil,
          ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
          length_cons, length_nil] at h'
      simp at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
⊢ p.length ≠ q.length

Tactic:
by_cases hw : w ∈ p.support

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∈ p.support
⊢ p.length ≠ q.length

case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
⊢ p.length ≠ q.length
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ G.IsAcyclic

Tactic:
isAcyclic_iff_forall_isBridge

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
h : Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
cases nonempty_fintype V
  rw [Nat.card_eq_fintype_card]
  simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
    ← Set.toFinset_card, Set.toFinset_iUnion ConnectedComponent.supp]
  rw [Finset.card_biUnion
    (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]
  simp_rw [← Set.ncard_eq_toFinset_card', ← Finset.coe_filter_univ, Set.ncard_coe_finset]
  exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm

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

Goal state before:
pp: case pos
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht

Goal state after:
case pos
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ ⊥.Copy G
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : v ≠ u
⊢ G.eccent u ≠ 0

Tactic:
contrapose huv

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : G.eccent u = 0
⊢ v = u
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : u ≠ v
⊢ G.ediam ≠ 0

Tactic:
contrapose huv

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : G.ediam = 0
⊢ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist v w ≤ 2 * G.eccent u

Tactic:
calc
    G.edist v w
      ≤ G.edist v u + G.edist u w := G.edist_triangle
    _ = G.edist u v + G.edist u w := by rw [edist_comm]
    _ ≤ G.eccent u + G.eccent u := add_le_add edist_le_eccent edist_le_eccent
    _ = 2 * G.eccent u := (two_mul _).symm

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
⊢ ∃ u v, G.edist u v = G.radius

Tactic:
obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
  obtain ⟨v, hv⟩ := G.exists_edist_eq_eccent_of_finite w
  use w, v
  rw [hv, hw]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ 1 ≤ G.radius

Tactic:
apply le_iInf

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ ∀ (i : α), 1 ≤ G.eccent i
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
← Nat.sub_add_comm

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

n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)
Module: Mathlib.Data.Set.Card.Arithmetic

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

Tactic:
Nat.cast_finsum_mem ht

Goal state after:
case pos
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : (⋃ i ∈ t, s i).Finite
⊢ ∑ᶠ (x : ι) (_ : x ∈ t), ↑(s x).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), ↑(s i).ncard
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
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
⊢ ∃ M, M.IsPerfectMatching

Tactic:
use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂

Goal state after:
case h
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
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
⊢ (hall_subgraph (fun v ↦ ↑(b v)) ⋯ hb₂).IsPerfectMatching
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ #p.support.toFinset = Fintype.card α

Tactic:
hp.toFinset_support,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ #univ = Fintype.card α
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + Fintype.card ↑(G.commonNeighbors v w) = 2 * k

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k

Tactic:
← Set.toFinset_card

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) + #(G.commonNeighbors v w).toFinset = 2 * k

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k
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.neighborSet v ∩ G.neighborSet w).toFinset = Fintype.card ↑(G.commonNeighbors v w)

Tactic:
← 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.StronglyRegular

Goal state before:
pp: case convert_4
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 ∧ w ≠ v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = Fintype.card ↑(G.commonNeighbors v w)

Tactic:
← Set.toFinset_card

Goal state after:
case convert_4
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 ∧ w ≠ v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case inl
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
⊢ ↑(Fintype.card ↑(G.commonNeighbors v v)) =
    (k • 1 v v + ℓ • if G.Adj v v then 1 else 0) + μ • if v ≠ v ∧ ¬G.Adj v v then 1 else 0

Tactic:
← Set.toFinset_card

Goal state after:
case inl
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
⊢ ↑(#(G.commonNeighbors v v).toFinset) =
    (k • 1 v v + ℓ • if G.Adj v v then 1 else 0) + μ • if v ≠ v ∧ ¬G.Adj v v then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2

Tactic:
← Set.toFinset_card

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ {v | Odd (G.degree v)}.toFinset.card = 0 ∨ {v | Odd (G.degree v)}.toFinset.card = 2
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ Nat.card V - 1 + 1 ≤ Nat.card V

Tactic:
exact Nat.add_le_of_le_sub (Order.one_le_iff_pos.mpr Nat.card_pos) (le_refl _)

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
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
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
have induce_le : ((cycles.connectedComponentMk c).toSimpleGraph).spanningCoe ≤
      (G ⊔ edge a c) ⊔ edge x b := by
    refine le_trans (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp) ?_
    simp only [← hsupG, cycles]
    exact le_trans (by apply symmDiff_le_sup) (sup_le_sup hM1sub hM2sub)

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

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

Tactic:
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 : α → β → σ
⊢ (Primrec₂ fun a n ↦ (decode n).bind (some ∘ f a)) ↔ Primrec₂ f

Tactic:
exact bind_decode_iff.trans Primrec₂.option_some_iff

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

Goal state before:
pp: case zero
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) 0 = List.range 0

Tactic:
simp [*, List.range_succ]

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

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : Nat.rec [] (fun n IH ↦ IH ++ [n]) n✝ = List.range n✝
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) (n✝ + 1) = List.range (n✝ + 1)

Tactic:
simp [*, List.range_succ]

Goal state after: