mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G✝ : SimpleGraph (Fin n)
⊢ ∀ [inst : DecidableRel G✝.Adj], H'.Free G✝ → #G✝.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
_

Goal state after:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G✝ : SimpleGraph (Fin n)
inst✝ : DecidableRel G✝.Adj
⊢ H'.Free G✝ → #G✝.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
⊢ ∀ [inst : DecidableRel G.Adj], H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂

Tactic:
_

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
⊢ H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
⊢ ∀ [inst : DecidableRel G.Adj], H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁

Tactic:
_

Goal state after:
case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
⊢ H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
⊢ ⋯.toGraph = h.toGraphᶜ

Tactic:
by
  ext v w
  rcases h.zero_or_one v w with h | h <;> by_cases hvw : v = w <;> simp [Matrix.compl, h, hvw]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
⊢ ¬3 ≤ G.chromaticNumber → False

Tactic:
intro h
  have h' : G.chromaticNumber ≤ 2 := Order.le_of_lt_add_one <| not_le.mp h
  let c : G.Coloring (Fin 2) := (chromaticNumber_le_iff_colorable.mp h').some
  let c' : G.Coloring Bool := recolorOfEquiv G finTwoEquiv c
  have : ¬c' u ↔ c' u := (c'.odd_length_iff_not_congr p).mp hOdd
  simp_all

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
i✝ : K
⊢ ∀ ⦃j : K⦄, i✝ ≠ j → (fun k l ↦ Disjoint (C.labelGraph k) (C.labelGraph l)) i✝ j

Tactic:
_

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i✝ j✝ : K
⊢ i✝ ≠ j✝ → (fun k l ↦ Disjoint (C.labelGraph k) (C.labelGraph l)) i✝ j✝
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
x✝ : K
⊢ x✝ ∈ Set.univ → ∀ ⦃y : K⦄, y ∈ Set.univ → x✝ ≠ y → Function.onFun Disjoint C.labelGraph x✝ y

Tactic:
_

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x✝ : K
a✝ : x✝ ∈ Set.univ
⊢ ∀ ⦃y : K⦄, y ∈ Set.univ → x✝ ≠ y → Function.onFun Disjoint C.labelGraph x✝ y
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
x✝ : K
a✝ : x✝ ∈ Set.univ
⊢ ∀ ⦃y : K⦄, y ∈ Set.univ → x✝ ≠ y → Function.onFun Disjoint C.labelGraph x✝ y

Tactic:
_

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x✝ : K
a✝ : x✝ ∈ Set.univ
y✝ : K
⊢ y✝ ∈ Set.univ → x✝ ≠ y✝ → Function.onFun Disjoint C.labelGraph x✝ y✝
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
x✝ : K
a✝ : x✝ ∈ Set.univ
y✝ : K
⊢ y✝ ∈ Set.univ → x✝ ≠ y✝ → Function.onFun Disjoint C.labelGraph x✝ y✝

Tactic:
_

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x✝ : K
a✝¹ : x✝ ∈ Set.univ
y✝ : K
a✝ : y✝ ∈ Set.univ
⊢ x✝ ≠ y✝ → Function.onFun Disjoint C.labelGraph x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ : Fin 3
⊢ ∀ ⦃a₂ : Fin 3⦄,
    (fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂)
          a₁✝ =
        (fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂)
          a₂ →
      a₁✝ = a₂

Tactic:
_

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
⊢ (fun x ↦
          match x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂)
        a₁✝ =
      (fun x ↦
          match x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂)
        a₂✝ →
    a₁✝ = a₂✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
⊢ (fun x ↦
          match x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂)
        a₁✝ =
      (fun x ↦
          match x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂)
        a₂✝ →
    a₁✝ = a₂✝

Tactic:
_

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ : Fin 3
⊢ ∀ {b : Fin 3},
    G.Adj
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          a✝)
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          b) ↔
      (pathGraph 3)ᶜ.Adj a✝ b

Tactic:
_

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
⊢ G.Adj
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        a✝)
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        b✝) ↔
    (pathGraph 3)ᶜ.Adj a✝ b✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1 = ↑v.1

Tactic:
1,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1

Tactic:
1,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1

Tactic:
1,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩)

Tactic:
1,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

Tactic:
rintro ⟨u, v⟩ huv

Goal state after:
case refine_2.mk
V : Type u_1
G : SimpleGraph V
h : Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2
e✝ : Sym2 V
u v : V
huv : Quot.mk (Sym2.Rel V) (u, v) ∈ G.edgeSet
⊢ G.IsBridge (Quot.mk (Sym2.Rel V) (u, v))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| extremalNumber n ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
1,

Goal state after:
n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| extremalNumber n ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| ↑(extremalNumber (n + 1) H) / ↑((n + 1).choose 2)

Tactic:
1,

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
| ↑(extremalNumber (n + 1) H)
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.Free G → ↑(#G.edgeFinset) ≤ ↑(extremalNumber n H) / ↑(n.choose 2) * ↑((n + 1).choose 2)

Tactic:
_

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
⊢ H.Free G → ↑(#G.edgeFinset) ≤ ↑(extremalNumber n H) / ↑(n.choose 2) * ↑((n + 1).choose 2)
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'
v : Fin n
ht'_pos : 0 < t'
hv : False ∨ v ∈ K.vertsᶜ ∧ ¬∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t

Tactic:
false_or,

Goal state after:
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 ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t
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'
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 ∈ K.verts | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < #K.verts - t' + t

Tactic:
1,

Goal state after:
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 ∈ K.verts | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
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'
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 ∈ K.verts | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})

Tactic:
1,

Goal state after:
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 ∈ K.verts | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: 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)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
| ↑(extremalNumber n H)

Tactic:
1,

Goal state after:
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)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
| extremalNumber n H
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
| 2 * extremalNumber n (completeBipartiteGraph α β) ≤ zarankiewicz n n s t

Tactic:
1,

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
| 2 * extremalNumber n (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (t ∪ u).ncard

Tactic:
ncard_union_eq hdtu hfin.1 hfin.2,

Goal state after:
case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (t.ncard + u.ncard)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
⊢ ∀ [inst : DecidableRel G.Adj], (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2

Tactic:
_

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
⊢ (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : Infinite α
⊢ ¬p.IsHamiltonian

Tactic:
by
  contrapose! h; exact h.finite

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : Infinite α
⊢ ¬p.IsHamiltonianCycle

Tactic:
by
  contrapose! h; exact h.finite

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
⊢ e ∈ G.edgeSet → ∑ a, incMatrix R G a e = 2

Tactic:
refine e.ind ?_

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ∑ a, incMatrix R G a s(x, y) = 2
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ e ∈ G.edgeSet → ↑(#{x | e ∈ G.incidenceSet x}) = 2

Tactic:
refine e.ind ?_

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ↑(#{x_1 | s(x, y) ∈ G.incidenceSet x_1}) = 2
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ e ∉ G.edgeSet → ↑(#{x | e ∈ G.incidenceSet x}) = 0

Tactic:
refine e.ind ?_

Goal state after:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∉ G.edgeSet → ↑(#{x_1 | s(x, y) ∈ G.incidenceSet x_1}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ (∑ x, if x ∈ G.incidenceSet a ∩ G.incidenceSet b then 1 x else 0) = 1

Tactic:
Pi.one_apply,

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ (∑ x, if x ∈ G.incidenceSet a ∩ G.incidenceSet b then 1 else 0) = 1
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ((∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
      ∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) /
    2

Tactic:
1,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| (∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
    ∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ((∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
      ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0) /
    2

Tactic:
1,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| (∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
    ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
w' : V
hww' : w' ∈ G.neighborSet v ∧ w' ≠ w
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩

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

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
⊢ x ∈ ⊤ → x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

Tactic:
_

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: V : Type u_1
r w✝ : V
⊢ r ≠ w✝ → (starGraph r).Adj r w✝

Tactic:
_

Goal state after:
V : Type u_1
r w✝ : V
a✝ : r ≠ w✝
⊢ (starGraph r).Adj r w✝
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 ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]

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 ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - (1 + 1) = n - (2 * k - μ) - 2

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
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
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w ∩ Gᶜ.neighborFinset v) = k - ℓ - 1

Tactic:
neighborFinset_compl,

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
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w ∩ ((G.neighborFinset v)ᶜ \ {v})) = 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 : w ∈ Gᶜ.neighborFinset v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ

Tactic:
neighborFinset_compl,

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 : w ∈ (G.neighborFinset v)ᶜ \ {v}
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ
Module: Mathlib.Combinatorics.SimpleGraph.Trails

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

Tactic:
· have := huv.ne; grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
nontriviality V
  obtain ⟨x⟩ := not_subsingleton_iff_nontrivial.mp (not_subsingleton V) |>.to_nonempty
  refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_
  simp only [vertexCoverNum, le_iInf_iff] at hn
  have := hn (Set.univ \ {x}) (by grind [IsVertexCover, Adj.ne'])
  simpa [Set.encard_sdiff_singleton_of_mem (Set.mem_univ _)] using this

Goal state after: