mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ 2 ^ Fintype.card α - #{⊥} = 2 ^ Fintype.card α - 1

Tactic:
card_singleton

Goal state after:
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ 2 ^ Fintype.card α - 1 = 2 ^ Fintype.card α - 1
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
refine (ih ?_ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans

Goal state after:
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ #t ≤ Fintype.card α / 2
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #𝒜 ≤ #𝒜.shatterer

Tactic:
refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
  · simp
  · rfl
  intro a 𝒜 ih₀ ih₁
  set ℬ : Finset (Finset α) :=
    ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).image (insert a)
  have hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) := by
    refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_
    simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_ofPred_eq, and_imp,
      mem_shatterer]
    exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)
  rw [← card_memberSubfamily_add_card_nonMemberSubfamily a]
  refine (Nat.add_le_add ih₁ ih₀).trans ?_
  rw [← card_union_add_card_inter, ← hℬ, ← card_union_of_disjoint]
  swap
  · simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]
    rintro _ (hs | hs) s - rfl
    · exact aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _
    · exact aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _
  refine card_mono <| union_subset (union_subset ?_ <| shatterer_mono <| filter_subset _ _) ?_
  · simp only [subset_iff, mem_shatterer]
    rintro s hs t ht
    obtain ⟨u, hu, rfl⟩ := hs ht
    rw [mem_memberSubfamily] at hu
    refine ⟨insert a u, hu.1, inter_insert_of_notMem fun ha ↦ ?_⟩
    obtain ⟨v, hv, hsv⟩ := hs.exists_inter_eq_singleton ha
    rw [mem_memberSubfamily] at hv
    rw [← singleton_subset_iff (a := a), ← hsv] at hv
    exact hv.2 inter_subset_right
  · refine forall_mem_image.2 fun s hs ↦ mem_shatterer.2 fun t ht ↦ ?_
    simp only [mem_inter, mem_shatterer] at hs
    rw [subset_insert_iff] at ht
    by_cases ha : a ∈ t
    · obtain ⟨u, hu, hsu⟩ := hs.1 ht
      rw [mem_memberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rw [← insert_inter_distrib, hsu, insert_erase ha]
    · obtain ⟨u, hu, hsu⟩ := hs.2 ht
      rw [mem_nonMemberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rwa [insert_inter_of_notMem hu.2, hsu, erase_eq_self]

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

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ u ∈ 𝒜
ha✝ : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
ha : a ∈ s ∩ u
⊢ False

Tactic:
exact hu.1 hu.2

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

Goal state before:
pp: V : Type u
inst✝¹ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ 0 < G.degree v

Tactic:
simp [degree_pos_iff_mem_support, h.support_eq_univ]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ (¬∃ v, ∀ (w : V), G.Reachable v w) → Gᶜ.Preconnected

Tactic:
intro h u v

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : ∀ (v : V), ∃ w, ¬G.Reachable v w
⊢ Gᶜ.Reachable u v

Tactic:
have ⟨w, huw⟩ := h u

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

Goal state before:
pp: case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)

Tactic:
ConnectedComponent.connectedComponentMk_eq_of_adj hab

Goal state after:
case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk b✝).toSimpleGraph.Adj →r H.Adj)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

Tactic:
ConnectedComponent.connectedComponentMk_eq_of_adj hab

Goal state after:
case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk b✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk a✝).toSimpleGraph.Adj

Tactic:
ConnectedComponent.connectedComponentMk_eq_of_adj hab

Goal state after:
case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk b✝).toSimpleGraph.Adj
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case refine_1
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ #𝒞 ≤ #𝒜

pp: case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → toColex t < toColex s ∧ #t = r → t ∈ 𝒞

Tactic:
· rwa [card_powersetCard, card_attachFin, card_range]

Goal state after:
case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → toColex t < toColex s ∧ #t = r → t ∈ 𝒞
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk a✝

Tactic:
ConnectedComponent.connectedComponentMk_eq_of_adj hab

Goal state after:
case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk b✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

Tactic:
ConnectedComponent.connectedComponentMk_eq_of_adj hab

Goal state after:
case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk b✝
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ) (a : G.Coloring (Fin m)), n ≤ m

Tactic:
simp [le_chromaticNumber_iff_colorable, Colorable]

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

Goal state before:
pp: ι : Type u_4
V : ι → Type u_5
inst✝ : Fintype ι
f : (i : ι) → V i
⊢ (completeMultipartiteGraph V).chromaticNumber = ↑(card ι)

Tactic:
by
  apply le_antisymm (colorable V).chromaticNumber_le
  by_contra! h
  exact not_cliqueFree_of_le_card V f le_rfl <| cliqueFree_of_chromaticNumber_lt h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k l : ℕ
u v : V
hkl : k ≤ l
h : G.IsEdgeReachable l u v
x✝ : Set (Sym2 V)
hk : x✝.encard < ↑k
⊢ x✝.encard < ↑l

Tactic:
by grw [← hkl]; exact hk

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
s₁ s₂ : α ⊕ β
⊢ Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁ = Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂ → s₁ = s₂

Tactic:
match s₁, s₂ with
    | .inl p₁, .inl p₂ => simp
    | .inr p₁, .inl p₂ =>
      simpa using (h (fα p₂).prop (fβ p₁).prop).ne'
    | .inl p₁, .inr p₂ =>
      simpa using (h (fα p₁).prop (fβ p₂).prop).symm.ne'
    | .inr p₁, .inr p₂ => simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ G.dist u v = 0 ↔ u = v

Tactic:
simp [hr]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ G.Connected

Tactic:
have := (nonempty_prod.1 h.nonempty).2

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ G.Connected
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ H.Connected

Tactic:
have := (nonempty_prod.1 h.nonempty).2

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ H.Connected
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
  use x, hxs, hx
  suffices {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x} by simpa [Finset.subset_iff] using this
  rwa [Finset.filter_erase, ← Finset.subset_empty, ← Finset.subset_insert_iff,
    LawfulSingleton.insert_empty_eq] at h

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

Goal state before:
pp: case inr.inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

Tactic:
exact ((hG ..).sum_sup_edge (hH ..)).symm

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

Goal state before:
pp: n : ℕ
v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}

Tactic:
ext w
  simp only [mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]
  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.CycleGraph

Goal state before:
pp: case refine_2.refine_2
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
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
wlog hle : x > y

Goal state after:
case refine_2.refine_2.inr
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
this :
  ∀ {V : Type u_1} {G : SimpleGraph V} {n : ℕ},
    2 < n →
      ∀ (a : V) (p : G.Walk a a),
        p.IsCycle →
          ∀ (hp₂ : p.length = n) (x : ℕ) (hx : x < n) (y : ℕ) (hy : y < n),
            (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩ → x ≠ y → x > y → G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
hle : ¬x > y
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

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
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

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

Tactic:
simp [← coe_finsetWalkLength_eq]

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

Goal state before:
pp: n r : ℕ
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

Tactic:
by
  simp_rw [SimpleGraph.ext_iff, funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not]
  refine ⟨fun h ↦ ?_, ?_⟩
  · contrapose! h
    use ⟨0, (Nat.pos_of_ne_zero h.1).trans h.2⟩, ⟨r, h.2⟩
    simp [h.1.symm]
  · rintro (rfl | h) a b
    · simp [Fin.val_inj]
    · rw [Nat.mod_eq_of_lt (a.2.trans_le h), Nat.mod_eq_of_lt (b.2.trans_le h), Fin.val_inj]

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
⊢ e ∈ (F ⊔ fromEdgeSet {e}).edgeSet

Tactic:
simp [H.not_isDiag_of_mem_edgeSet heH]

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

Goal state before:
pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ¬↑v = n + 2 - 1
⊢ 2 ≠ ⟨↑v % 2, ⋯⟩

Tactic:
refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val (?_))).symm

Goal state after:
case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ¬↑v = n + 2 - 1
⊢ ↑v % 2 < ↑2
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : ∑ v, 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1

Tactic:
Finset.sum_const,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : Finset.univ.card • 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail

Tactic:
have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : 1 ≤ List.count (pwz.getVert (pwz.length - 1)) pwz.support
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ a✝ ∈ h.finpartition.part s

Tactic:
convert! Finpartition.mem_part_ofSetoid_iff_rel.symm

Goal state after:
case e'_1
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ h.setoid s a✝
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
hn : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a
⊢ False

Tactic:
obtain ⟨large, hl, small, hs, ineq⟩ := hn

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
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ G.IsPathGraph3Compl v w₂ w₁

Tactic:
by
  obtain ⟨h1, h2, h3⟩ := h
  exact ⟨h1.symm, h3, h2⟩

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1 = ↑v.1

Tactic:
enter [1, 1, 1, 1, 1]
        rw [Nat.mul_add_mod_self_right]

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| ↑v.1 % r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
hr : r = 0
⊢ #∅ = r ∨ t = 0

Tactic:
simp [hr]

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

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

Tactic:
intro h v huv

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⨆ p, G.edist p.1 p.2

Tactic:
rw [ediam, eccent_def, iSup_prod]

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

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊤.center = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]
    intro u
    rw [mem_center_iff, eccent_top, radius_top]

Goal state after: