mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ ∃ s, (∀ (i : σ), s i ∈ S i) ∧ (eval s) f ≠ 0

Tactic:
by
  let _ : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
  by_contra! Heval
  apply ht
  obtain ⟨h, hh, hf⟩ := combinatorial_nullstellensatz_exists_linearCombination S
    (fun i ↦ by rw [← Finset.card_pos]; exact Nat.zero_lt_of_lt (htS i)) f Heval
  rw [hf]
  rw [linearCombination_apply, Finsupp.sum, coeff_sum]
  apply Finset.sum_eq_zero
  intro i _
  set g := h i * Alon.P (S i) i with hg
  by_cases hi : h i = 0
  · simp [hi]
  have : g.totalDegree ≤ f.totalDegree := by
    rw [hg, mul_comm]
    exact hh i
  -- one could simplify this by proving `totalDegree_mul_eq` (at least in a domain)
  rw [hg, ← degree_degLexDegree,
    degree_mul_of_isRegular_right hi (by simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]),
    Alon.degree_P, map_add, degree_degLexDegree, degree_single, ht'] at this
  rw [smul_eq_mul, coeff_mul, Finset.sum_eq_zero]
  rintro ⟨p, q⟩ hpq
  simp only [Finset.mem_antidiagonal] at hpq
  simp only [mul_eq_zero, Classical.or_iff_not_imp_right]
  rw [← ne_eq, ← mem_support_iff]
  intro hq
  obtain ⟨e, hq', hq⟩ := Alon.of_mem_P_support _ _ _ hq
  apply coeff_eq_zero_of_totalDegree_lt
  rw [← Finsupp.degree_apply]
  apply lt_of_add_lt_add_right (lt_of_le_of_lt this _)
  rw [← hpq, map_add, add_lt_add_iff_left, hq, degree_single]
  apply lt_of_le_of_lt _ (htS i)
  simp [← hpq, hq]

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

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

Tactic:
simp_rw [mem_compression, erase_idem]
  refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_
  rwa [erase_eq_of_notMem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inl
hm : 0 ≠ 1
⊢ schnirelmannDensity {n | n % 0 = 1} = (↑0)⁻¹

Tactic:
simp only [Nat.cast_zero, inv_zero]
    refine schnirelmannDensity_finite ?_
    simp

Goal state after:
Module: Mathlib.Data.Finset.Sups

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

Tactic:
simp_rw [← disjSups_assoc, disjSups_comm s]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
⊢ sᶜˢᶜˢ = s

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
⊢ univᶜˢ = univ

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupPrime a
⊢ a ≠ ⊥

Tactic:
by rintro rfl; exact not_supPrime_bot ha

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

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜

Tactic:
rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a : α
u : Finset α
hau : a ∉ u
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[#u] 𝒜 ↔ ∃ u_1, #u_1 = #u ∧ u_1 ⊆ t ∧ t \ u_1 ∈ 𝒜
hut : insert a u ⊆ t
htu : t \ insert a u ∈ 𝒜
⊢ ∃ a ∈ t, ∃ u_1, #u_1 = #u ∧ (u_1 ⊆ t ∧ a ∉ u_1) ∧ t \ insert a u_1 ∈ 𝒜
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b c : α
⊢ a \ (c \ b) ≤ a ⊓ b ⊔ a \ c

Tactic:
by rw [sdiff_sdiff_right', sup_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ x, (↑(card α) - ↑(#({s}.truncatedSup x))) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))

Tactic:
sum_congr rfl fun t _ ↦ this t,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ t, if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
have hvt : v ≤ t := huvs.2.trans (erase_subset _ t)

Goal state after:
case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case h₂
α : 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
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) ≤
    2 ^ #s * #(𝒜 ∩ ℬ)

Tactic:
refine (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
    ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq ?_

Goal state after:
case h₂
α : 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
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ 2 ^ #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      2 ^ #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    2 ^ #s * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_3
ι : 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)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α +
      #(s.biUnion f') * (2 ^ Fintype.card α + 2 ^ Fintype.card α - 2 ^ Fintype.card α) ≤
    (2 ^ Fintype.card α + 2 ^ Fintype.card α) * 2 ^ Fintype.card α -
      (2 ^ Fintype.card α + 2 ^ Fintype.card α) * 2 ^ (Fintype.card α - #(cons i s hi))

Tactic:
add_tsub_cancel_left,

Goal state after:
case inr.cons.refine_3
ι : 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)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α + #(s.biUnion f') * 2 ^ Fintype.card α ≤
    (2 ^ Fintype.card α + 2 ^ Fintype.card α) * 2 ^ Fintype.card α -
      (2 ^ Fintype.card α + 2 ^ Fintype.card α) * 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
⊢ ∂ (initSeg s) = initSeg (s.erase (s.min' hs))

Tactic:
by
  -- This is a pretty painful proof, with lots of cases.
  ext t
  simp only [mem_shadow_iff_insert_mem, mem_initSeg]
  constructor
  -- First show that if t ∪ a ≤ s, then t ≤ s - min s
  · rintro ⟨a, ha, hst, hts⟩
    constructor
    · rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]
    · simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _)
  -- Now show that if t ≤ s - min s, there is j such that t ∪ j ≤ s
  -- We choose j as the smallest thing not in t
  simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc]
  simp only [toColex_inj, and_imp]
  rintro cards' (rfl | ⟨k, hks, hkt, z⟩)
  -- If t = s - min s, then use j = min s so t ∪ j = s
  · refine ⟨min' s hs, notMem_erase _ _, ?_⟩
    rw [insert_erase (min'_mem _ _)]
    exact ⟨rfl, Or.inl rfl⟩
  set j := min' tᶜ ⟨k, mem_compl.2 hkt⟩
  -- Assume first t < s - min s, and take k as the colex witness for this
  have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›)
  have : j ∉ t := mem_compl.1 (min'_mem _ _)
  have hcard : #s = #(insert j t) := by
    rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]
  refine ⟨j, ‹_›, hcard, ?_⟩
  -- Cases on j < k or j = k
  obtain hjk | r₁ := hjk.lt_or_eq
  -- if j < k, k is our colex witness for t ∪ {j} < s
  · refine Or.inr ⟨k, mem_of_mem_erase ‹_›, fun hk ↦ hkt <| mem_of_mem_insert_of_ne hk hjk.ne',
      fun x hx ↦ ?_⟩
    simpa only [mem_insert, z hx, (hjk.trans hx).ne', mem_erase, Ne, false_or,
      and_iff_right_iff_imp] using fun _ ↦ ((min'_le _ _ <| mem_of_mem_erase hks).trans_lt hx).ne'
  -- if j = k, all of range k is in t so by sizes t ∪ {j} = s
  refine Or.inl (eq_of_subset_of_card_le (fun a ha ↦ ?_) hcard.ge).symm
  rcases lt_trichotomy k a with (lt | rfl | gt)
  · apply mem_insert_of_mem
    rw [z lt]
    refine mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha
    apply min'_le _ _ (mem_of_mem_erase ‹_›)
  · rw [r₁]; apply mem_insert_self
  · apply mem_insert_of_mem
    rw [← r₁] at gt
    by_contra
    apply (min'_le tᶜ _ _).not_gt gt
    rwa [mem_compl]

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

Goal state before:
pp: case zero
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
hk : 0 ≤ Fintype.card α
⊢ #(𝒜 # Fintype.card α) ≤ #(falling (Fintype.card α) 𝒜)

Tactic:
exact card_le_card (slice_subset_falling _ _)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
x : V
hx : x ∈ p.support
⊢ ∃ y ∈ p.support, G.Adj x y

Tactic:
by
  induction p with grind [Walk.nil_iff_support_eq, Walk.cons_tail_support, adj_comm]

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

Goal state before:
pp: case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ∈ 𝒞
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i

Tactic:
rw [mem_powersetCard] at Ah

Goal state after:
case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ G.chromaticNumber = ↑(sInf {n' | G.Colorable n'})

Tactic:
rw [ENat.natCast_sInf, chromaticNumber]
  exact ⟨_, h⟩

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

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Set.InjOn (insert a) ↑u.powerset

Tactic:
exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ notMem_mono (mem_powerset.1 hs) hu

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
⊢ G.CliqueFree n

Tactic:
have := colorable_chromaticNumber hc'

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
⊢ G.IsEdgeReachable (k + 1) u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v

Tactic:
by
  refine ⟨fun h e s hk ↦ ?_, fun h s hs ↦ ?_⟩
  · rw [deleteEdges_deleteEdges, Set.union_comm]
    apply h
    grw [Set.encard_union_le, Set.encard_singleton]
    exact ENat.add_lt_add_iff_right ENat.one_ne_top |>.mpr hk
  obtain rfl | ⟨e, he⟩ := s.eq_empty_or_nonempty
  · simpa using (h s(u, u)).reachable hk
  · rw [← Set.insert_sdiff_self_of_mem he, Set.insert_eq, ← deleteEdges_deleteEdges]
    refine h e <| ENat.add_lt_add_iff_right ENat.one_ne_top |>.mp ?_
    rwa [Set.encard_sdiff_singleton_add_one he]

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ Function.Injective fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
grind [Function.Injective]

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
apply hpc.getVert_injOn' (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hl1
    simp_all

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h✝ : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ (s.erase x).erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅

Tactic:
erase_right_comm,

Goal state after:
case h
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h✝ : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ (s.erase y).erase x | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : Group M
⊢ mulCayley Set.univ = ⊤

Tactic:
ext _ _

Goal state after:
M : Type u_1
inst✝ : Group M
x✝¹ x✝ : M
⊢ (mulCayley Set.univ).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v : V
p q : G.Path u v
⊢ p = q

Tactic:
have := p.isPath.exists_isCycle_of_ne q.isPath

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v : V
p q : G.Path u v
this : ↑p ≠ ↑q → ∃ u' v' p' q', p'.IsSubwalk ↑p ∧ q'.IsSubwalk ↑q ∧ (p'.append q'.reverse).IsCycle
⊢ p = q
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (H.Free G ∧ ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], H.Free G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
and_congr_right_iff,

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ H.Free G →
    ((∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], H.Free G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
      #G.edgeFinset = extremalNumber (Fintype.card V) H)
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

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

Goal state before:
pp: case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

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

Goal state before:
pp: case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

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

Goal state before:
pp: case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

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

Goal state before:
pp: case inr
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 t < G.degree s
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_gt hd) h
    exact this (by rwa [adj_comm] at hn) hd.ne' cf hd

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
⊢ Odd w.length

Tactic:
rw [cycleGraph.length_cycle, hn3]

Goal state after:
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
⊢ Odd n
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n✝ r : ℕ
hr : r > 0
n : ℕ
⊢ (n % r + r * (n / r) + n % r) * (n % r + r * (n / r) - n % r) * (r - 1) / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2

Tactic:
add_tsub_cancel_left,

Goal state after:
n✝ r : ℕ
hr : r > 0
n : ℕ
⊢ (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
| Fintype.card (Fin (n + 1)) * extremalNumber n H

Tactic:
← card_univ

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
| #univ * extremalNumber n H
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : Nonempty ((i : α) × Subtype Walk.IsCycle)
⊢ ∃ x, ↑(↑x.snd).length = ⨅ x, ↑(↑x.snd).length

Tactic:
exact ciInf_mem _

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑(#K.verts) * (1 - 1 / ↑r) + ↑(#K.verts) * ε - (↑(#K.verts) - (↑t' - ↑t))) - ↑(#K.verts) * (↑t' - ↑t)

Tactic:
mul_sub (#K.verts : ℝ) _ _,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * (↑(#K.verts) * 1 - ↑(#K.verts) * (1 / ↑r) + ↑(#K.verts) * ε - (↑(#K.verts) - (↑t' - ↑t))) -
    ↑(#K.verts) * (↑t' - ↑t)