mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
⊢ x ∉ w.support

Tactic:
rintro hxw
  obtain ⟨y, -, hxy⟩ := adj_of_mem_walk_support w (by rintro ⟨⟩; simp_all) hxw
  refine hw.not_mem_support_of_not_reachable (x := y) ?_ ?_ hxw <;>
  · rintro ⟨p⟩
    obtain ⟨hx₂, -, hy₂⟩ : G.Adj x p.penultimate ∧ _ ∧ ¬p.penultimate = y := by
      simpa using p.reverse.adj_snd (not_nil_of_ne ‹_›)
    exact hy₂ <| hx hx₂ hxy

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v ⊆ t

Tactic:
rw [isBipartiteWith_neighborFinset h hv]
  exact filter_subset (G.Adj v ·) t

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ #(G.neighborFinset v) ≤ #t

Tactic:
exact card_le_card (isBipartiteWith_neighborFinset_subset h hv)

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v w x z : V
h : G.Adj x w
p' : G.Walk w z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support

Tactic:
simp [*]

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v w x y z : V
h✝ : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
h : w ∈ p'.support
⊢ w ∈ p'.support

Tactic:
simp [*]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support → w = y ∨ w ∈ p'.support

Tactic:
by simp +contextual

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ : V
⊢ e ∈ nil.toSubgraph.edgeSet ↔ e ∈ nil.edges

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : e ∈ p✝.toSubgraph.edgeSet ↔ e ∈ p✝.edges
⊢ e ∈ (cons h✝ p✝).toSubgraph.edgeSet ↔ e ∈ (cons h✝ p✝).edges

Tactic:
simp [*]

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
⊢ cons ⋯ (Walk.map (cons h✝ w).toSubgraph.hom (Walk.map (Subgraph.inclusion ⋯) w.mapToSubgraph)) = cons h✝ w

Tactic:
map_map

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ cons ⋯ (Walk.map ((cons h✝ w).toSubgraph.hom.comp (Subgraph.inclusion ⋯)) w.mapToSubgraph) = cons h✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝¹ v v✝ : V
hadj : G.Adj u v✝
w : G.Walk v✝ v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ cons ⋯ (Walk.map { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (Walk.map (Subgraph.inclusion ⋯) w.mapToSubgraph)) =
    Walk.induce s (cons hadj w) hs

Tactic:
map_map

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
u v✝¹ v v✝ : V
hadj : G.Adj u v✝
w : G.Walk v✝ v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ cons ⋯ (Walk.map (Hom.comp { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (Subgraph.inclusion ⋯)) w.mapToSubgraph) =
    Walk.induce s (cons hadj w) hs
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ ¬p.reverse.Nil

Tactic:
by rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]; exact
        Walk.not_nil_iff_lt_length.mp hnp

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G →g G'
g : H →g H'
h : I →g I'
⊢ (f.sum (g.sum h)).comp Iso.sumAssoc.toHom = Iso.sumAssoc.toHom.comp ((f.sum g).sum h)

Tactic:
ext ((v | w) | u)

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G →g G'
g : H →g H'
h : I →g I'
v : V
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toHom) (Sum.inl (Sum.inl v)) =
    (Iso.sumAssoc.toHom.comp ((f.sum g).sum h)) (Sum.inl (Sum.inl v))

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G →g G'
g : H →g H'
h : I →g I'
w : W
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toHom) (Sum.inl (Sum.inr w)) =
    (Iso.sumAssoc.toHom.comp ((f.sum g).sum h)) (Sum.inl (Sum.inr w))

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G →g G'
g : H →g H'
h : I →g I'
u : U
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toHom) (Sum.inr u) = (Iso.sumAssoc.toHom.comp ((f.sum g).sum h)) (Sum.inr u)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
⊢ (f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding = Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)

Tactic:
ext ((v | w) | u)

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
v : V
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding) (Sum.inl (Sum.inl v)) =
    (Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)) (Sum.inl (Sum.inl v))

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
w : W
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding) (Sum.inl (Sum.inr w)) =
    (Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)) (Sum.inl (Sum.inr w))

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
u : U
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding) (Sum.inr u) =
    (Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)) (Sum.inr u)
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft.length + (w'.ofBoxProdRight.length + 1) =
    (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft else ⋯ ▸ w'.ofBoxProdLeft).length +
      (if h : True ∧ True then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
congr <;> simp [h₂.2.symm]

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
⊢ sumAssoc.comp ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc

Tactic:
ext ((v | w) | u)

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
v : V
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inl v)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inl v))

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
w : W
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inr w)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inr w))

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
u : U
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inr u) = ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inr u)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts = (⊤.induce H.verts).verts

Tactic:
by exact rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∃ v, ∀ (w : ↑s), (induce s G).Reachable v w

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

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ ∀ (w : ↑s), (induce s G).Reachable ⟨u, hu⟩ w
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✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
i✝ j✝ : V
⊢ A.complᵀ i✝ j✝ = A.compl i✝ j✝

Tactic:
simp [compl, h.apply, eq_comm]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬c u = c v

Tactic:
exact c.valid h

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩, invFun := fun x ↦ ↑x.snd, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩, invFun := fun x ↦ ↑x.snd, left_inv := ⋯, right_inv := ⋯ } b) ↔
      G.Adj a b

Tactic:
Equiv.coe_fn_mk,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj ⟨⟦a⟧, ⟨a, ⋯⟩⟩ ⟨⟦b⟧, ⟨b, ⋯⟩⟩ ↔ G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ ↑({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
              right_inv := ⋯ }
            v) %
        r ≠
      ↑({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
              right_inv := ⋯ }
            w) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w

Tactic:
Equiv.coe_fn_mk,

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ K.verts = K.parts.biUnion id

Tactic:
verts,

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ K.parts.disjiUnion id ⋯ = K.parts.biUnion id
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.verts = r * t

Tactic:
verts,

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #(K.parts.disjiUnion id ⋯) = r * t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ ⊤.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) ⊤ ↔ G.IsTuranMaximal (Fintype.card α - 1)

Tactic:
← isExtremal_top_free_iff_isTuranMaximal,

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ ⊤.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) ⊤ ↔ G.IsExtremal ⊤.Free
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #(range r) = r

Tactic:
card_range

Goal state after:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ r = r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
⊢ #({i ∈ range r | c % r = (n + i) % r}) ≤ 1

Tactic:
change #{i ∈ range r | _ ≡ _ [MOD r]} ≤ 1

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
⊢ #({i ∈ range r | c ≡ n + i [MOD r]}) ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case a
n r c : ℕ
hr : r > 0
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty

Tactic:
use ((r - 1) * n + c) % r

Goal state after:
case h
n r c : ℕ
hr : r > 0
⊢ ((r - 1) * n + c) % r ∈ {i ∈ range r | c % r = (n + i) % r}
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
| ∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

Tactic:
enter [2, v]

Goal state after:
n r : ℕ
v : Fin (n + r)
| ∑ i, if ↑v % r ≠ ↑i % r then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.radius = G.ediam
⊢ ∃ e, ∀ (u : α), G.eccent u = e

Tactic:
use G.radius

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.radius = G.ediam
⊢ ∀ (u : α), G.eccent u = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∃ e, ∀ (u : α), G.eccent u = e

Tactic:
use G.radius

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∀ (u : α), G.eccent u = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr

Goal state after:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w✝ : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).IsBipartiteWith ↑K.verts ↑K.vertsᶜ

Tactic:
by
  rw [coe_compl K.verts]
  exact between_isBipartiteWith (disjoint_compl_right)

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'
⊢ #(K.vertsᶜ \ filter K t) • (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
nsmul_eq_mul,

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'
⊢ ↑(#(K.vertsᶜ \ filter K t)) * (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑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'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts) - ↑(#(filter K t))) * (↑(#K.verts) - ↑t' + ↑t) + #(filter K t) • ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
nsmul_eq_mul,

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'
⊢ (↑n - ↑(#K.verts) - ↑(#(filter K t))) * (↑(#K.verts) - ↑t' + ↑t) + ↑(#(filter K t)) * ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ h.toEdge ⟨v, ⋯⟩ = ⟨s(v, w), hvw⟩

Tactic:
by
  rw [IsMatching.toEdge, Subtype.mk_eq_mk, ← h hvw.fst_mem |>.choose_spec.right w hvw]

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
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:
inter_comm

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
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
⊢ #(s ∩ t) = k
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:
simp_rw [toLinearMap₂'_apply', lapMatrix, sub_mulVec, dotProduct_sub, dotProduct_mulVec_degMatrix,
    dotProduct_mulVec_adjMatrix, ← sum_sub_distrib, degree_eq_sum_if_adj, sum_mul, ite_mul, one_mul,
    zero_mul, ← sum_sub_distrib, ite_sub_ite, sub_zero]
  rw [← add_self_div_two (∑ x_1 : V, ∑ x_2 : V, _)]
  conv_lhs => enter [1, 2, 2, i, 2, j]; rw [if_congr (adj_comm G i j) rfl rfl]
  conv_lhs => enter [1, 2]; rw [Finset.sum_comm]
  simp_rw [← sum_add_distrib, ite_add_ite]
  congr 2 with i
  congr 2 with j
  ring_nf

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
⊢ (G.neighborSet v).Nonempty

Tactic:
refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)

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
⊢ (p.toSubgraph.neighborSet v).ncard ≠ 0
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
⊢ Nat.casesOn 0 0 id = Nat.pred 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Nat.casesOn (n✝ + 1) 0 id = (n✝ + 1).pred

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: n : ℕ
⊢ (n + 1).ppred = none ↔ n + 1 = 0

Tactic:
by constructor <;> intro <;> contradiction

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) [] = ([], List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) [])

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
head✝ : β
tail✝ : List β
tail_ih✝ :
  List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) tail✝ =
    (tail✝, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) tail✝)
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (head✝ :: tail✝) =
    (head✝ :: tail✝, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) (head✝ :: tail✝))

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
if H : k = 0 then simp [H, eq_comm]
  else
    have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
      rw [le_antisymm_iff, ← (@Nat.lt_succ_iff _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
          Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
    simpa [H, zero_lt_iff, eq_comm (b := q)]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
⊢ List.foldr (fun b s ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.foldr (fun b s ↦ ((tail✝, l₂), b, s).2.1 :: ((tail✝, l₂), b, s).2.2) (tail✝, l₂).2 (tail✝, l₂).1 = tail✝ ++ l₂
⊢ List.foldr (fun b s ↦ ((head✝ :: tail✝, l₂), b, s).2.1 :: ((head✝ :: tail✝, l₂), b, s).2.2) (head✝ :: tail✝, l₂).2
      (head✝ :: tail✝, l₂).1 =
    head✝ :: tail✝ ++ l₂

Tactic:
simp [*]

Goal state after: