mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hn : n < p.vertices.length
hv✝ : p.vertices[n] ∈ p.vertices
p₁ : Path a p.vertices[n]
p₂ : Path p.vertices[n] b
hp : p = p₁.comp p₂
hv : p₁.length = n
⊢ ∃ p₁ p₂, p = p₁.comp p₂

Tactic:
exact ⟨p₁, p₂, hp⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
⊢ v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
hxe_ne

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
hxe_ne : v ≠ (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s

Tactic:
rintro (h | h)

Goal state after:
case mp.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

case mp.inr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜 ∨ s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜

Tactic:
rintro (h | h)

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

case inr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: h : Set.ofPred Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity {n | n % 2 = 1} = 2⁻¹

Tactic:
schnirelmannDensity_setOfPred_mod_eq_one (by norm_num1),

Goal state after:
h : Set.ofPred Odd = {n | n % 2 = 1}
⊢ (↑2)⁻¹ = 2⁻¹
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
a b : α
⊢ (b ⊔ a \ b) \ (b \ a) = a

Tactic:
sup_sdiff_self_right,

Goal state after:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableLE α
a b : α
⊢ (b ⊔ a) \ (b \ a) = a
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)

Tactic:
by
  simp_rw [← disjSups_assoc, disjSups_right_comm]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
⊢ α ↪o Set { a // SupIrred a }

Tactic:
by_cases! h : IsEmpty α

Goal state after:
case pos
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : IsEmpty α
⊢ α ↪o Set { a // SupIrred a }

case neg
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : Nonempty α
⊢ α ↪o Set { a // SupIrred a }
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ (#(Finset.memberSubfamily a 𝒜) + #(Finset.nonMemberSubfamily a 𝒜)) *
      (#(Finset.memberSubfamily a ℬ) + #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)

Tactic:
add_mul,

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #(Finset.memberSubfamily a 𝒜) * (#(Finset.memberSubfamily a ℬ) + #(Finset.nonMemberSubfamily a ℬ)) +
      #(Finset.nonMemberSubfamily a 𝒜) * (#(Finset.memberSubfamily a ℬ) + #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
⊢ u.erase x ⊆ s

Tactic:
← subset_insert_iff

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
⊢ u ⊆ insert x s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
rw [h₀₁.antisymm, h₁₀.antisymm, add_zero] <;> positivity

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜

Tactic:
exact h hst ht

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
⊢ G.Connected

Tactic:
by
  refine connected_iff _ |>.mpr ⟨fun u w ↦ ?_, ⟨v⟩⟩
  exact (Reachable.of_isUniversal u h).symm.trans (Reachable.of_isUniversal w h)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑C.colorClasses ≤ card α

Tactic:
simp only [colorClasses]
  convert! Setoid.card_classes_ker_le C

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ G.Reachable w v

Tactic:
exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom,
    fun a ↦ a.symm.mem_subgraphVerts h hv⟩

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

Goal state before:
pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ (G.commonNeighbors u v).Nonempty

Tactic:
use w.getVert 1

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ w.getVert 1 ∈ G.commonNeighbors u v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
hc : G.Adj u v
⊢ False

Tactic:
by simp +decide [edist_eq_one_iff_adj.mpr hc] at h

Goal state after:
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]

Goal state after:
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
this : i = 0
⊢ p.snd = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case pos
α : 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:
rw [top_case] at h

Goal state after:
case pos
α : 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.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.Prod

Goal state before:
pp: α : 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.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤

Tactic:
rw [top_case] at h

Goal state after:
α : 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.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)
⊢ G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
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
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
      | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
    fun x ↦
    match x with
    | ⟨e, he⟩ =>
      Sym2.fromRelNdrec e he
        (fun x x_1 x_2 ↦
          match x, x_1, x_2 with
          | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
          | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
          | Sum.inl u, Sum.inr v, h => False.elim ⋯
          | Sum.inr u, Sum.inl v, h => False.elim ⋯)
        ⋯

Tactic:
rintro (⟨⟨u, v⟩, h⟩ | ⟨⟨u, v⟩, h⟩)

Goal state after:
case inl.mk
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
val✝ : Sym2 V
u v : V
h : Quot.mk (Sym2.Rel V) (u, v) ∈ G.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩)) =
    Sum.inl ⟨Quot.mk (Sym2.Rel V) (u, v), h⟩

case inr.mk
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
val✝ : Sym2 W
u v : W
h : Quot.mk (Sym2.Rel W) (u, v) ∈ H.edgeSet
⊢ (fun x ↦
        match x with
        | ⟨e, he⟩ =>
          Sym2.fromRelNdrec e he
            (fun x x_1 x_2 ↦
              match x, x_1, x_2 with
              | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
              | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
              | Sum.inl u, Sum.inr v, h => False.elim ⋯
              | Sum.inr u, Sum.inl v, h => False.elim ⋯)
            ⋯)
      ((fun x ↦
          match x with
          | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
          | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
        (Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩)) =
    Sum.inr ⟨Quot.mk (Sym2.Rel W) (u, v), h⟩
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

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

Tactic:
reachable_iff_reflTransGen,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case inr
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 : ↑(⟨y, hy⟩ - ⟨x, hx⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
· 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:
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ mulCayley ({1} \ {1}) = ⊥

Tactic:
Set.sdiff_self,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
⊢ mulCayley ∅ = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂

Tactic:
rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
    intro G _ h
    apply card_edgeFinset_le_extremalNumber
    contrapose h
    exact h.trans' ⟨e.toCopy⟩

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

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
    intro G _ h
    apply card_edgeFinset_le_extremalNumber
    contrapose h
    exact h.trans' ⟨e.toCopy⟩

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : AddGroup α
inst✝¹ : One α
inst✝ : DecidableEq V
⊢ adjMatrix α (completeGraph V) = of 1 - 1

Tactic:
by ext; simp [one_apply, sub_ite]

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
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ (cons h nil).IsPath

Tactic:
simp [h.ne]

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u → decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

Tactic:
rintro (h | h)

Goal state after:
case inl
n : ℕ
u v : Fin n
h : ↑u + 1 = ↑v
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

case inr
n : ℕ
u v : Fin n
h : ↑v + 1 = ↑u
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj u w

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

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

Goal state before:
pp: case right
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
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1

Tactic:
have : #large ≤ card V := by simpa using card_le_card large.subset_univ

Goal state after:
case right
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
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
this : #large ≤ Fintype.card V
⊢ #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h✝ : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
this : (G.deleteEdges {s(u, w)}).Reachable u w
⊢ ∃ w, w.IsCycle

Tactic:
obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h✝ : G.IsEdgeReachable n u v
w✝ : V
hw : G.Adj u w✝
h : G.IsEdgeReachable 2 u w✝
this : (G.deleteEdges {s(u, w✝)}).Reachable u w✝
w : V
p : G.Walk w w
hp₁ : p.IsCycle
hp₂ : s(u, w✝) ∈ p.edges
⊢ ∃ w, w.IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
⊢ Set.InjOn G.connectedComponentMk (Quot.out '' C)

Tactic:
by
    rintro x ⟨c, ⟨hc, rfl⟩⟩ y ⟨d, ⟨hd, rfl⟩⟩ hxy
    simp only [connectedComponentMk] at hxy
    aesop

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.edgeFinset = extremalNumber (Fintype.card V) ⊤ ↔
    Nonempty (G ≃g turanGraph (Fintype.card V) (Fintype.card α - 1))

Tactic:
by
  rw [← isTuranMaximal_iff_nonempty_iso_turanGraph (Nat.sub_pos_iff_lt.mpr one_lt_card),
    ← isExtremal_top_free_iff_isTuranMaximal, isExtremal_free_iff]

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

Goal state before:
pp: case e_a
n r : ℕ
⊢ (((∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
        ∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
← two_mul

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

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ u ∈ ⊤.center

Tactic:
rw [mem_center_iff, eccent_top, radius_top]

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]
      have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
      rw [Fintype.card_fin] at this; convert! this
      rw [turanGraph_eq_top]; exact .inr h.le

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

Goal state before:
pp: case inr.inr.e_a.e_a.e_a
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 : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r * (r - 1) * (n' / r) + (n' % r * (n' / r) + n' % r) * (r - 1)

Tactic:
add_mul,

Goal state after:
case inr.inr.e_a.e_a.e_a
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 : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) = r * (r - 1) * (n' / r) + (n' % r * (n' / r) * (r - 1) + n' % r * (r - 1))
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this : Fintype ↑(↑(Opposite.unop G')).verts
⊢ Fintype (↑(↑(Opposite.unop G')).verts → W)

Tactic:
classical exact Pi.instFintype

Goal state after:
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₂
x : V
⊢ f x ∈ p₁ ∨ f x ∈ p₂

Tactic:
simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]

Goal state after: