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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.chromaticNumber ≤ 1

Tactic:
rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.Colorable 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mk
V : Type u
G G' : SimpleGraph V
e : Sym2 V
hG : G ≤ G'
a b : V
h : ¬(G'.deleteEdges {s(a, b)}).Reachable a b
⊢ ¬(G.deleteEdges {s(a, b)}).Reachable a b

Tactic:
hG

Goal state after:
case mk
V : Type u
G G' : SimpleGraph V
e : Sym2 V
hG : G ≤ G'
a b : V
h : ¬(G'.deleteEdges {s(a, b)}).Reachable a b
⊢ ¬(G'.deleteEdges {s(a, b)}).Reachable a b
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v = bipartiteAbove G.Adj t v

Tactic:
rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Connected

Tactic:
← subgraphOfAdj_eq_induce huv

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
⊢ ∃ C, C.toSubgraph = G'

Tactic:
have ⟨v, hv⟩ := hconn.nonempty
    suffices G' ≤ (G.connectedComponentMk v).toSubgraph from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSubgraph _) this) this⟩
    exact le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦
      ConnectedComponent.sound <| hconn.coe.preconnected ⟨u, hu⟩ ⟨v, hv⟩ |>.map G'.hom

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
have : w ∈ p.toSubgraph.neighborSet v := hadj
  rw [h.neighborSet_toSubgraph_endpoint] at this
  push _ ∈ _ at this
  obtain hl | hr := this
  · exact ⟨p, ⟨h, hl.symm, rfl⟩⟩
  · use p.reverse
    rw [penultimate, ← getVert_reverse] at hr
    exact ⟨h.reverse, hr.symm, by rw [toSubgraph_reverse _]⟩

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

Goal state before:
pp: case neg
α : 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 = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
have rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤ := by rw [top_case] at h; aesop

Goal state after:
case neg
α : 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 ≠ ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case refine_2.refine_2
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
⊢ ∀ {a_1 b : Fin n}, (cycleGraph n).Adj a_1 b → G.Adj p.support[a_1.succ] p.support[b.succ]

pp: case refine_2.refine_3
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
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ?refine_2.refine_2 }

Tactic:
· 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]

Goal state after:
case refine_2.refine_3
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
⊢ Function.Injective ⇑{ toFun := fun n_1 ↦ p.support[n_1.succ], map_rel' := ⋯ }
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
rw [extremalNumber_of_fintypeCard_eq rfl]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : DecidableEq V
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
A : Matrix V V α
⊢ A.IsAdjMatrix ↔ (∀ (i j : V), A i j = 0 ∨ A i j = 1) ∧ A.IsSymm ∧ ∀ (x : V), A x x = 0

Tactic:
grind [IsAdjMatrix]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
by
  ext
  simp [compl, h.apply, eq_comm]

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

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
⊢ ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsTree

Tactic:
obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic hH_le hH_isAcyclic
  grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

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

Tactic:
refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))

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

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ 3 ≤ (cycleGraph n).chromaticNumber

Tactic:
· have hn3 : n - 3 + 3 = n := by
      refine Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))
      intro h2
      rw [← h2] at hOdd
      exact (Nat.not_odd_iff.mpr rfl) hOdd
    let w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
    have hOdd' : Odd w.length := by
      rw [cycleGraph.length_cycle, hn3]
      exact hOdd
    rw [← hn3]
    exact Walk.three_le_chromaticNumber_of_odd_loop w hOdd'

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
⊢ ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1

Tactic:
by
  have ⟨u, v, p, hp, hmax⟩ := exists_isPath_forall_isPath_length_le_length G
  have ⟨u', v', hne⟩ := exists_pair_ne V
  have ⟨p', hp'⟩ := h.connected.exists_isPath u' v'
  have hnil : ¬p.Nil := by grind
  refine ⟨u, v, hp.nil_iff_eq.not.mp hnil, ?_, ?_⟩ <;>
    rw [degree_eq_one_iff_existsUnique_adj]
  · refine ⟨_, p.adj_snd hnil, fun w hadj ↦ ?_⟩
    apply h.isAcyclic.eq_snd_of_adj_start hp hadj
    have : ¬(p.cons hadj.symm).IsPath := by grind [length_cons]
    grind [hp.cons]
  · refine ⟨_, p.adj_penultimate hnil |>.symm, fun w hadj ↦ ?_⟩
    apply h.isAcyclic.eq_penultimate_of_adj_end hp hadj
    have : ¬(p.concat hadj).IsPath := by grind [length_concat]
    grind [hp.concat]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
