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:
decreasing_by {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }

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

Goal state before:
pp: V : Type u
⊢ (completeGraph V).Connected ↔ Nonempty V

Tactic:
by simp [connected_iff]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
hc : (pvu.edges ++ puw.edges ++ pwv.edges).Nodup
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False

Tactic:
← Walk.edges_append

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
hc : ((pvu.append puw).edges ++ pwv.edges).Nodup
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
inst✝ : Fintype V
⊢ ⊤.chromaticNumber = ↑(card V)

Tactic:
chromaticNumber_eq_card_iff_forall_surjective (selfColoring _).colorable

Goal state after:
V : Type u
inst✝ : Fintype V
⊢ ∀ (C : ⊤.Coloring V), Surjective ⇑C
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
⊢ G.CliqueFree m

Tactic:
by_contra h

Goal state after:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ¬G.CliqueFree m
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case succ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
⊢ (completeMultipartiteGraph V).Colorable (n + 1 - 1)

Tactic:
have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
  apply (coloring V).colorable.mono
  have := not_cliqueFree_of_le_card V f le_rfl
  contrapose! this
  exact hc.mono this

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.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < ↑2
h' : s = {s(u, w.snd)}
⊢ (G.deleteEdges s).Reachable u w.snd

Tactic:
subst h'
    refine Reachable.trans (h hs) <| w.tail.toDeleteEdge _ (fun hh ↦ ?_) |>.reachable.symm
    have := hw.tail.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hh)
    simp only [Walk.getVert_tail, Nat.reduceAdd] at this
    simpa using hw.getVert_eq_start_iff_of_not_nil (Walk.not_nil_of_ne hne) |>.mp this.symm

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha✝ : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩

Tactic:
obtain rfl | rfl := ha <;> obtain rfl | rfl := hb

Goal state after:
case inl.inl
V : Type u
G : SimpleGraph V
w b : V
hvw : G.Adj b w
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩

case inl.inr
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

case inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

case inr.inr
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ : V
hl : x✝¹ ∈ map { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } univ
x✝ : V
hr : x✝ ∈ map { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } univ
⊢ G.Adj x✝¹ x✝

Tactic:
mem_map

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ : V
hl : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } a = x✝¹
x✝ : V
hr : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } a = x✝
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y ∈ (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯ ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x

Tactic:
simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset,
        mem_neighborSet, Equiv.refl_apply, boxProd_adj]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊔ H ⊔ K).Connected

Tactic:
refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Preconnected

case refine_2
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊓ H).verts.Nonempty

case refine_3
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ ((⊤.induce {u, v} ⊔ H) ⊓ K).verts.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
⊢ c.sumLeft.sum c.sumRight = c

Tactic:
ext (u | u)

Goal state after:
case inl
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : V
⊢ (c.sumLeft.sum c.sumRight) (Sum.inl u) = c (Sum.inl u)

case inr
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : W
⊢ (c.sumLeft.sum c.sumRight) (Sum.inr u) = c (Sum.inr u)
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: u v : Fin 1
⊢ ¬(cycleGraph 1).Adj u v

Tactic:
by
  simp [cycleGraph_one_eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (hasse α).Reachable a b

Tactic:
rw [reachable_iff_reflTransGen]
  exact
    reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax

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

Goal state before:
pp: n : ℕ
h : 0 < n + 3
⊢ (cycleCons n ⟨0, h⟩).length = ↑⟨0, h⟩

Tactic:
unfold cycleGraph.cycleCons
    rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
⊢ ∃ t', t ⊆ t' ∧ (induce (↑t') G).Connected

Tactic:
by
  classical
  obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_ofPred_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_ofPred_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩

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

Goal state before:
pp: case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
show x = y + 1 by grind [Fin.sub_val_of_le]

Goal state after:
case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab✝ : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨y + 1, ⋯⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ mulCayley {1} = ⊥

Tactic:
rw [← mulCayley_erase_one, Set.sdiff_self, mulCayley_empty]

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

Goal state before:
pp: case cons
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u✝ v✝ u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet

Tactic:
obtain ⟨H₁, hH₁, ih⟩ := ih

Goal state after:
case cons
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u✝ v✝ u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (cons h_adj p).edges, e ∈ H.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u v : V
p : (sSup Hs).Walk u v
⊢ ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet

Tactic:
induction p with
  | nil => exact ⟨hHs.some, hHs.some_mem, by simp⟩
  | @cons u v w h_adj p ih =>
    obtain ⟨H₁, hH₁, ih⟩ := ih
    obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
    obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
    simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩

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

Goal state before:
pp: case mpr.refine_2
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
p : G.Walk v w
hp : p.IsPath
q : G.Walk v w
hq : q.IsPath
⊢ ⟨p, hp⟩ = ⟨q, hq⟩

Tactic:
simp only [ExistsUnique.unique (h v w) hp hq]

Goal state after:
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
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

Tactic:
intro a ha b hb h

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : ((f a).firstDart ⋯).edge = ((f b).firstDart ⋯).edge
⊢ a = b
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

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

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

Tactic:
· grind [sup_eq_left, edge_le, Sym2.mem_diagSet, Sym2.mk_isDiag_iff]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬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 : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
intro cf

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : 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 : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
intro cf

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj v w

Tactic:
refine ⟨_, p.adj_penultimate hnil |>.symm, fun w hadj ↦ ?_⟩

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
w : V
hadj : (fun w ↦ G.Adj v w) w
⊢ w = p.penultimate
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' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
intro cf

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
cf : 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
⊢ h.finpartition.IsEquipartition

Tactic:
by
  set fp := h.finpartition
  by_contra hn
  rw [Finpartition.not_isEquipartition] at hn
  obtain ⟨large, hl, small, hs, ineq⟩ := hn
  obtain ⟨w, hw⟩ := fp.nonempty_of_mem_parts hl
  obtain ⟨v, hv⟩ := fp.nonempty_of_mem_parts hs
  apply absurd h
  rw [IsTuranMaximal, IsExtremal]; push Not; intro cf
  use G.replaceVertex v w, inferInstance, cf.replaceVertex v w
  have large_eq := fp.part_eq_of_mem hl hw
  have small_eq := fp.part_eq_of_mem hs hv
  have ha : G.Adj v w := by
    by_contra hn; rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn
    rw [hn] at ineq; lia
  rw [G.card_edgeFinset_replaceVertex_of_adj ha,
    degree_eq_card_sub_part_card h, small_eq, degree_eq_card_sub_part_card h, large_eq]
  have : #large ≤ card V := by simpa using card_le_card large.subset_univ
  lia

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ n ≥ 3, (cycleGraph n).Free G
v : V
p : G.Walk v v
hcyc : p.IsCycle
⊢ cycleGraph p.length ⊑ G

Tactic:
exact cycleGraph_isContained_iff hcyc.three_le_length |>.mpr ⟨v, p, hcyc, rfl⟩

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

Goal state before:
pp: case pos
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : t = 0
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
exact ⟨∅, .inr ht, by simp, by simp⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.radius = 0 ↔ Nonempty α ∧ Subsingleton α

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
  · contrapose! h
    simp [radius]
  · contrapose! h
    simp [radius_ne_zero_of_nontrivial]
  · rw [radius, ENat.iInf_eq_zero]
    use Classical.ofNonempty
    simpa [eccent] using Subsingleton.elim _

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

Goal state before:
pp: case inr.inr.e_a
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
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2

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

Goal state after:
case inr.inr.e_a
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
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
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
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : ⨅ a, ⨅ w, ⨅ (_ : w.IsCycle), ↑w.length ≠ ⊤
⊢ ∃ a w, w.IsCycle ∧ ⨅ a, ⨅ w, ⨅ (_ : w.IsCycle), ↑w.length = ↑w.length

Tactic:
iInf_subtype',

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
h : ⨅ a, ⨅ x, ↑(↑x).length ≠ ⊤
⊢ ∃ a w, w.IsCycle ∧ ⨅ a, ⨅ x, ↑(↑x).length = ↑w.length
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

pp: case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
· exact hs.exists_union_disjoint_cardinal_eq_of_infinite

Goal state after:
case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
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:
simpa using finite_univ.ncard_biUnion_le s

Goal state after:
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).PosSemidef

Tactic:
refine .of_dotProduct_mulVec_nonneg ?_ (fun x ↦ ?_)
  · rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]
  · rw [star_trivial, ← toLinearMap₂'_apply', lapMatrix_toLinearMap₂']
    positivity

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 ℓ μ
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Tactic:
exact h.regular.compl

Goal state after: