mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case ind.inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
h𝒜₃ : 𝒜.Nontrivial
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
cases m

Goal state after:
case ind.inr.zero
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
hm : 0 = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < 0 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
n✝ : ℕ
hm : n✝ + 1 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < n✝ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      (toColex t = toColex (s.erase (s.min' hs)) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        (toColex (insert a t) = toColex s ∨
          ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
simp only [toColex_inj, and_imp]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t →
    (t = s.erase (s.min' hs) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
      ∃ a ∉ t,
        #s = #(insert a t) ∧
          (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ ∀ (w : V), (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w

Tactic:
w

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
⊢ (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r ↑𝒜
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)

Tactic:
obtain ⟨𝒜', h𝒜, h𝒜𝒞⟩ := exists_subset_card_eq h𝒞𝒜
  -- By `kruskal_katona_helper`, we find a fully compressed family `ℬ` of the same size as `𝒜`
  -- whose shadow is no bigger.
  obtain ⟨ℬ, hℬ𝒜, h𝒜ℬ, hℬr, hℬ⟩ := UV.kruskal_katona_helper 𝒜' (h𝒜r.mono (by gcongr))
  -- This means that `ℬ` is an initial segment of the same size as `𝒞`. Hence they are equal and
  -- we are done.
  suffices ℬ = 𝒞 by subst 𝒞; exact hℬ𝒜.trans (by gcongr)
  have hcard : #ℬ = #𝒞 := h𝒜ℬ.symm.trans h𝒜𝒞
  obtain h𝒞ℬ | hℬ𝒞 := h𝒞.total (UV.isInitSeg_of_compressed hℬr hℬ)
  · exact (eq_of_subset_of_card_le h𝒞ℬ hcard.le).symm
  · exact eq_of_subset_of_card_le hℬ𝒞 hcard.ge

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ y ∈ hs.proj ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (hs.equivQuotient.symm (Quotient.mk'' x))

Tactic:
simp only [Set.mem_preimage, hs.mem_iff_index_eq]

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x y : α
⊢ hs.proj y ∈ {Quotient.mk'' x} ↔ hs.index y = hs.equivQuotient.symm (Quotient.mk'' x)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ ¬∃ a ∈ p.edges, Sym2.map (⇑(Hom.ofLE ⋯)) a = s(v, w)

Tactic:
Hom.ofLE_apply,

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ ¬∃ a ∈ p.edges, Sym2.map (fun x ↦ x) a = s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v : V
⊢ ∀ {w : V}, G.Adj v w → 0 ≠ 0

Tactic:
w

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → 0 ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ G.chromaticNumber ≤ G'.chromaticNumber

Tactic:
by
  rw [chromaticNumber, chromaticNumber]
  simp only [Set.mem_ofPred_eq, le_iInf_iff]
  intro m hc
  have := h _ hc
  rw [← chromaticNumber_le_iff_colorable] at this
  exact this

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

Goal state before:
pp: V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
v : V ⊕ W
⊢ ∀ {w : V ⊕ W}, (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight

Tactic:
w

Goal state after:
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
v w : V ⊕ W
⊢ (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ G.neighborSet w = {v | v ∈ s ∧ G.Adj v w}

Tactic:
ext v
  rw [mem_neighborSet, adj_comm, Set.mem_ofPred_eq, iff_and_self]
  exact h.mem_of_mem_adj' hw

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

Goal state before:
pp: case inl
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl (s₁.getLeft hs₁)))
    (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₂.getRight hs₂)))

Tactic:
Sum.elim_inl,

Goal state after:
case inl
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁))
    (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₂.getRight hs₂)))
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₁.getRight hs₁)))
    (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl (s₂.getLeft hs₂)))

Tactic:
Sum.elim_inl,

Goal state after:
case inr
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₁.getRight hs₁)))
    ((Subtype.val ∘ ⇑fα) (s₂.getLeft hs₂))
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v

Tactic:
have h : 0 < G.edist u v := edist_pos_of_ne huv

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ p.snd = p.getVert (i + 1)

Tactic:
have : i = 0 := by
      apply hp.getVert_injOn (by rw [Set.mem_ofPred]; lia) (by rw [Set.mem_ofPred]; lia)
      rw [p.getVert_zero, hl1]
    simp [this]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
⊢ ¬p.tail.Nil

Tactic:
simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢
      lia

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

Goal state before:
pp: n : ℕ
v w : Fin (n + 2)
⊢ v - w = 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1

Tactic:
sub_eq_iff_eq_add',

Goal state after:
n : ℕ
v w : Fin (n + 2)
⊢ v = w + 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
v w : Fin (n + 2)
⊢ v = w + 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1

Tactic:
sub_eq_iff_eq_add',

Goal state after:
n : ℕ
v w : Fin (n + 2)
⊢ v = w + 1 ∨ w = v + 1 ↔ w = v - 1 ∨ w = v + 1
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
⊢ hasse (α × β) = hasse α □ hasse β

Tactic:
by
  ext x y
  simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
    or_or_or_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (hasse α).Reachable a b

Tactic:
by
  rw [reachable_iff_reflTransGen]
  exact
    reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax

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

Goal state before:
pp: case succ
n n✝ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝) = (↑⟨m, hm⟩ - n✝) % (n + 3)
m : ℕ
hm : m < n + 3
hi : n✝ + 1 ≤ ↑⟨m, hm⟩
⊢ ↑((cycleCons n ⟨m, hm⟩).getVert (n✝ + 1)) = (↑⟨m, hm⟩ - (n✝ + 1)) % (n + 3)

Tactic:
cases m

Goal state after:
case succ.zero
n n✝ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝) = (↑⟨m, hm⟩ - n✝) % (n + 3)
hm : 0 < n + 3
hi : n✝ + 1 ≤ ↑⟨0, hm⟩
⊢ ↑((cycleCons n ⟨0, hm⟩).getVert (n✝ + 1)) = (↑⟨0, hm⟩ - (n✝ + 1)) % (n + 3)

case succ.succ
n n✝¹ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝¹ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝¹) = (↑⟨m, hm⟩ - n✝¹) % (n + 3)
n✝ : ℕ
hm : n✝ + 1 < n + 3
hi : n✝¹ + 1 ≤ ↑⟨n✝ + 1, hm⟩
⊢ ↑((cycleCons n ⟨n✝ + 1, hm⟩).getVert (n✝¹ + 1)) = (↑⟨n✝ + 1, hm⟩ - (n✝¹ + 1)) % (n + 3)
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n m : ℕ
hm : m ≤ n + 3
⊢ (cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩

Tactic:
cases m

Goal state after:
case zero
n : ℕ
hm : 0 ≤ n + 3
⊢ (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), ⋯⟩

case succ
n n✝ : ℕ
hm : n✝ + 1 ≤ n + 3
⊢ (cycle n).getVert (n✝ + 1) = ⟨(n + 3 - (n✝ + 1)) % (n + 3), ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n m : ℕ
hm : m ≤ n + 3
⊢ (cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩

Tactic:
by
  cases m
  · simp
  · grind +locals [getVert_cons_succ, cycleGraph.getVert_cycleCons]

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

Goal state before:
pp: case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
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
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
simp_rw [show x = y + 1 by grind [Fin.sub_val_of_le]]
        exact p.isChain_adj_support.getElem _ _ |>.symm

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

Goal state before:
pp: case mp
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v : V
⊢ ∀ (w : V), ∃! p, p.IsPath

Tactic:
w

Goal state after:
case mp
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v w : V
⊢ ∃! p, p.IsPath
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
v : V
⊢ ∀ (v_1 : V), G.Reachable v v_1

Tactic:
w

Goal state after:
case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
⊢ G.Reachable v w
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case cons
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
⊢ u' ∉ tail.support

Tactic:
rcases tail.length.eq_zero_or_pos with h' | h'

Goal state after:
case cons.inl
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length = 0
⊢ u' ∉ tail.support

case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
⊢ u' ∉ tail.support
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✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
⊢ ⋯.toGraph = h.toGraphᶜ

Tactic:
ext v w
  rcases h.zero_or_one v w with h | h <;> by_cases hvw : v = w <;> simp [Matrix.compl, h, hvw]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V

Tactic:
have := Fintype.ofFinite V
  classical
  refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  simp_rw [isAcyclic_iff_forall_adj_isBridge]
  refine fun x y h ↦ by_contra fun hbr ↦
    (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
  rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]
  exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]

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

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
⊢ ∀ (w : G.Walk u✝ u✝), ¬Odd w.length

Tactic:
w

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
w : G.Walk u✝ u✝
⊢ ¬Odd w.length
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case map_rel'
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ Odd (((Nonempty.some ⋯).concat hab).length + (Nonempty.some ⋯).reverse.length)

Tactic:
length_concat,

Goal state after:
case map_rel'
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ Odd ((Nonempty.some ⋯).length + 1 + (Nonempty.some ⋯).reverse.length)
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 < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, ¬(G.IsClique ↑x ∧ #x = r)

Tactic:
and_comm,

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
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, ¬(#x = r ∧ G.IsClique ↑x)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
⊢ (Fintype.card (Fin r) - #{v.1}) * #univ = (r - 1) * t

Tactic:
card_singleton,

Goal state after:
r t : ℕ
v : Fin r × Fin t
⊢ (Fintype.card (Fin r) - 1) * #univ = (r - 1) * t
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case injective'
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
hF : ∀ {c₁ c₂ : Fin n} {v₁ : ↑(C.colorClass c₁)} {v₂ : ↑(C.colorClass c₂)}, c₁ = c₂ → (F c₁) v₁ = (F c₂) v₂ → ↑v₁ = ↑v₂
v : α
⊢ ∀ ⦃a₂ : α⦄,
    { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } v =
        { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } a₂ →
      v = a₂

Tactic:
w

Goal state after:
case injective'
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
hF : ∀ {c₁ c₂ : Fin n} {v₁ : ↑(C.colorClass c₁)} {v₂ : ↑(C.colorClass c₂)}, c₁ = c₂ → (F c₁) v₁ = (F c₂) v₂ → ↑v₁ = ↑v₂
v w : α
⊢ { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } v =
      { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } w →
    v = w
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts = r ∨ t = 0

Tactic:
exact K.card_parts

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

Goal state before:
pp: case neg
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
let fₜ (p : K.parts) : Fin t ↪ p :=
      Classical.arbitrary (Fin t ↪ p)

Goal state after:
case neg
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
⊢ (completeEquipartiteGraph r t).Copy G
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
by
  have h : 1 ≤ G.eccent u := Order.one_le_iff_ne_zero.mpr (eccent_ne_zero u)
  rw [← h.ge_iff_eq']
  exact eccent_le_one_iff u

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.radius = 1

Tactic:
by
  simp [radius]

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

Goal state before:
pp: case neg.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
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)

Tactic:
refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩

Goal state after:
case neg.refine_2.refine_1
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
⊢ s ∉ K.parts

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 ?neg.refine_2.refine_1✝) = r + 1 ∨ t = 0

case neg.refine_2.refine_3
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
⊢ ∀ {p : Finset V}, p ∈ cons s K.parts ?neg.refine_2.refine_1✝ → #p = t

case neg.refine_2.refine_4
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 ?neg.refine_2.refine_1✝)).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
⊢ False

Tactic:
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
⊢ False