inst✝ : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C

Tactic:
refine EdgeLabeling.ext_get ?_
  grind [toTopEdgeLabeling_get, TopEdgeLabeling.labelGraph_adj, Adj.ne]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
x✝ : ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
w✝² w✝¹ w✝ : α
h1 : G.Adj w✝¹ w✝
h2 : ¬G.Adj w✝² w✝¹
h3 : ¬G.Adj w✝² w✝
h : G.IsCompleteMultipartite
⊢ ¬G.Adj w✝¹ w✝²

Tactic:
by rwa [adj_comm] at h2

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
⊢ {c' | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty

Tactic:
refine Set.nonempty_of_ncard_ne_zero fun h' ↦ Nat.not_odd_zero ?_

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
h' : {c' | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.ncard = 0
⊢ Odd 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.diam = 1 ↔ G = ⊤

Tactic:
by
  rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]

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:
rw [Nat.mod_eq_of_lt h, tsub_self, zero_mul, Nat.zero_div, zero_add]

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.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ #(cons s K.parts ⋯) = r + 1 ∨ t = 0

Tactic:
rw [Finset.card_cons, K.card_parts.resolve_right ht]
        exact .inl rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph u ≤ finsubgraphOfAdj e

Tactic:
simp [singletonFinsubgraph, finsubgraphOfAdj]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph v ≤ finsubgraphOfAdj e

Tactic:
simp [singletonFinsubgraph, finsubgraphOfAdj]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Subtype.val '' ⇑f ⁻¹' range Sum.inl ∪ Subtype.val '' ⇑f ⁻¹' range Sum.inr = s

case refine_2
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Disjoint (Subtype.val '' ⇑f ⁻¹' range Sum.inl) (Subtype.val '' ⇑f ⁻¹' range Sum.inr)

case refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inl) = #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inr)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
intro B ⟨_, h⟩

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
B : SimpleGraph (Fin m ⊕ Fin n)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ #B.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ ¬G.Colorable (r + 1)

Tactic:
intro ⟨C⟩
  have h := C.surjOn_of_card_le_isClique hw.isNClique_fst_left.1 (by simp [hw.isNClique_fst_left.2])
  have := C.surjOn_of_card_le_isClique hw.isNClique_snd_right.1 (by simp [hw.isNClique_snd_right.2])
  -- Since `C` is an `r + 1`-coloring and `insert w₁ s` is an `r + 1`-clique, it contains a vertex
  -- `x` which shares its color with `v`
  obtain ⟨x, hx, hcx⟩ := h (a := C v) trivial
  -- Similarly there is a vertex `y` in `insert w₂ t` which shares its color with `v`.
  obtain ⟨y, hy, hcy⟩ := this (a := C v) trivial
  rw [coe_insert] at *
  -- However since `insert v s` and `insert v t` are cliques, we must have `x = w₁` and `y = w₂`.
  cases hx with
  | inl hx =>
    cases hy with
    | inl hy =>
    -- But this is a contradiction since `w₁` and `w₂` are adjacent.
      subst_vars; exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)
    | inr hy =>
      apply (C.valid _ hcy.symm).elim
      exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)
  | inr hx =>
    apply (C.valid _ hcx.symm).elim
    exact hw.isNClique_left.1 (by simp) (by simp [hx]) fun h ↦ hw.notMem_left (h ▸ hx)

Goal state after:
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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
⊢ ∃ a b c d,
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s

Tactic:
obtain ⟨a, ha, haj⟩ := hw.isNClique_fst_left.exists_not_adj_of_cliqueFree_succ hcf x
  obtain ⟨b, hb, hbj⟩ := hw.isNClique_snd_right.exists_not_adj_of_cliqueFree_succ hcf x
  obtain ⟨c, hc, hcj⟩ := hw.isNClique_left.exists_not_adj_of_cliqueFree_succ hcf x
  obtain ⟨d, hd, hdj⟩ := hw.isNClique_right.exists_not_adj_of_cliqueFree_succ hcf x
  exact ⟨_, _, _, _, ha, haj, hb, hbj, hc, hcj, hd, hdj, by grind⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
⊢ c.toSimpleGraph.spanningCoe.IsCycles

Tactic:
by
  intro v ⟨w, hw⟩
  rw [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph] at hw
  rw [← h ⟨w, hw.2⟩]
  congr 1
  ext w'
  simp only [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph, hw, true_and]

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:
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:
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: 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:
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.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
ht : p.IsTrail
x : V
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
induction p with
  | nil => simp
  | cons huv p ih =>
    rw [isTrail_cons] at ht
    specialize ih ht.1
    simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]
    split_ifs with h
    · rw [decide_eq_true_eq] at h
      obtain (rfl | rfl) := h
      · rw [Nat.even_add_one, ih]
        simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
        rintro rfl rfl
        exact G.loopless.irrefl _ huv
      · have := huv.ne; grind
    · grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsVertexCover cᶜ ↔ G.IsIndepSet c

Tactic:
simp [← isIndepSet_compl_iff_isVertexCover]

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ ↑(n - 1) ≤ ENat.card V - (1 + 1)

Tactic:
ENat.natCast_sub,

Goal state after:
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ ↑n - ↑1 ≤ ENat.card V - (1 + 1)
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
⊢ μ.transpose = ν.transpose ↔ μ = ν

Tactic:
transpose_eq_iff_eq_transpose

Goal state after:
μ ν : YoungDiagram
⊢ μ = ν.transpose.transpose ↔ μ = ν
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < w[n]

Tactic:
exact ⟨not_false, fun n hn => ⟨hn, hpos _ (List.getElem_mem hn)⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
⊢ Primrec fun a ↦ List.foldl (fun s b ↦ h a (s, b)) (g a) (f a)

Tactic:
by
  let := prim H
  let G (a : α) (IH : σ × List β) : σ × List β := List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
  have hG : Primrec₂ G := list_casesOn' H (snd.comp snd) snd <|
    to₂ <|
    pair (hh.comp (fst.comp fst) <| pair ((fst.comp snd).comp fst) (fst.comp snd))
      (snd.comp snd)
  let F := fun (a : α) (n : ℕ) => (G a)^[n] (g a, f a)
  have hF : Primrec fun a => (F a (encode (f a))).1 :=
    (fst.comp <|
      nat_iterate (encode_iff.2 hf) (pair hg hf) <|
      hG)
  suffices ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n) by
    refine hF.of_eq fun a => ?_
    rw [this, List.take_of_length_le (length_le_encode _)]
  introv
  dsimp only [F]
  generalize f a = l
  generalize g a = x
  induction n generalizing l x with
  | zero => rfl
  | succ n IH =>
    simp only [iterate_succ, comp_apply]
    rcases l with - | ⟨b, l⟩ <;> simp [G, IH]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case right
f : ℕ → ℕ
⊢ Nat.Partrec ↑fun n ↦ (unpair n).2

Tactic:
exact right

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n x✝ : ℕ
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) x✝ ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) x✝

Tactic:
induction n.unpair.2 with

Goal state after:
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
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)

Tactic:
by
  have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
  exact ⟨b (min_bi b) / 2, ⟨⟨by positivity, R.bi_min_div_two_lt_one⟩, R.eventually_bi_mul_le_r⟩⟩

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case ind
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
⊢ 0 < T n

Tactic:
cases lt_or_ge n R.n₀ with
    | inl hn => exact R.T_gt_zero' n hn -- n < R.n₀
    | inr hn => -- R.n₀ ≤ n
      rw [R.h_rec n hn]
      have := R.g_nonneg
      refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by simp_all)
      exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun x ↦ -(x⁻¹ * (log x ^ 2)⁻¹)) = fun x ↦ (-x * log x ^ 2)⁻¹

Tactic:
← mul_inv,

Goal state after:
⊢ (fun x ↦ -(x * log x ^ 2)⁻¹) = fun x ↦ (-x * log x ^ 2)⁻¹