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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        _x →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.length

Tactic:
{

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        _x →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ∀ (v w : V), (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w

Tactic:
intro v w h

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
⊢ G.Reachable v w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case cons
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
⊢ C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h

Goal state after:
case cons
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
hw : w ∈ C
⊢ C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (extend (⇑f) (⇑C) (const β default) b)

Tactic:
← hb,

Goal state after:
case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (extend (⇑f) (⇑C) (const β default) (f w✝))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
e : Sym2 V
hG : G ≤ G'
h : G'.IsBridge e
⊢ G.IsBridge e

Tactic:
by obtain ⟨a, b⟩ := e; rw [isBridge_iff] at ⊢ h; grw [hG]; assumption

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsEdgeConnected 1 ↔ G.Preconnected

Tactic:
by
  simp [IsEdgeConnected, Preconnected]

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

Tactic:
{

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

Tactic:
{

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

Tactic:
mapToSubgraph,

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ Walk.map (cons h✝ w).toSubgraph.hom (cons ⋯ (Walk.map (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
⊢ Walk.map { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (cons hadj w).mapToSubgraph = Walk.induce s (cons hadj w) hs

Tactic:
mapToSubgraph,

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
⊢ Walk.map { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (cons ⋯ (Walk.map (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
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
obtain ⟨x, hxs, hx, h⟩ := p.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty s h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h✝ : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable n

Tactic:
by rw [← n.max_self]; exact cG.sum_max cH

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLength n u v ↔ p ∈ {p | p.length = n}

Tactic:
by
    rw [← Finset.mem_coe, coe_finsetWalkLength_eq]

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

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

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

Tactic:
· rintro ⟨hc, hu⟩
    refine ⟨hc.nonempty, ?_⟩
    intro v w
    let q := (hc v w).some.toPath
    use q
    simp only [true_and, Path.isPath]
    intro p hp
    specialize hu v w ⟨p, hp⟩ q
    exact Subtype.ext_iff.mp hu

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
have := hG.connected.nonempty

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
⊢ G.edgeFinset.card + 1 = Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ ¬extremalNumber (Fintype.card V) H < #G.edgeFinset

Tactic:
push Not

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
⊢ (G ⊔ edge u v).IsAcyclic ↔ G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)

Tactic:
refine ⟨?_, fun ⟨hacyc, hreach⟩ ↦ hacyc.sup_edge_of_not_reachable <| by grind⟩

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
⊢ (G ⊔ edge u v).IsAcyclic → G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
push Not

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
push Not

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
⊢ ¬∀ ⦃x : V⦄, x ∈ ↑z → ∀ ⦃y : V⦄, y ∈ ↑z → x ≠ y → G.Adj x y

Tactic:
push Not

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
v₁' : ↑(C.colorClass c₂) := ⟨↑v₁, ⋯⟩
hv : (F c₂) v₁' = (F c₂) v₂
hv' : (F c₁) v₁ = (F c₂) v₁'
⊢ ↑v₁ = ↑v₂

Tactic:
simpa [Subtype.ext_iff] using (F c₂).injective hv

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

Goal state before:
pp: case injective'
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
hF : ∀ {c₁ c₂ : Fin n} {v₁ : ↑(C.colorClass c₁)} {v₂ : ↑(C.colorClass c₂)}, c₁ = c₂ → (F c₁) v₁ = (F c₂) v₂ → ↑v₁ = ↑v₂
⊢ Injective ⇑{ toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ }

Tactic:
intro v w h

Goal state after:
case injective'
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h✝ : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
hF : ∀ {c₁ c₂ : Fin n} {v₁ : ↑(C.colorClass c₁)} {v₂ : ↑(C.colorClass c₂)}, c₁ = c₂ → (F c₁) v₁ = (F c₂) v₂ → ↑v₁ = ↑v₂
v w : α
h :
  { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } v =
    { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } w
⊢ v = w
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_3
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ G.radius = 0

Tactic:
rw [radius, ENat.iInf_eq_zero]
    use Classical.ofNonempty
    simpa [eccent] using Subsingleton.elim _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : G.ComponentCompl ↑K → ↑{v | ∃ k ∈ K, G.Adj k v} :=
  fun C ↦
    let p := ⋯;
    ⟨p.choose.1, ⋯⟩
touch_inj : Function.Injective touch
this : Finite ↑(Set.range touch)
⊢ Finite (G.ComponentCompl ↑K)

Tactic:
apply Finite.of_injective_finite_range touch_inj

Goal state after:
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:
enter [1, 2, 1]
    rw [← Fintype.card_fin n]

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
| Fintype.card (Fin n)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = ∑ᶠ (i : ι), (s i).ncard

Tactic:
rw [← finsum_mem_univ, ← finite_univ.ncard_biUnion (by simpa) (fun _ _ _ _ hab ↦ h hab)]
  simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ ∃ M, p₁ ⊆ M.verts ∧ M.IsMatching

Tactic:
classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ {v w : V}, ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → G.Adj v w

Tactic:
intro v w h

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h✝ : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v w : V
h : (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.support = 1

Tactic:
rw [← cons_support_tail hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]

Goal state after:
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)
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ↑(#{x_1 | s(x, y) ∈ G.incidenceSet x_1}) = 2

Tactic:
intro v w h

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)
v w : α
h : s(v, w) ∈ G.edgeSet
⊢ ↑(#{x | s(v, w) ∈ G.incidenceSet x}) = 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)
⊢ ∀ (x y : α), s(x, y) ∉ G.edgeSet → ↑(#{x_1 | s(x, y) ∈ G.incidenceSet x_1}) = 0

Tactic:
intro v w h

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)
v w : α
h : s(v, w) ∉ G.edgeSet
⊢ ↑(#{x | s(v, w) ∈ G.incidenceSet x}) = 0
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:
← SimpleGraph.mem_neighborSet

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v
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:
← SimpleGraph.mem_neighborSet

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

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ G.ediam ≤ 2

pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ 2 ≤ G.ediam

Tactic:
· rw [ediam_le_iff]
    intro u v
    by_contra! hc
    obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc
    have h := h.of_not_adj hn ha
    simp_all

Goal state after:
case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ 2 ≤ G.ediam
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' : ℕ
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'
ih : completeEquipartiteGraph r t' ⊑ G
⊢ completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
obtain ⟨K⟩ := completeEquipartiteGraph_isContained_iff.mp ih

Goal state after:
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' : ℕ
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'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
⊢ completeEquipartiteGraph (r + 1) t ⊑ G
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:
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']

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 - ℓ)
Module: Mathlib.Combinatorics.SimpleGraph.Trails

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

Tactic:
rintro rfl rfl

Goal state after:
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
huv : G.Adj v✝ v✝
p : G.Walk v✝ v✝
ih : Even (List.countP (fun e ↦ decide (v✝ ∈ e)) p.edges) ↔ v✝ ≠ v✝ → v✝ ≠ v✝ ∧ v✝ ≠ v✝
ht : p.IsTrail ∧ s(v✝, v✝) ∉ p.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set ↑G.deleteUniversalVerts.verts
⊢ Disjoint (Subtype.val '' s) G.universalVerts

Tactic:
by
  simpa [← Set.disjoint_compl_right_iff_subset, Set.compl_eq_univ_sdiff] using
    Subtype.coe_image_subset _ s

Goal state after: