mathlib-initiative/mathlib-tactics huggingface dataset:
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) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i) → B ⊆ range'k ∧ #B = r - i

Tactic:
rintro ⟨A, Ah, hBA, card_sdiff_i⟩

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 ∈ 𝒞
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ A = ∅

Tactic:
← Finset.card_eq_zero,

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ #A = 0
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ (G.deleteEdges {s(v, w)}).edgeSet

Tactic:
rw [edgeSet_deleteEdges]

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ G.edgeSet \ {s(v, w)}
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₁ (insert a s) * 0 + f₁ (insert a s) * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

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

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
⊢ G.chromaticNumber ≤ ↑(card V) - 1

Tactic:
apply chromaticNumber_le_iff_colorable.mpr

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
⊢ G.Colorable (card V - 1)
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)
⊢ α ⊕ β ↪ V

Tactic:
by
    refine ⟨Sum.elim (Subtype.val ∘ fα) (Subtype.val ∘ fβ), fun s₁ s₂ ↦ ?_⟩
    match s₁, s₂ with
    | .inl p₁, .inl p₂ => simp
    | .inr p₁, .inl p₂ =>
      simpa using (h (fα p₂).prop (fβ p₁).prop).ne'
    | .inl p₁, .inr p₂ =>
      simpa using (h (fα p₁).prop (fβ p₂).prop).symm.ne'
    | .inr p₁, .inr p₂ => simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
⊢ between s t G = between t s G

Tactic:
simp [between, or_comm]

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

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w

Tactic:
· simpa [adj_toSubgraph_iff_mem_edges] using! fun _ _ h ↦ p.edges_toPath_subset_edges h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ Walk.map (cons h✝ w).toSubgraph.hom (cons h✝ w).mapToSubgraph = cons h✝ w

Tactic:
by
    rw [mapToSubgraph, Walk.map, map_map]
    exact congrArg₂ _ rfl w.map_mapToSubgraph_hom

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < G.dist u v
⊢ Set.univ.Nonempty

Tactic:
rw [dist_eq_sInf] at h

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < sInf (Set.range Walk.length)
⊢ Set.univ.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Or.by_cases ⋯ (fun hG ↦ cons ⋯ (Walk.map (G.boxProdLeft H b).toHom w).ofBoxProdLeft) fun hH ↦
      ⋯ ▸ (Walk.map (G.boxProdLeft H b).toHom w).ofBoxProdLeft) =
    cons' x y z h w

Tactic:
Or.by_cases,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (if hp : G.Adj (x, b).1 ((G.boxProdLeft H b).toHom y).1 ∧ (x, b).2 = ((G.boxProdLeft H b).toHom y).2 then
      cons ⋯ (Walk.map (G.boxProdLeft H b).toHom w).ofBoxProdLeft
    else ⋯ ▸ (Walk.map (G.boxProdLeft H b).toHom w).ofBoxProdLeft) =
    cons' x y z h w
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
⊢ (⋯.by_cases (fun hH ↦ cons ⋯ (Walk.map (G.boxProdRight G a).toHom w).ofBoxProdRight) fun hG ↦
      ⋯ ▸ (Walk.map (G.boxProdRight G a).toHom w).ofBoxProdRight) =
    cons' x y z h w

Tactic:
Or.by_cases,

Goal state after:
α : 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
⊢ (if hp : G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1 then
      cons ⋯ (Walk.map (G.boxProdRight G a).toHom w).ofBoxProdRight
    else ⋯ ▸ (Walk.map (G.boxProdRight G a).toHom w).ofBoxProdRight) =
    cons' x y z h w
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
β : Type u_2
V : Type u_3
inst✝ : DecidableEq V
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ Function.LeftInverse (fun v_1 ↦ ⟨List.idxOf (↑v_1) w.support, ⋯⟩) ⇑w.pathGraphHomToSubgraph

Tactic:
by grind [pathGraphHomToSubgraph, RelHom.coeFn_mk, hw.support_nodup]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
⊢ ∀ (x : G.Walk u v), x ∈ {w ∈ G.finsetWalkLength n u v | w.IsPath} ↔ x ∈ {p | p.IsPath ∧ p.length = n}

Tactic:
simp [mem_finsetWalkLength_iff, and_comm]

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

Goal state before:
pp: case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Preconnected

pp: case mpr.refine_2
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ ∀ (u v : V) (x y : G.Path u v), x = y

Tactic:
· intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable

Goal state after:
case mpr.refine_2
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ ∀ (u v : V) (x y : G.Path u v), x = y
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
⊢ (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup

Tactic:
have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
        tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
          ⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩

Goal state after:
case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
⊢ (s(u', v') ∉ (tail.takeUntil u' hh).edges ∧ (tail.takeUntil u' hh).edges.Nodup) ∧ (tail.takeUntil u' hh).support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
h : A.compl = B.compl
i j : V
⊢ A i j = B i j

Tactic:
by
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
    without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
    as we are relying on seeing through the definition of `Matrix`, and `of`.
    The original proof was: `grind [of, congr($h i j), compl, IsAdjMatrix]` -/
    simp [compl] at h; grind [congr($h i j), IsAdjMatrix]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
h : G.IsTree
⊢ Nat.card ↑G.edgeSet + 1 = Nat.card V

Tactic:
simpa [edgeFinset] using h.card_edgeFinset

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Set.univ.PairwiseDisjoint C.labelGraph

Tactic:
intro _ _ _ _ h
  exact pairwise_disjoint_labelGraph h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Set.univ.PairwiseDisjoint C.labelGraph

Tactic:
by
  intro _ _ _ _ h
  exact pairwise_disjoint_labelGraph h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
obtain ⟨T, _, T_isTree⟩ := hconn.exists_isTree_le
  have ⟨hT, _⟩ := T_isTree
  have := Fintype.ofFinite V
  classical
  obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial
  exact ⟨v, (hT.induce_compl_singleton_of_degree_eq_one hv).mono (by tauto)⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
⊢ G.dist u v ≠ G.dist u w

Tactic:
← hp',

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
⊢ p.length ≠ G.dist u w
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| r * (t - 1 + 1)

Tactic:
Nat.mul_add_one,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| r * (t - 1) + r
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
⊢ G.Adj u v ↔ ⊤.Adj u v

Tactic:
refine ⟨Adj.ne, fun huv ↦ ?_⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : ⊤.Adj u v
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.edist u v ≤ 1

Tactic:
rw [edist_le_one_iff_adj_or_eq]

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.Adj u v ∨ u = v
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
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * (n' / r + 1) ^ 2 / 2

Tactic:
have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd

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)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * (n' / r + 1) ^ 2 / 2
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph u ≤ finsubgraphOfAdj e

Tactic:
by
  simp [singletonFinsubgraph, finsubgraphOfAdj]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph v ≤ finsubgraphOfAdj e

Tactic:
by
  simp [singletonFinsubgraph, finsubgraphOfAdj]

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

Goal state before:
pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < t

Tactic:
contrapose! hs

Goal state after:
case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
⊢ ∃ x ∈ powersetCard t p, ∀ x_1 ∈ x, G.Adj v x_1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H ⊑ G

Tactic:
classical
  rw [(G.overFinIso rfl).card_edgeFinset_eq, isContained_congr Iso.refl (G.overFinIso rfl)]
  apply Nat.find_spec <| eventually_atTop.mp <| eventually_isContained_of_card_edgeFinset H hε_pos
  simpa only [turanDensityConst, hε_pos, ↓reduceDIte] using h_verts

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'
⊢ ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset) =
    ∑ v ∈ K.vertsᶜ \ {v ∉ K.verts | ∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w},
        ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) +
      ∑ v ∈ K.vertsᶜ with ∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w,
        ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v)

Tactic:
sum_sdiff (filter_subset _ 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'
⊢ ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset) = ∑ x ∈ K.vertsᶜ, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree x)
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 * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)

Tactic:
← add_sub_cancel_right (N : ℝ) (r * t' : ℝ),

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 + ↑r * ↑t' - ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
p2 : G.IsPathGraph3Compl v w₁ w₂
d1 : v ∉ s
d2 : v ∉ t
d3 : w₁ ∉ s
d4 : w₂ ∉ t
c1 : G.IsNClique (r + 1) (insert v s)
c2 : G.IsNClique (r + 1) (insert w₁ s)
c3 : G.IsNClique (r + 1) (insert v t)
c4 : G.IsNClique (r + 1) (insert w₂ t)
hk : #(s ∩ t) = k
⊢ #(t ∩ s) = k

Tactic:
by rwa [inter_comm]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ x ∈ X, #({w ∈ W | G.Adj x w}) + ∑ x ∈ Xᶜ, #({w ∈ W | G.Adj x w}) ≤ #X * (#W - i) + #Xᶜ * (#W - j)

Tactic:
card_eq_sum_ones X,

Goal state after:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ x ∈ X, #({w ∈ W | G.Adj x w}) + ∑ x ∈ Xᶜ, #({w ∈ W | G.Adj x w}) ≤ (∑ x ∈ X, 1) * (#W - i) + #Xᶜ * (#W - j)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
hG : G.IsHamiltonian
v : α
⊢ ∃ p, p.IsHamiltonianCycle

Tactic:
obtain ⟨u, p, hp⟩ := hG Fintype.one_lt_card.ne'; exact ⟨p.rotate v <| hp.mem_support _, by simpa⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x

Tactic:
refine ⟨?_, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ v ≠ x

case refine_2
α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₁ ≠ x

case refine_3
α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₂ ≠ x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
hMmatch : (M.induce (Subtype.val '' (↑c).supp)).IsMatching
this : Fintype ↑(M.induce (Subtype.val '' (↑c).supp)).verts
⊢ Even (↑c).supp.ncard

Tactic:
have := Fintype.ofFinite c.val.supp
  simpa [Finset.card_image_of_injective] using hMmatch.even_card

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
⊢ (p.toSubgraph.neighborSet v).ncard ≠ 0

Tactic:
rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]

Goal state after:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv✝ : v✝ ∈ c.supp
w✝ : V
hw : w✝ ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w✝) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
⊢ 2 ≠ 0