mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.degree (⋯.unit⁻¹ • f) = m.degree f

Tactic:
apply degree_smul_of_isRegular (Units.isRegular _)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finitary
⊢ (M ／ C).Finitary

Tactic:
by
  obtain ⟨J, hJ⟩ := M.exists_isBasis' C
  suffices (M ／ J).Finitary by
    rw [hJ.contract_eq_contract_delete]
    infer_instance
  exact ⟨fun I hI ↦ hJ.indep.contract_indep_iff.2  ⟨disjoint_left.2 fun e heI ↦
    ((hI {e} (by simpa) (by simp)).subset_ground rfl).2,
    indep_of_forall_finite_subset_indep _ fun K hK hKfin ↦
      (hJ.indep.contract_indep_iff.1 <| hI (K ∩ I)
      inter_subset_right (hKfin.inter_of_left _)).2.subset (by tauto_set)⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
⊢ P = 0

Tactic:
set Q := optionEquivLeft R σ P with hQ

Goal state after:
case h_option
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
⊢ P = 0
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
hc : i = j
⊢ m.toSyn (m.degree (b j * (monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))) ≤
    m.toSyn (m.degree f)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
hc : ¬i = j
⊢ m.toSyn (m.degree (b j * 0)) ≤ m.toSyn (m.degree f)

Tactic:
· subst j
          grw [degree_mul_le, map_add, degree_monomial_le, ← map_add, add_tsub_cancel_of_le hf]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
j : ι
hc : ¬i = j
⊢ m.toSyn (m.degree (b j * 0)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b c : V
p : Path a b
e : b ⟶ c
x : V
⊢ x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c

Tactic:
simp only [vertices_cons]

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b c : V
p : Path a b
e : b ⟶ c
x : V
⊢ x ∈ p.vertices.concat c ↔ x ∈ p.vertices ∨ x = c
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₁ p₂, p = p₁.comp p₂

Tactic:
obtain ⟨v, p₁, p₂, hp, hv, rfl⟩ := p.exists_eq_comp_and_length_eq_of_lt_length n hn

Goal state after:
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₂
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: case mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t

pp: case mpr
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2

Tactic:
· rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
    exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ↑(#({a ∈ Ioc 0 1 | a ∈ A})) ≤ 1

Tactic:
Nat.cast_le_one

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ #({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a

Tactic:
by
  simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le]
  simp_rw [← image_sup_product]
  rw [inf'_image]
  simp [Function.uncurry_def]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r + 1) ↑(∂⁺ 𝒜)

Tactic:
by
  intro A h
  obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h
  rw [card_insert_of_notMem hi, h𝒜 hA]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case refine_2
α : 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
hus : u ⊆ s
⊢ insert x ((s ∪ v) \ u) ∈ 𝒜

Tactic:
← insert_sdiff_of_notMem _ ‹x ∉ u›,

Goal state after:
case refine_2
α : 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
hus : u ⊆ s
⊢ insert x (s ∪ v) \ u ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rw [inter_comm, mul_comm #𝒜]
  exact hℬ.card_inter_le_finset h𝒜

Goal state after:
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₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

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

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k → s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s

Tactic:
rintro ⟨⟨t, ht, hst⟩, hs⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}

Tactic:
intro hx _s' hs' hx'
    rwa [eq_of_mem_eqv_class H hs' hx' hs hx]

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

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

Tactic:
exact chromaticNumber_mono_of_hom G.selfColoring

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk u x
⊢ False

Tactic:
obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk u x
hx₂ : G.Adj x p.penultimate
hy₂ : ¬p.penultimate = y
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk v x
⊢ False

Tactic:
obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
p : (G.deleteEdges {s(y, x)}).Walk v x
hx₂ : G.Adj x p.penultimate
hy₂ : ¬p.penultimate = y
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ : V
hl : x✝¹ ∈ ↑(map { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } univ)
x✝ : V
hr : x✝ ∈ ↑(map { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } univ)
⊢ G.Adj x✝¹ x✝

Tactic:
rw [mem_coe, mem_map] at hl hr

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ : V
hl : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } a = x✝¹
x✝ : V
hr : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } a = x✝
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
| inr huv =>

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

Goal state before:
pp: V : Type u_1
u v : V
h : u ≠ v
⊢ ⊥.edist u v = ⊤

Tactic:
ne_eq,

Goal state after:
V : Type u_1
u v : V
h : ¬u = v
⊢ ⊥.edist u v = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b₁ b₂ x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w

Tactic:
rw [Walk.boxProdRight, map_cons, ofBoxProdRight, Or.by_cases, dif_pos, ←
      Walk.boxProdRight]
    · simp [ofBoxProdRight_boxProdRight]
    · exact ⟨h, rfl⟩

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

