mathlib-initiative/mathlib-tactics huggingface dataset:
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
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (↑(insert w₁ s)) Set.univ
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₂ t)

Tactic:
by simp [hw.isNClique_snd_right.2]

Goal state after:
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
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (↑(insert w₁ s)) Set.univ
⊢ False

Tactic:
have := C.surjOn_of_card_le_isClique hw.isNClique_snd_right.1 (by simp [hw.isNClique_snd_right.2])

Goal state after:
α : 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
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (↑(insert w₁ s)) Set.univ
this : Set.SurjOn (⇑C) (↑(insert w₂ t)) Set.univ
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
h : Maximal (fun H ↦ H.CliqueFree (r + 1)) G
⊢ G.Colorable r ↔ G.IsCompleteMultipartite

Tactic:
by
  classical
  match r with
  | 0 => exact ⟨fun _ ↦ ⟨fun x ↦ cliqueFree_one.1 h.1 |>.elim' x⟩,
                fun _ ↦ G.colorable_zero_iff.2 <| cliqueFree_one.1 h.1⟩
  | r + 1 =>
    refine ⟨fun hc ↦ ?_, fun hc ↦ hc.colorable_of_cliqueFree h.1⟩
    contrapose hc
    obtain ⟨_, _, _, _, _, hw⟩ :=
      exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc
    exact hw.not_colorable_succ

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})
⊢ ∑ w ∈ W, G.degree w = ∑ v, #(G.neighborFinset v ∩ W)

Tactic:
[

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})
⊢ ∑ w ∈ W, G.degree w = ∑ v, #(G.neighborFinset v ∩ W)
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})
⊢ ∑ v, #(G.neighborFinset v ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)

Tactic:
[

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})
⊢ ∑ v, #(G.neighborFinset v ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)
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 ∈ X, 1) * (#W - i) + (∑ x ∈ Xᶜ, 1) * (#W - j)

Tactic:
sum_mul,

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}) ≤ ∑ i_1 ∈ X, 1 * (#W - i) + ∑ i ∈ Xᶜ, 1 * (#W - j)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fintype.card α = p.support.length

Tactic:
[

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fintype.card α = p.support.length
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.refine_1
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) ↑w

pp: case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w

Tactic:
· obtain ⟨v, hv⟩ := (Set.mem_image _ _ _).mp <| (Subgraph.verts_coeSubgraph M).symm ▸ hv
    simp only [coeSubgraph_adj, Subtype.coe_eta, Subtype.coe_prop, exists_const]
    exact ⟨hv.2 ▸ v.2, hw.1⟩

Goal state after:
case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
p : G.Walk a a
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
⊢ (Walk.map f p).tail.IsHamiltonian

Tactic:
by
    simp only [IsHamiltonian, hf.surjective.forall]
    intro x
    rcases p with (_ | ⟨y, p⟩)
    · cases hp.ne_nil rfl
    simp only [map_cons, getVert_cons_succ, tail_cons, support_copy, support_map]
    rw [List.count_map_of_injective _ _ hf.injective]
    simpa using hp.isHamiltonian_tail x

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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))

Tactic:
[

Goal state after:
α : 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
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
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
[

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
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 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✝ : NonAssocRing R
v : V
vec : V → R
⊢ (lapMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u

Tactic:
[

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✝ : NonAssocRing R
v : V
vec : V → R
⊢ (lapMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u
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
⊢ (((toLinearMap₂' R) (lapMatrix R G)) x) x = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
[

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
⊢ (((toLinearMap₂' R) (lapMatrix R G)) x) x = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
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, ((∑ j, if G.Adj x_1 j then 1 else 0) * x x_1 * x x_1 - ∑ j, if G.Adj x_1 j then x x_1 * x j else 0) =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
sum_mul,

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, (∑ i, (if G.Adj x_1 i then 1 else 0) * x x_1 * x x_1 - ∑ j, if G.Adj x_1 j then x x_1 * x j else 0) =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
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) +
        ∑ y, ∑ x_1, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) /
      2 =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
[

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) +
        ∑ y, ∑ x_1, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) /
      2 =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: case refine_1
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).IsHermitian

Tactic:
IsHermitian,

Goal state after:
case refine_1
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G)ᴴ = lapMatrix R G
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ M, M.IsPerfectMatching

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃ w', w ≠ w' ∧ G.Adj v w'

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃ w', w ≠ w' ∧ G.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'

Tactic:
[

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.spanningCoe.IsCycles

Tactic:
by
  intro v hv
  apply hpc.ncard_neighborSet_toSubgraph_eq_two
  obtain ⟨_, hw⟩ := hv
  exact p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles

Tactic:
exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs])

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑2 = ↑(p.toSubgraph.neighborSet v).ncard

Tactic:
this

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ ↑2 = ↑2
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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))

Tactic:
have ⟨h1s, h2t⟩ : insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W := by grind

Goal state after:
α : 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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ ↑(t'.choose t) ^ r * ↑t + ↑r * ↑t' ≤ (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)

Tactic:
rw [mul_div_assoc, le_mul_iff_one_le_right (by positivity),
              one_le_div (sub_pos.mpr ht_lt_rt'ε), sub_le_sub_iff_right,
              mul_comm (r : ℝ) (t' : ℝ),  mul_assoc, mul_le_iff_le_one_right (by positivity)]
            exact hrε_lt_1.le

Goal state after:
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
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ

Tactic:
rw [← h.of_not_adj hne ha]
  exact h.card_neighborFinset_union_eq

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

Goal state before:
pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_ne_1 : r ≠ 1
⊢ completeEquipartiteGraph r t' ⊑ G

Tactic:
· have hδ' := calc (G.minDegree : ℝ)
          _ ≥ (1 - 1 / (r - 1) + (1 / (r - 1) - 1 / r) + ε) * n := by
              rwa [← sub_add_sub_cancel _ (1 / (r - 1) : ℝ) _] at hδ
          _ = (1 - 1 / ↑(r - 1) + ε') * n := by
              rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div
                (sub_ne_zero_of_ne (mod_cast hr_ne_1)) (mod_cast hr_pos.ne'),
                sub_sub_cancel, mul_one, one_div_mul_one_div_rev, mul_comm (r : ℝ) _,
                ← Nat.cast_pred hr_pos, add_assoc]
        rw [← Nat.succ_pred_eq_of_pos hr_pos]
        exact ih n (hn.trans' (le_max_of_le_left (le_max_right 1 N'))) hδ'

Goal state after:
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 : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2

Tactic:
[

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 : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2
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
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Tactic:
[

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
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * 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
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1

Tactic:
[

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
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1
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)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
[

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)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3.e_a.e_a
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) = ℓ

Tactic:
[

Goal state after:
case convert_3.e_a.e_a
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) = ℓ
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:
[

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
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