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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : Finsupp.degree (degLex.degree (h i) + single i #(S i)) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0

Tactic:
map_add,

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : Finsupp.degree (degLex.degree (h i)) + Finsupp.degree (single i #(S i)) ≤ f.totalDegree
⊢ coeff t (h i • ∏ r ∈ S i, (X i - C r)) = 0
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ Bijective (φ.star u ∘ ⇑(starEquivCostar u).symm) ↔ Bijective (φ.star u)

Tactic:
EquivLike.bijective_comp

Goal state after:
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ Bijective (φ.star u) ↔ Bijective (φ.star u)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
hq✝ : q ∈ (∏ r ∈ S i, (X i - C r)).support
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ Finsupp.degree (p + q) < Finsupp.degree p + #(S i)

Tactic:
map_add,

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
hq✝ : q ∈ (∏ r ∈ S i, (X i - C r)).support
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ Finsupp.degree p + Finsupp.degree q < Finsupp.degree p + #(S i)
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ schnirelmannDensity A ≤ 1 ∧ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A

Tactic:
and_iff_right schnirelmannDensity_le_one

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
by norm_num1

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedSup a = a

Tactic:
by
  refine le_antisymm ?_ le_truncatedSup
  simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter]
  rintro b ⟨hb, hab⟩
  exact (hs.eq ha hb hab).ge

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
h : a ∈ upperClosure ↑s
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a

Tactic:
obtain ⟨b, hb, hba⟩ := h

Goal state after:
case pos
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b : α
hb : b ∈ ↑s
hba : b ≤ a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
rw [compress_idem]

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ InfIrred (Ici a)

Tactic:
refine ⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩
  have := mem_Ici_iff.2 (le_refl a)
  rw [← hst] at this
  exact this.imp (fun ha ↦ le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_left) fun ha ↦
      le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_right

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∈ 𝓒 u v s
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s

Tactic:
by
  rw [mem_compression] at ha
  obtain ha | ⟨_, b, hb, h⟩ := ha
  · exact ha.1
  unfold compress at h
  split_ifs at h
  · rw [← h, le_sdiff_right] at hva
    rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
  · rwa [← h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
⊢ {t ∈ 𝒜 | t.erase a = s} =
    if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
ext t; split_ifs <;> simp [erase_eq_iff ha] <;> aesop

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

Goal state before:
pp: case inr.cons.refine_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' i)ᶜ

Tactic:
rw [coe_compl]

Goal state after:
case inr.cons.refine_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsLowerSet (↑(f' i))ᶜ
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case hb
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
s : Finset α
hs : s ∈ 𝒜
⊢ 0 < ↑((Fintype.card α).choose #s)

Tactic:
exact mod_cast choose_pos s.card_le_univ

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (0 + 0) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [add_zero, mul_zero]
      exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent

Tactic:
ext ⟨v⟩
  rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
h : G.chromaticNumber < 2
⊢ False

Tactic:
obtain ⟨c⟩ := chromaticNumber_le_iff_colorable.mp (Order.le_of_lt_add_one h)

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
h : G.chromaticNumber < 2
c : G.Coloring (Fin 1)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: ι : Type u_4
V : ι → Type u_5
inst✝ : Fintype ι
f : (i : ι) → V i
h : (completeMultipartiteGraph V).chromaticNumber < ↑(card ι)
⊢ False

Tactic:
exact not_cliqueFree_of_le_card V f le_rfl <| cliqueFree_of_chromaticNumber_lt h

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

Goal state before:
pp: 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' := ⋯ }
⊢ (_root_.completeBipartiteGraph α β).Copy G

Tactic:
refine ⟨⟨f.toFun, fun {s₁ s₂} hadj ↦ ?_⟩, f.injective⟩

Goal state after:
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₂ : α ⊕ β
hadj : (_root_.completeBipartiteGraph α β).Adj s₁ s₂
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
⊢ G.neighborSet w ⊆ (between s sᶜ G).neighborSet w ∪ sᶜ

Tactic:
by
  intro v hadj
  rw [neighborSet, Set.mem_union, Set.mem_ofPred, between_adj]
  by_cases hv : v ∈ s
  · exact Or.inl ⟨hadj, Or.inr ⟨hw, hv⟩⟩
  · exact Or.inr hv

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂

Tactic:
rw [edgeSet_completeBipartiteGraph, ← ENat.card_prod, ← Set.encard_univ, ← Set.image_univ]

Goal state after:
W₁ : Type u_2
W₂ : Type u_3
⊢ ((fun x ↦ s(Sum.inl x.1, Sum.inr x.2)) '' Set.univ).encard = Set.univ.encard
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
simp_rw [Subgraph.IsInduced, IsChordless, IsChord, Sym2.forall, Sym2.lift_mk, G.mem_edgeSet,
    mem_verts_toSubgraph, adj_toSubgraph_iff_mem_edges]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → s(v_1, w_1) ∈ w.edges) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

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

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

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
x✝ : G.edist u v = ⊤ ∨ G.edist u v ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
cases eq_or_ne (G.edist u v) ⊤ with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.reverse.length) = G.edist v u

Tactic:
Walk.length_reverse,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.length) = G.edist v u
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 <;> grind +locals [getVert_cons_succ]

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

Goal state before:
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' := ⋯ }

Tactic:
· have hlen : p.tail.support.length = n := by
        grind [length_tail_add_one, not_nil_iff_lt_length]
      have (m : Fin n) : p.support[m.succ]'(by grind) = p.tail.support[m] := by
        simp [p.support_tail_of_not_nil hp₁.not_nil]
      simp_rw [this]
      have := IsPath.mk' <| (support_tail_of_not_nil _ hp₁.not_nil) ▸ hp₁.support_nodup
      exact hlen ▸ (isPath_iff_injective_get_support _ |>.mp this)

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

Goal state before:
pp: case zero
⊢ cycleGraph (0 + 1) = circulantGraph {1}

pp: case succ
n✝ : ℕ
⊢ cycleGraph (n✝ + 1 + 1) = circulantGraph {1}

Tactic:
· exact edgeFinset_inj.mp rfl

Goal state after:
case succ
n✝ : ℕ
⊢ cycleGraph (n✝ + 1 + 1) = circulantGraph {1}
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
⊢ (sSup Hs).IsAcyclic

Tactic:
intro u p hp
    obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir
    exact h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : ↑(G.subgraphOfAdj h).verts
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this✝ : ↑p.penultimate = ↑w ∧ ↑w = ↑p.snd ∨ ↑p.penultimate = ↑p.snd
this : u = ↑p.penultimate ∧ v = ↑w ∨ u = ↑w ∧ v = ↑p.penultimate
⊢ False

Tactic:
grind [IsCycle.snd_ne_penultimate]

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

Goal state before:
pp: n : ℕ
⊢ turanGraph n 0 = ⊤

Tactic:
simp [turanGraph, Fin.val_inj, Top.top]

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
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
this :
  ∀ {G : SimpleGraph V} [inst : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ G' inst_1, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
hd : G.degree s < G.degree t
⊢ ¬G.Adj t s

Tactic:
rwa [adj_comm] at hn

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬c u = true ↔ c v = true

Tactic:
← not_iff,

Goal state after:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬(c u = true ↔ c v = true)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : Even n
⊢ ∀ {v w : Fin n}, (cycleGraph n).Adj v w → decide (↑v % 2 = 0) ≠ decide (↑w % 2 = 0)

Tactic:
intro u v hadj

Goal state after:
n : ℕ
h : Even n
u v : Fin n
hadj : (cycleGraph n).Adj u v
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ ∀ {v w : Fin n},
    (cycleGraph n).Adj v w → (if ↑v = n - 1 then 2 else ⟨↑v % 2, ⋯⟩) ≠ if ↑w = n - 1 then 2 else ⟨↑w % 2, ⋯⟩

Tactic:
intro u v hadj

Goal state after:
n : ℕ
h : 2 ≤ n
u v : Fin n
hadj : (cycleGraph n).Adj u v
⊢ (if ↑u = n - 1 then 2 else ⟨↑u % 2, ⋯⟩) ≠ if ↑v = n - 1 then 2 else ⟨↑v % 2, ⋯⟩
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 : 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 : V
hadj : (fun w ↦ G.Adj u w) w
⊢ ¬(cons ⋯ p).IsPath

Tactic:
grind [length_cons]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
he : e ∈ G.edgeSet
⊢ K

Tactic:
revert he
    refine Sym2.hrec f (fun a b ↦ ?_) e
    apply Function.hfunext (by simp [adj_comm])
    grind

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
⊢ ∀ {a b : V},
    G.Adj a b →
      (completeGraph (Fin 2)).Adj
        (let u := verts (G.connectedComponentMk a);
        ⟨G.dist u a % 2, ⋯⟩)
        (let u := verts (G.connectedComponentMk b);
        ⟨G.dist u b % 2, ⋯⟩)

Tactic:
intro u v hadj

Goal state after:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
hadj : G.Adj u v
⊢ (completeGraph (Fin 2)).Adj
    (let u_1 := verts (G.connectedComponentMk u);
    ⟨G.dist u_1 u % 2, ⋯⟩)
    (let u := verts (G.connectedComponentMk v);
    ⟨G.dist u v % 2, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ r * t * ((r - 1) * t) = r * (r - 1) * t ^ 2

Tactic:
← mul_assoc,

Goal state after:
r t : ℕ
⊢ r * t * (r - 1) * t = r * (r - 1) * t ^ 2
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
a : V
ha : s ∩ c.supp = {a}
⊢ {a} ⊆ c.supp

Tactic:
simp [← ha]

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

Goal state before:
pp: α : Type u_1
⊢ ⊤.center = Set.univ

Tactic:
cases subsingleton_or_nontrivial α
  · exact center_eq_univ_of_subsingleton
  · rw [Set.eq_univ_iff_forall]
    intro u
    rw [mem_center_iff, eccent_top, radius_top]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
⊢ Function.Injective supp

Tactic:
refine ConnectedComponent.ind₂ ?_
  rintro ⟨v, hv⟩ ⟨w, hw⟩ h
  simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_ofPred_eq, ComponentCompl.supp] at h ⊢
  exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec

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

Goal state before:
pp: case inr.inr.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 - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2

Tactic:
rw [ring₂, ← add_assoc]

Goal state after:
case inr.inr.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 - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
← mul_assoc,

Goal state after:
n r : ℕ
⊢ r * (n % r) * (n % r - 1) ≤ (n % r) ^ 2 * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case refine_1
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
⊢ (Set.Ici 2).Nonempty

Tactic:
exact Set.nonempty_Ici

Goal state after: