mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
GL : β → α → α → Prop
GE : Set β
isLink_symm✝¹ : ∀ ⦃e : β⦄, e ∈ GE → Std.Symm (GL e)
eq_or_eq_of_isLink_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, GL e x y → GL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝¹ : ∀ (e : β), e ∈ GE ↔ ∃ x y, GL e x y
HV : Set α
HL : β → α → α → Prop
HE : Set β
isLink_symm✝ : ∀ ⦃e : β⦄, e ∈ HE → Std.Symm (HL e)
eq_or_eq_of_isLink_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, HL e x y → HL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝ : ∀ (e : β), e ∈ HE ↔ ∃ x y, HL e x y
left_mem_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y : α⦄, HL e x y → x ∈ HV
left_mem_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y : α⦄, GL e x y → x ∈ HV
u v :
  ↑V({ vertexSet := HV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝ })
hadj✝ :
  { vertexSet := HV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
          eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
          edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹,
          left_mem_of_isLink := left_mem_of_isLink✝ }.toSimpleGraph.Adj
    u v
hne : u ≠ v
hadj :
  { vertexSet := HV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝ }.Adj
    ↑u ↑v
hle :
  { vertexSet := HV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹,
        left_mem_of_isLink := left_mem_of_isLink✝ }.IsSubgraph
    { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝, left_mem_of_isLink := left_mem_of_isLink✝¹ }
⊢ (⋯ ▸
        { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
            edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝,
            left_mem_of_isLink := left_mem_of_isLink✝¹ }.toSimpleGraph).Adj
    u v

Tactic:
simp [toSimpleGraph_adj, hne, hadj.mono hle]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ (M✶ ＼ I).coloops

Tactic:
← dual_contract,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ (M ／ I)✶.coloops
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
⊢ ⟨i, e⟩ ∉ B₂ →
    ∃ a b, (⟨a, b⟩ ∈ B₂ ∧ ⟨a, b⟩ ∉ B₁) ∧ ∀ (i_1 : ι), (M i_1).IsBase (Sigma.mk i_1 ⁻¹' insert ⟨a, b⟩ (B₁ \ {⟨i, e⟩}))

Tactic:
he₂

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
⊢ ∃ a b, (⟨a, b⟩ ∈ B₂ ∧ ⟨a, b⟩ ∉ B₁) ∧ ∀ (i_1 : ι), (M i_1).IsBase (Sigma.mk i_1 ⁻¹' insert ⟨a, b⟩ (B₁ \ {⟨i, e⟩}))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α), ∀ C ⊆ M.E, M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)

Tactic:
← closure_inter_ground,

Goal state after:
case inr
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α), ∀ C ⊆ M.E, M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
⊢ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X (C ∩ M.E) ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C

Tactic:
and_congr_right_iff

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
⊢ M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b c : V
p : Path a b
e : b ⟶ c
x : V
⊢ x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c

Tactic:
simp only [vertices_cons]
  simp_all only [concat_eq_append, mem_append, mem_cons, not_mem_nil, or_false]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p 𝒜

Tactic:
set u := 𝒜.sup id
  have hu : ∀ s ∈ 𝒜, s ⊆ u := fun s ↦ le_sup (f := id)
  clear_value u
  induction u using Finset.induction generalizing 𝒜 with
  | empty =>
    simp_rw [subset_empty] at hu
    rw [← subset_singleton_iff', subset_singleton_iff] at hu
    obtain rfl | rfl := hu <;> assumption
  | insert a u _ ih =>
    refine subfamily a (ih _ ?_) (ih _ ?_)
    · simp only [mem_nonMemberSubfamily, and_imp]
      exact fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs
    · simp only [mem_memberSubfamily, and_imp]
      exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

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

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁ : i ∈ range (n + 1)
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
rw [mem_range] at h₁

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁ : i < n + 1
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ s ∩ u ∪ t ∩ u = u

Tactic:
rwa [← union_inter_distrib_right, inter_eq_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∈ upperClosure ↑t
⊢ (s ∪ t).truncatedInf a = t.truncatedInf a

Tactic:
rw [union_comm, truncatedInf_union_left ht hs]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
a : α
ha : a ∈ ↑s
has : ∀ ⦃y : α⦄, (fun x ↦ x ∈ ↑s) y → y ≤ a → a ≤ y
⊢ ∃ a, Ici a = s

Tactic:
exact ⟨a, (hs.2 <| erase_inf_Ici ha fun b hb ↦ le_imp_eq_iff_le_imp_ge.2 <| has hb).resolve_left
      (lt_erase.2 ha).ne'⟩

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s

Tactic:
rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ s, ↑(#(𝒜ᶜˢ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
rw [← @map_univ_of_surjective (Finset α) _ _ _ ⟨compl, compl_injective⟩ compl_surjective, sum_map]

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ x,
        ↑(#(𝒜ᶜˢ.truncatedInf ({ toFun := compl, inj' := ⋯ } x))) /
          (↑(#({ toFun := compl, inj' := ⋯ } x)) * ↑((card α).choose #({ toFun := compl, inj' := ⋯ } x))) +
      ∑ s ∈ map { toFun := compl, inj' := ⋯ } univ,
        ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs)) →
    ∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s

Tactic:
le_iff_eq_or_lt,

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      (toColex t = toColex (s.erase (s.min' hs)) ∨ toColex t < toColex (s.erase (s.min' hs))) →
    ∃ a ∉ t, #s = #(insert a t) ∧ (toColex (insert a t) = toColex s ∨ toColex (insert a t) < toColex s)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (V.erase (V.min' hV)).Nonempty

pp: case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).max' ⋯ < (V.erase (V.min' hV)).max' ?inr.refine_3

Tactic:
· rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]

Goal state after:
case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).max' ⋯ < (V.erase (V.min' hV)).max' ⋯
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x : α
⊢ {y | (mkClasses c H) x y} ∈ c

Tactic:
convert! @Setoid.eqv_class_mem _ _ H x using 3

Goal state after:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x x✝ : α
⊢ (mkClasses c H) x x✝ ↔ (mkClasses c H) x✝ x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ p, p.IsPath

Tactic:
classical
  obtain ⟨W⟩ := hr
  exact ⟨_, Path.isPath W.toPath⟩

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w

Tactic:
· exact hadj

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : a ∈ i✝.supp
⊢ a ∉ j✝.supp

Tactic:
hsy

Goal state after:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : a ∈ i✝.supp
hsy : a ∈ j✝.supp
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
⊢ ∃ u, G.Adj v u

Tactic:
have ⟨u, huv⟩ := exists_ne v

Goal state after:
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v u : V
huv : u ≠ v
⊢ ∃ u, G.Adj v u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).Connected

Tactic:
refine ⟨⟨?_⟩⟩

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).coe.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ G.edist u v = ⊤

Tactic:
by
  simp [edist, not_reachable_iff_isEmpty_walk.mp h]

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

Goal state before:
pp: case right
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
this : ¬G.Adj u v
hc : (G.commonNeighbors u v).Nonempty
⊢ False

Tactic:
simp [edist_eq_two_iff.mpr ⟨hn, this, hc⟩] at h

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 2 ≤ G.edist u v

pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ G.edist u v ≠ 2

Tactic:
· have hn : u ≠ v := fun hc ↦ by simp [hc] at h
    have : ¬ G.Adj u v := fun hc ↦ by simp +decide [edist_eq_one_iff_adj.mpr hc] at h
    use hn, this
    by_contra! hc
    simp [edist_eq_two_iff.mpr ⟨hn, this, hc⟩] at h

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 2 ≤ G.edist u v

case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ G.edist u v ≠ 2
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 2 = insert c (G.neighborSet c)

Tactic:
by
  ext v
  simp [one_add_one_eq_two.symm, ENat.lt_add_one_iff ENat.one_ne_top,
    edist_le_one_iff_adj_or_eq, adj_comm, or_comm]

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'⟩
⊢ ∀ (w : ↑s), (induce s G).Reachable ⟨u, hu⟩ w

Tactic:
rintro ⟨v, hv⟩

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'⟩
v : V
hv : v ∈ s
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
⊢ pathGraph n ≤ cycleGraph n

Tactic:
by
  match n with
  | 0 | 1 => simp
  | n + 2 =>
    intro u v h
    rw [pathGraph_adj] at h
    rw [cycleGraph_adj']
    cases h with
    | inl h | inr h =>
      simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
⊢ GaloisConnection (fun x ↦ mulCayley x) fun x ↦ {g | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a}

Tactic:
intro S

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set M
⊢ ∀ (b : SimpleGraph M), (fun x ↦ mulCayley x) S ≤ b ↔ S ⊆ (fun x ↦ {g | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a}) b
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
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ (G.replaceVertex s t).degree u = G.degree u - 1

Tactic:
rw [degree, degree, ← card_singleton t, ← card_sdiff_of_subset (by simp [h.symm])]

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)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ #((G.replaceVertex s t).neighborFinset u) = #(G.neighborFinset u \ {t})
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Pairwise fun k l ↦ Disjoint (C.labelGraph k) (C.labelGraph l)

Tactic:
by
  intro _ _ h
  rw [disjoint_left]
  grind [labelGraph_adj]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α}, ¬h.setoid a b ↔ G.Adj a b

Tactic:
intros

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
a✝ b✝ : α
⊢ ¬h.setoid a✝ b✝ ↔ G.Adj a✝ b✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
| n * (r - 1)

Tactic:
← card_range n,

Goal state after:
n r : ℕ
| #(range n) * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
⊢ completeEquipartiteGraph (r + 1) t ⊑ G ↔ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Tactic:
rw [completeEquipartiteGraph_isContained_iff]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t) ↔ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ K ∩ ↑C ⊆ ∅

Tactic:
exact fun v ⟨vK, vC⟩ => vC.choose vK

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ (↑n - 1) * ↑n / 2 * ↑(#G.edgeFinset) ≤ (↑n + 1) * ↑n / 2 * ↑(extremalNumber n H)

Tactic:
← mul_div (n - 1 : ℝ),

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ (↑n - 1) * (↑n / 2) * ↑(#G.edgeFinset) ≤ (↑n + 1) * ↑n / 2 * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl.inr
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hcy : C y = C v
hx : x = w₁
hy : y ∈ ↑t
⊢ False

Tactic:
apply (C.valid _ hcy.symm).elim

Goal state after:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hcy : C y = C v
hx : x = w₁
hy : y ∈ ↑t
⊢ G.Adj v y
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]

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) =
    (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj (p.getVert n) v

Tactic:
Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ G.Adj (p.getVert n) v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y _x →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
v : V
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, p✝⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun x1 x2 ↦ x1 < x2)
        (fun x ↦ PSigma.casesOn x fun v p ↦ PSigma.casesOn p fun p hp ↦ Nat.card V + 1 - p.length) y ⟨v, ⟨p, hp⟩⟩ →
      (G \ y.2.1.toSubgraph.spanningCoe).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left✝ : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length

Tactic:
decreasing_by
  have := Fintype.ofFinite V
  simp_wf
  have := Walk.IsPath.length_lt hp
  lia

Goal state after: