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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
by
  have : DecidableEq ι := by
    classical
    infer_instance
  obtain hs | hs := le_total (Fintype.card α) #s
  · rw [tsub_eq_zero_of_le hs, pow_zero]
    refine (card_le_card <| biUnion_subset.2 fun i hi a ha ↦
      mem_compl.2 <| notMem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq ?_
    rw [card_compl, Fintype.card_finset, card_singleton]
  induction s using Finset.cons_induction generalizing f with
  | empty => simp
  | cons i s hi ih =>
  set f' : ι → Finset (Finset α) :=
    fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
  have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) =
      2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
    rintro j hj
    simp_rw [f', dif_pos hj, ← Fintype.card_finset]
    exact Classical.choose_spec (hf j hj).exists_card_eq
  have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) := by
    refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)
    rw [Fintype.card_finset]
    exact (hf₁ _ hj).2.1
  refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
  nth_rw 1 [cons_eq_insert i]
  rw [biUnion_insert]
  refine (card_mono <| @le_sup_sdiff _ _ (f' i) _).trans ((card_union_le _ _).trans ?_)
  rw [union_sdiff_left, sdiff_eq_inter_compl]
  refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
  rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
  refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
  · rw [coe_biUnion]
    exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
  · rw [coe_compl]
    exact (hf₂ _ <| mem_cons_self _ _).compl
  rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]
  gcongr
  refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_
  rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∉ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + 0) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [add_zero, add_mul]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ s * f₂ t + f₁ (insert a s) * f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
by
  have : 0 < ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0) :=
    Nat.cast_pos.2 <| choose_pos (Nat.div_le_self _ _)
  have h := calc
    ∑ s ∈ 𝒜, ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0)⁻¹
    _ ≤ ∑ s ∈ 𝒜, ((Fintype.card α).choose #s : ℚ≥0)⁻¹ := by
      gcongr with s hs
      · exact mod_cast choose_pos s.card_le_univ
      · exact choose_le_middle _ _
    _ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_inv_choose h𝒜
  simpa [mul_inv_le_iff₀' this] using h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Reachable = Relation.ReflTransGen G.Adj

Tactic:
ext
  exact reachable_iff_reflTransGen ..

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
s : Set V
x✝ : Maximal (fun x ↦ (induce x G).Connected) s
hconn : (fun x ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun x ↦ (induce x G).Connected) y → s ⊆ y → y ⊆ s
v : V
hv : v ∈ s
⊢ ∃ C, C.supp = s

Tactic:
suffices s ≤ (G.connectedComponentMk v).supp from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSimpleGraph _) this) this⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
s : Set V
x✝ : Maximal (fun x ↦ (induce x G).Connected) s
hconn : (fun x ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun x ↦ (induce x G).Connected) y → s ⊆ y → y ⊆ s
v : V
hv : v ∈ s
⊢ s ⊆ (G.connectedComponentMk v).supp
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
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) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i) → B ⊆ range'k ∧ #B = r - i

Tactic:
rintro ⟨A, Ah, hBA, card_sdiff_i⟩
        rw [mem_powersetCard] at Ah
        refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
        rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ s(v, w) ∉ List.map (Sym2.map ⇑(Hom.ofLE ⋯)) p.edges

Tactic:
List.mem_map,

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ ¬∃ a ∈ p.edges, Sym2.map (⇑(Hom.ofLE ⋯)) a = s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

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

Tactic:
rw [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.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v = {w ∈ t | G.Adj v w}

Tactic:
ext w
  rw [mem_neighborFinset, mem_filter, iff_and_self]
  exact h.mem_of_mem_adj hv

Goal state after:
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✝¹ x✝ : V
w✝¹ : α
left✝¹ : w✝¹ ∈ univ
hl : { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹ = x✝¹
w✝ : β
left✝ : w✝ ∈ univ
hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝ = x✝
⊢ G.Adj x✝¹ x✝

Tactic:
← hl,

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✝¹ x✝ : V
w✝¹ : α
left✝¹ : w✝¹ ∈ univ
hl : { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹ = x✝¹
w✝ : β
left✝ : w✝ ∈ univ
hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝ = x✝
⊢ G.Adj ({ toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹) x✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj u w.snd

Tactic:
simpa using w.toSubgraph_adj_getVert (not_nil_iff_lt_length.mp h)

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ ((fun x ↦ s(Sum.inl x.1, Sum.inr x.2)) '' Set.univ).encard = Set.univ.encard

Tactic:
exact Function.Injective.encard_image (by grind [Function.Injective]) Set.univ

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
⊢ ¬1 = G.dist u v

Tactic:
by
    by_contra hc
    obtain ⟨p, hp⟩ := Reachable.exists_walk_length_eq_dist h
    exact hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩)

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : ¬G.Reachable u w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
grind [dist_eq_zero_iff_eq_or_not_reachable]

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : ¬G.Reachable u w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
grind [dist_eq_zero_iff_eq_or_not_reachable]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
⊢ p.snd = v'

Tactic:
rcases hi.1 with ⟨hl1, rfl⟩ | ⟨hr1, hr2⟩

Goal state after:
case inl
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ p.snd = p.getVert (i + 1)

case inr
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ p.snd = v'
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
⊢ p.snd = v'

Tactic:
by
  have ⟨i, hi⟩ := p.toSubgraph_adj_iff.mp hadj
  simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hi
  rcases hi.1 with ⟨hl1, rfl⟩ | ⟨hr1, hr2⟩
  · have : i = 0 := by
      apply hp.getVert_injOn (by rw [Set.mem_ofPred]; lia) (by rw [Set.mem_ofPred]; lia)
      rw [p.getVert_zero, hl1]
    simp [this]
  · have : i + 1 = 0 := by
      apply hp.getVert_injOn (by rw [Set.mem_ofPred]; lia) (by rw [Set.mem_ofPred]; lia)
      rw [p.getVert_zero, hr2]
    contradiction

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    1 + w'.ofBoxProdLeft.length +
      (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
add_assoc

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    1 +
      (w'.ofBoxProdLeft.length +
        (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case top
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
hG : G.chromaticNumber ≤ ⊤
hH : H.chromaticNumber ≤ ⊤
⊢ (G ⊕g H).chromaticNumber ≤ ⊤

Tactic:
| top =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
S : Set (Set V)
Sn : S.Nonempty
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
⊢ (induce (⋃₀ S) G).Connected

Tactic:
obtain ⟨s, sS⟩ := Sn

Goal state after:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
⊢ (induce (⋃₀ S) G).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
⊢ ⊤ = G.Reachable

Tactic:
G.preconnected_iff_reachable_eq_top.mp hG.preconnected

Goal state after:
case refine_2
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
hT' : T.IsTree
⊢ ⊤ = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
⊢ ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsTree

Tactic:
obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic hH_le hH_isAcyclic

Goal state after:
V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
F : SimpleGraph V
hF : H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
⊢ ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsTree
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
v : V
⊢ (G.replaceVertex s t).Adj s v ↔ G.Adj s v

Tactic:
by_cases eq : v = t

Goal state after:
case pos
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
v : V
eq : v = t
⊢ (G.replaceVertex s t).Adj s v ↔ G.Adj s v

case neg
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
v : V
eq : ¬v = t
⊢ (G.replaceVertex s t).Adj s v ↔ G.Adj s v
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
k : K
⊢ C.labelGraph k ≤ G

Tactic:
intro x y
  grind [labelGraph_adj]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ Injective fun x ↦
    match x with
    | 0 => w₁
    | 1 => v
    | 2 => w₂

Tactic:
intro _ _ _
    have := h.ne_fst
    have := h.ne_snd
    have := h.adj.ne
    aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Preconnected ∧ Nonempty V

Tactic:
← Finset.univ_nonempty_iff

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Preconnected ∧ univ.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
        ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
          ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0)) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
add_assoc

Goal state after:
n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
        ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
          ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0)) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + (2 * (n * (r - 1)) + 2 * r.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ (G.edist u v).toNat = G.ediam.toNat

Tactic:
congrArg ENat.toNat huv

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.diam = 0
u v : α
huv : G.edist u v = G.ediam
⊢ G.ediam.toNat = G.ediam.toNat
Module: Mathlib.Combinatorics.SimpleGraph.Diam

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

Tactic:
by
  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.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.center = Set.univ ↔ G.radius = G.ediam

Tactic:
radius_eq_ediam_iff,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.center = Set.univ ↔ ∃ e, ∀ (u : α), G.eccent u = e
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ (#K'.parts).pred = r ∨ t = 0

Tactic:
K'.card_parts.resolve_right ht

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ (r + 1).pred = r ∨ t = 0
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ r + 1 = #K'.parts

Tactic:
K'.card_parts.resolve_right ht

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ r + 1 = r + 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| #({v_1 ∈ K.verts | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < #K.verts - t' + t

Tactic:
enter [1, 1, 2]

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| K.verts
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝ : v ∈ p
h : f ⟨v, h✝⟩ = w
⊢ G.Adj v w

pp: case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ G.Adj v w

Tactic:
· exact h ▸ h₂ ⟨v, by assumption⟩

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : 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))
⊢ False

Tactic:
have h := C.surjOn_of_card_le_isClique hw.isNClique_fst_left.1 (by simp [hw.isNClique_fst_left.2])

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
⊢ ↑t < ↑r * ↑t' * ε

Tactic:
rw [mul_comm (r : ℝ) (t' : ℝ), mul_assoc, ← div_lt_iff₀ (by positivity), Nat.cast_add_one]

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
⊢ ↑t / (↑r * ε) < ↑⌊↑t / (↑r * ε)⌋₊ + 1
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✝ : NonAssocRing R
i : V
⊢ (lapMatrix R G *ᵥ fun x ↦ 1) i = 0 i

Tactic:
rw [lapMatrix_mulVec_apply]

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✝ : NonAssocRing R
i : V
⊢ ↑(G.degree i) * 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i