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

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

Tactic:
exact Or.inl ⟨by rwa [insert_erase ha], notMem_erase _ _⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp
  exact (le_div_iff₀ (by positivity)).1 (schnirelmannDensity_le_div hn)

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
⊢ {b}.truncatedSup a = if a ≤ b then b else ⊤

Tactic:
by
  simp [truncatedSup]; split_ifs <;> simp [Finset.filter_true_of_mem, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : a \ v ⊔ v = ((b ⊔ u) \ u) \ v ⊔ v
⊢ a = b

Tactic:
hb.1.symm.sup_sdiff_cancel_right,

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
h : a \ v ⊔ v = b \ v ⊔ v
⊢ a = b
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v : α
⊢ Set.InjOn (fun x ↦ (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}

Tactic:
rintro a ha b hb hab
  have h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v := by
    dsimp at hab
    rw [hab]
  rwa [sdiff_sdiff_comm, ha.1.symm.sup_sdiff_cancel_right, sdiff_sdiff_comm,
    hb.1.symm.sup_sdiff_cancel_right, sdiff_sup_cancel ha.2, sdiff_sup_cancel hb.2] at h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s \\ tᶜˢ = s ⊼ t

Tactic:
← infs_compls_eq_diffs,

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊼ tᶜˢᶜˢ = s ⊼ t
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [exists₂_congr]

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

Tactic:
simpa [eq_comm] using h𝒜₂

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

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

pp: case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ

Tactic:
· grw [inter_subset_right]

Goal state after:
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
rw [← hU'] at same_size

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case a
α : 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 ∈ 𝒜
⊢ (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
exact choose_le_middle _ _

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

Goal state before:
pp: case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable = ∅
U V : Finset (Fin n)
hUV : UsefulCompression U V
⊢ IsCompressed U V 𝒜

Tactic:
rw [eq_empty_iff_forall_notMem] at husable

Goal state after:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : UsefulCompression U V
⊢ IsCompressed U V 𝒜
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
q_b : Quotient r
a : α
h_eq : Quot.lift f f_respects_relation ⟦a⟧ = Quot.lift f f_respects_relation q_b
⊢ ⟦a⟧ = q_b

Tactic:
induction q_b using Quotient.ind with | _ b

Goal state after:
case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : Quot.lift f f_respects_relation ⟦a⟧ = Quot.lift f f_respects_relation ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Preconnected ↔ G.Reachable = ⊤

Tactic:
aesop (add simp Preconnected)

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

Goal state before:
pp: case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ v ∈ (G.connectedComponentMk v).supp

Tactic:
simp only [mem_supp_iff]

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (∃ p, s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'

Tactic:
· rintro ⟨p, h⟩
    refine ⟨p.transfer _ fun e ep => ?_⟩
    rw [edgeSet_deleteEdges]
    exact ⟨p.edges_subset_edgeSet ep, fun h' => h (h' ▸ ep)⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
h : G.chromaticNumber ≠ ⊤
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at h
  obtain ⟨n, hn⟩ := h
  exact colorable_chromaticNumber hn

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
obtain hxy | hxy := em' <| G.Adj x y

Goal state after:
case inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

case inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected
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
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

Tactic:
rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
    · exact sum_congr rfl fun s hs ↦ collapse_eq (notMem_mono (mem_powerset.1 hs) hu) _ _
    · 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
α : Type u_2
inst✝ : Fintype α
s : Finset V
h : G.IsClique ↑s
hc : card α ≤ s.card
C : G.Coloring α
⊢ Set.SurjOn (⇑C) (↑s) Set.univ

Tactic:
intro _ _
  obtain ⟨_, hx⟩ := card_le_chromaticNumber_iff_forall_surjective.mp
                    (by simp_all [← induce_eq_top]) (C.comp (Embedding.induce s).toHom) _
  exact ⟨_, Subtype.coe_prop _, hx⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.takeUntil u h).toSubgraph ⊔ (c.dropUntil u h).toSubgraph = c.toSubgraph

Tactic:
← toSubgraph_append,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ ((c.takeUntil u h).append (c.dropUntil u h)).toSubgraph = c.toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
rw [not_nil_iff_lt_length] at h
  simpa [show w.length - 1 + 1 = w.length by lia]
    using w.toSubgraph_adj_getVert (by lia : w.length - 1 < w.length)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
rintro ⟨i', ⟨hl, _⟩ | ⟨_, hl⟩⟩ <;>
    apply hp.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hl

Goal state after:
case inl
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
right✝ : p.getVert (i' + 1) = v
hl : i' = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

case inr
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
left✝ : p.getVert i' = v
hl : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hconn : G.Connected
⊢ G.dist u v = 0 ↔ u = v

Tactic:
simp [hconn u v]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 → (G □ H).Reachable x y

Tactic:
· intro ⟨⟨w₁⟩, ⟨w₂⟩⟩
    exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ (Walk.cons h p).toSubgraph.Connected

Tactic:
apply Subgraph.connected_sup (subgraphOfAdj_connected h).preconnected ih.preconnected
    exists w
    simp

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ (cycleGraph n).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
match n with
  | 0 => exact u.elim0
  | 1 => simp [cycleGraph_one_adj]
  | n + 2 => simp [cycleGraph_adj, Fin.ext_iff]

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

Goal state before:
pp: 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
hlen : p.tail.support.length = n
m : Fin n
⊢ p.support[m.succ] = p.tail.support[m]

Tactic:
simp [p.support_tail_of_not_nil hp₁.not_nil]

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

Goal state before:
pp: V : Type u_1
inst✝ : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C

Tactic:
by
  refine EdgeLabeling.ext_get ?_
  grind [toTopEdgeLabeling_get, TopEdgeLabeling.labelGraph_adj, Adj.ne]

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

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsExtremal ⊤.Free

Tactic:
rw [isExtremal_top_free_iff_isTuranMaximal]

Goal state after:
n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
sq,

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h_tendsto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)

Tactic:
turanDensity,

Goal state after:
W : Type u_1
H : SimpleGraph W
h_tendsto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (atTop.limUnder fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)

Tactic:
have hπ := tendsto_turanDensity H
  apply Tendsto.const_mul (1 / turanDensity H : ℝ) at hπ
  simp_rw [one_div_mul_cancel h, div_mul_div_comm, one_mul] at hπ
  have hz : ∀ᶠ (x : ℕ) in atTop, turanDensity H * x.choose 2 ≠ 0 := by
    rw [eventually_atTop]
    refine ⟨2, fun n hn ↦ ?_⟩
    simpa [h, Nat.choose_eq_zero_iff]
  simpa [isEquivalent_iff_tendsto_one hz] using! hπ

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
this : w.IsCycle
⊢ ⊤.egirth ≤ 3

Tactic:
egirth_le_length this

Goal state after:
α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
this : w.IsCycle
⊢ ↑w.length ≤ 3
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t ≤ extremalNumber (m + n) (completeBipartiteGraph α β)

Tactic:
by
  conv =>
    enter [2, 1]
    rw [← Fintype.card_fin (m + n)]
  simp_rw [zarankiewicz, Finset.sup_le_iff, mem_filter, mem_univ, true_and]
  intro B ⟨_, h⟩
  rw [(Iso.map finSumFinEquiv B).card_edgeFinset_eq]
  refine card_edgeFinset_le_extremalNumber <|
    (h.congr_left ?_).congr_right (Iso.map finSumFinEquiv B).symm
  exact completeBipartiteGraphCongr
    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
⊢ p₁ ⊆ (hall_subgraph f this ⋯).verts ∧ (hall_subgraph f this ⋯).IsMatching

Tactic:
refine ⟨by simp, fun v hv ↦ ?_⟩

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v : V
hv : v ∈ (hall_subgraph f this ⋯).verts
⊢ ∃! w, (hall_subgraph f this ⋯).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ ↑(f ⟨v, hy⟩) = ↑(f.symm ⟨v, hr⟩)

Tactic:
exact (h.ne_of_mem hy hr rfl).elim

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype ↑C.colorClasses
⊢ Fintype.card ↑C.colorClasses ≤ Fintype.card (Fin n)

Tactic:
exact C.card_colorClasses_le

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
have dXle : ∀ x ∈ X, 3 ≤ #{z ∈ W | ¬ G.Adj x z} := by
    intro _ hx
    by_contra! h
    obtain ⟨_, _, hW⟩ := hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf
      (by simpa [X] using hx) <| Nat.le_of_succ_le_succ h
    exact hm hW

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (n - k - 1)

Tactic:
rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
rw [Nat.le_div_iff_mul_le <| Nat.add_pos_right _ zero_lt_three]

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
⊢ G.minDegree * (2 * r + k + 3) ≤ (2 * r + k) * ‖α‖
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ #({b ∈ Gᶜ.neighborFinset v | G.Adj w b}) = k - ℓ - 1

Tactic:
← mem_neighborFinset,

Goal state after:
case convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ #({x ∈ Gᶜ.neighborFinset v | x ∈ G.neighborFinset w}) = k - ℓ - 1
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #({x ∈ G.neighborFinset v | G.Adj w x}) = μ

Tactic:
← mem_neighborFinset,

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #({x ∈ G.neighborFinset v | x ∈ G.neighborFinset w}) = μ
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
rw [decide_eq_true_eq] at h
      obtain (rfl | rfl) := h
      · rw [Nat.even_add_one, ih]
        simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
        rintro rfl rfl
        exact G.loopless.irrefl _ huv
      · have := huv.ne; grind

Goal state after: