mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
⊢ ∃ a, C a = b

Tactic:
by_cases he : C (Sum.inl v) = b

Goal state after:
case pos
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : C (Sum.inl v) = b
⊢ ∃ a, C a = b

case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
⊢ ∃ a, C a = b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
⊢ (induce s G).Preconnected

Tactic:
by
  rintro ⟨u, hu⟩ ⟨v, hv⟩
  obtain ⟨p, hp⟩ := hG.exists_isPath u v
  constructor
  convert! p.induce s _
  rintro w hwp
  by_contra hws
  exact hp.not_mem_support_of_subsingleton_neighborSet (by grind) (by grind) (hs _ hws) hwp

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 ⊆ ∅.powerset
hℬ : ℬ ⊆ ∅.powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ

Goal state after:
case empty
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case refine_2.inl
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
hs : ∅.encard < ↑(k + 1)
⊢ (G.deleteEdges ∅).Reachable u v

Tactic:
simpa using (h s(u, u)).reachable hk

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

Goal state before:
pp: case neg.inr
V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
x : Sym2 V
hs₂ : {x}.encard < ↑2
hs₁ : {x}.encard = ↑1
hx : s(u, v) ≠ x
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
· exact deleteEdges_adj.mpr ⟨huv, hx⟩ |>.reachable

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

Goal state before:
pp: case refine_2
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this✝ : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
this :
  (∑ s ∈ map { toFun := ⇑g, inj' := hg } s', extend (⇑g) (f₁ ∘ Subtype.val) 0 s) *
      ∑ s ∈ map { toFun := ⇑g, inj' := hg } t', extend (⇑g) (f₂ ∘ Subtype.val) 0 s ≤
    (∑ s ∈ map { toFun := ⇑g, inj' := hg } s' ⊼ map { toFun := ⇑g, inj' := hg } t',
        extend (⇑g) (f₃ ∘ Subtype.val) 0 s) *
      ∑ s ∈ map { toFun := ⇑g, inj' := hg } s' ⊻ map { toFun := ⇑g, inj' := hg } t', extend (⇑g) (f₄ ∘ Subtype.val) 0 s
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Tactic:
simpa only [← hs', ← ht', ← map_sups, ← map_infs, sum_map, Embedding.coeFn_mk, hg.extend_apply]
      using! this

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
⊢ v' ∈ G'.verts

Tactic:
have ⟨e, he, hv'e⟩ := hv'

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
e : Sym2 V
he : e ∈ w.edges
hv'e : v' ∈ e
⊢ v' ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(u, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
cases u

Goal state after:
case refine_1.inl
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₁
h : s(Sum.inl val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

case refine_1.inr
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₂
h : s(Sum.inr val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ G.edist u v ≠ ⊤

Tactic:
rw [h]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ ↑k ≠ ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ edist ?m.16 ?m.17 ?m.18 ≠ ⊤

Tactic:
rw [h]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤
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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
u v : V ⊕ W
⊢ (G ⊕g H).Adj u v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) u) (Sum.map (⇑f) (⇑g) v)

Tactic:
cases u

Goal state after:
case 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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝)) (Sum.map (⇑f) (⇑g) v)

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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝)) (Sum.map (⇑f) (⇑g) v)
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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
u v : V ⊕ W
⊢ Sum.map (⇑f) (⇑g) u = Sum.map (⇑f) (⇑g) v → u = v

Tactic:
cases u

Goal state after:
case 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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : V
⊢ Sum.map (⇑f) (⇑g) (Sum.inl val✝) = Sum.map (⇑f) (⇑g) v → Sum.inl val✝ = v

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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : W
⊢ Sum.map (⇑f) (⇑g) (Sum.inr val✝) = Sum.map (⇑f) (⇑g) v → Sum.inr val✝ = v
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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
u v : V ⊕ W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } u) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } v) ↔ (G ⊕g H).Adj u v

Tactic:
cases u

Goal state after:
case 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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : V
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } v) ↔
    (G ⊕g H).Adj (Sum.inl val✝) v

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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } v) ↔
    (G ⊕g H).Adj (Sum.inr val✝) v
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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
u v : V ⊕ W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) u) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj u v

Tactic:
cases u

Goal state after:
case 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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
v : V ⊕ W
val✝ : V
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj (Sum.inl val✝) v

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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
v : V ⊕ W
val✝ : W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj (Sum.inr val✝) v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
use p.reverse
    rw [penultimate, ← getVert_reverse] at hr
    exact ⟨h.reverse, hr.symm, by rw [toSubgraph_reverse _]⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) ∧ H.verts.Nonempty ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
and_comm

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
u v : V ⊕ W
huv : (G ⊕g H).Adj u v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) u) (Sum.elim (⇑cG) (⇑cH) v)

Tactic:
cases u

Goal state after:
case 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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝)) (Sum.elim (⇑cG) (⇑cH) v)

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
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝)) (Sum.elim (⇑cG) (⇑cH) v)
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

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

Tactic:
rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]

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

Goal state before:
pp: case mpr.inl
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
h : ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
v g : M
hg : g ∈ s
hvw : ¬v = v * g
⊢ G.Adj v (v * g)

Tactic:
exact (h g hg v (hvw ·.symm)).symm

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

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

Tactic:
refine ⟨Connected.mk ?_, ?_⟩

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

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.Extremal.Basic

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
rw [Iso.card_edgeFinset_eq (.map e G)]

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
rw [Iso.card_edgeFinset_eq (.map e G)]

Goal state after:
case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
h' : SimpleGraph.map (⇑e) G ∈ {x | H.Free x}
⊢ #(SimpleGraph.map (⇑e) G).edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ Odd {v | G.connectedComponentMk v = c}.ncard ∧
      {v | G.connectedComponentMk v = c} ⊆ {v | G'.connectedComponentMk v = c'} ↔
    {v | G.connectedComponentMk v = c} ⊆ {v | G'.connectedComponentMk v = c'} ∧
      Odd {v | G.connectedComponentMk v = c}.ncard

Tactic:
and_comm

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

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (∑ x, x.supp.ncard)

Tactic:
← Finset.coe_filter_univ,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (↑{x | Odd x.supp.ncard}).ncard ↔ Odd (∑ x, x.supp.ncard)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ IsEmpty (Fin r × Fin t)

Tactic:
simp [ht, Fin.isEmpty]

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

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : n + w ≡ n + x [MOD r]
⊢ w = x

Tactic:
Nat.ModEq.add_iff_left rfl

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w ≡ x [MOD r]
⊢ w = x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ (c.supp \ s).ncard = c.supp.ncard

Tactic:
(disjoint_supp_of_notMem hrep h).sdiff_eq_right

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ c.supp.ncard = c.supp.ncard
Module: Mathlib.Combinatorics.SimpleGraph.Diam

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

Tactic:
intro hall

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
⊢ G.eccent u ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ False

Tactic:
exact h <| IsEmpty.forall_iff.mpr trivial

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
r' : ℕ
⊢ IsEmpty (Fin r' × Fin t)

Tactic:
simp [ht, Fin.isEmpty]

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

Goal state before:
pp: case inr.inr
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
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
let n' := n - r
      have n'r : n = n' + r := by lia
      rw [n'r, card_edgeFinset_turanGraph_add, card_edgeFinset_turanGraph, ring₁, ring₁,
        add_rotate, ← add_assoc, Nat.add_mod_right, Nat.add_div_right _ hr]
      congr 1
      have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd
      rw [← Nat.div_mul_right_comm rd, ← Nat.div_mul_right_comm rd, ← Nat.choose_two_right]
      have ring₂ : n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
          n' % r * (n' / r + 1) * (r - 1) + r.choose 2 +
          r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2 := by grind
      rw [ring₂, ← add_assoc]; congr 1
      rw [← add_rotate, ← add_rotate _ _ (r.choose 2)]; congr 1
      rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
        ← add_rotate, add_comm _ (_ * _)]; congr 1
      rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
⊢ (⋃ i, s i).ncard ≤ ∑ᶠ (i : ι), (s i).ncard

Tactic:
by
  simpa using finite_univ.ncard_biUnion_le s

Goal state after:
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 | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = {s(a, b)}

Tactic:
exact G.incidenceSet_inter_incidenceSet_of_adj h

Goal state after:
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:
obtain ⟨w', ⟨hww, hww'⟩⟩ := h.other_adj_of_adj hadj

Goal state after:
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'
⊢ ∃! w', w ≠ w' ∧ G.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
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
⊢ completeEquipartiteGraph r t' ⊑ G

Tactic:
have h0 : r ≤ 1 ∨ t' = 0 := Or.inl hr_eq_1.le
        rw [completeEquipartiteGraph_eq_bot_iff.mpr h0, bot_isContained_iff_card_le,
          card_prod, Fintype.card_fin, Fintype.card_fin, hr_eq_1, one_mul, Fintype.card_fin]
        apply hn.trans'
        exact_mod_cast calc (t' : ℝ)
          _ ≤ r * t' := le_mul_of_one_le_left (by positivity) (mod_cast hr_pos)
          _ ≤ t'.choose t ^ r * t + r * t' := le_add_of_nonneg_left (by positivity)
          _ ≤ (t'.choose t ^ r * t + r * t') * (t' - t) / (r * t' * ε - t) := by
            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
          _ ≤ ⌈(t'.choose t ^ r * t + r * t') * (t' - t) / (r * t' * ε - t)⌉₊ := Nat.le_ceil _
          _ ≤ N := Nat.cast_le.mpr (le_max_right _ _)

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 ℓ μ
ha : G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ

Tactic:
rw [← h.of_adj v w ha]
  exact h.card_neighborFinset_union_eq

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

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