Goal state before:
pp: case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ (s ∪ t) = s ∪ t

Tactic:
simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]

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

Goal state before:
pp: n✝ n : ℕ
u v : Fin (n + 2)
h : ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
⊢ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
cases h with
    | inl h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

| inr h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

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

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

Tactic:
grind +locals [getVert_cons_succ]

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

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

Tactic:
grind +locals [getVert_cons_succ]

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

Goal state before:
pp: case refine_1.inr.inl.refine_1
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
⊢ #left.toRight = #left

Tactic:
exact card_bij (fun i _ ↦ .inr i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getRight <| (hmem_left hi).right Sum.isRight_inr, by simp [hi]⟩)

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

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

Tactic:
adjMatrix_dotProduct

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ ∑ u ∈ G.neighborFinset v, vec u = ∑ u ∈ G.neighborFinset v, vec u
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
d : ℕ
a : α
hd : G.IsRegularOfDegree d
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = ↑d * a

Tactic:
simp [hd v]

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

Goal state before:
pp: case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
| inr huv =>

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

Goal state before:
pp: n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
cases hadj with
      | inl huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

| inr huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.Connected
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Tactic:
obtain hV | hV := (finite_or_infinite V).symm

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Infinite V
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬↑u % 2 = ↑v % 2

Tactic:
| inr huv =>

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ⟦a⟧ ≠ ⟦b⟧ ↔ G.Adj a b

Tactic:
ne_eq,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ¬⟦a⟧ = ⟦b⟧ ↔ G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
⊢ G.Adj
      (match a✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match b✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    a✝ ≠ b✝ ∧ ¬(pathGraph 3).Adj a✝ b✝

Tactic:
ne_eq,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
⊢ G.Adj
      (match a✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match b✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a✝ = b✝ ∧ ¬(pathGraph 3).Adj a✝ b✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ Fin (r * t) → Fin r × Fin t

Tactic:
by
    refine fun v ↦ (⟨v % r, ?_⟩, ⟨v / r, ?_⟩)
    · have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
      exact Nat.mod_lt v hr
    · exact Nat.div_lt_of_lt_mul v.prop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ x, s ∩ c.supp = {x}

Tactic:
obtain ⟨a, ha⟩ := existsUnique_rep hrep h

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : (fun x ↦ x ∈ s ∩ c.supp) a ∧ ∀ (y : V), (fun x ↦ x ∈ s ∩ c.supp) y → y = a
⊢ ∃ x, s ∩ c.supp = {x}
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ #(turanGraph (n + r) r).edgeFinset = #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2

Tactic:
← mul_right_inj' two_ne_zero

Goal state after:
n r : ℕ
⊢ 2 * #(turanGraph (n + r) r).edgeFinset = 2 * (#(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

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

Tactic:
constructor
  · intro h v huv
    have hd : G.edist u v ≤ 1 := edist_le_eccent.trans h
    have hd' : 1 ≤ G.edist u v := Order.one_le_iff_pos.mpr (G.edist_pos_of_ne huv)
    exact edist_eq_one_iff_adj.mp (le_antisymm (hd') hd).symm
  · intro hall
    rw [eccent_le_iff]
    intro v
    rw [edist_le_one_iff_adj_or_eq]
    exact or_iff_not_imp_right.mpr (hall v)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ ∃ u v, G.dist u v = G.diam

Tactic:
by_cases h : G.diam = 0
  · simp [h]
  · obtain ⟨u, v, huv⟩ := exists_edist_eq_ediam_of_ne_top <| ediam_ne_top_of_diam_ne_zero h
    use u, v
    rw [diam, dist, congrArg ENat.toNat huv]

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

Goal state before:
pp: n r : ℕ
| r

Tactic:
← card_range r

Goal state after:
n r : ℕ
| #(range r)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.ediam = ⊤ ↔ G.radius = ⊤

Tactic:
refine ⟨?_, fun hr ↦ eq_top_iff.mpr (hr ▸ radius_le_ediam)⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.ediam = ⊤ → G.radius = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Adj ⟨v, vK⟩ ⟨w, wK⟩

Tactic:
exact a

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ ↑C
p : G.Walk v u
⊢ False

Tactic:
obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ :=
    p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ ↑C
p : G.Walk v u
x y : V
xy : G.Adj (x, y).1 (x, y).2
xC : { fst := x, snd := y, adj := xy }.toProd.1 ∈ ↑C
ynC : { fst := x, snd := y, adj := xy }.toProd.2 ∉ ↑C
⊢ False