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

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
⊢ ∑ x ∈ 𝒜 with compress U V x ∈ 𝒜, ∑ a ∈ x, 2 ^ ↑a + ∑ x ∈ image (compress U V) 𝒜 with x ∉ 𝒜, ∑ a ∈ x, 2 ^ ↑a <
    ∑ A ∈ {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, ∑ a ∈ A, 2 ^ ↑a

Tactic:
sum_union (disjoint_filter_filter_not _ _ _),

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
⊢ ∑ x ∈ 𝒜 with compress U V x ∈ 𝒜, ∑ a ∈ x, 2 ^ ↑a + ∑ x ∈ image (compress U V) 𝒜 with x ∉ 𝒜, ∑ a ∈ x, 2 ^ ↑a <
    ∑ x ∈ 𝒜 with compress U V x ∈ 𝒜, ∑ a ∈ x, 2 ^ ↑a + ∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ x, 2 ^ ↑a
Module: Mathlib.Combinatorics.SetFamily.Shatter

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

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
· obtain ⟨v, hv, hsv⟩ := hs <| insert_subset ha ht
    rw [Down.mem_compression] at hv
    obtain hv | hv := hv
    · refine ⟨erase v a, hv.2, ?_⟩
      rw [inter_erase, hsv, erase_insert]
      rintro ha
      rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu
      exact hu.1 hu.2
    rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv
    cases hv.1 hv.2
    rw [hsv]
    exact mem_insert_self _ _

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[k] 𝒞) ≤ #(∂^[k] 𝒜)

Tactic:
induction k generalizing r 𝒜 𝒞 with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hv : v ∈ Subtype.val '' ↑c
hw : w ∈ H.verts
hadj : H.Adj v w
⊢ w ∈ Subtype.val '' ↑c

Tactic:
obtain ⟨_, h⟩ := hv

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ w ∈ Subtype.val '' ↑c
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
⊢ x ∈ range (hs.piecewise f) → x ∈ ⋃ i, f i '' s i

pp: case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
x✝ : x ∈ ⋃ i, f i '' s i
t : Set β
i : ι
hi : (fun i ↦ f i '' s i) i = t
ht : x ∈ t
⊢ x ∈ range (hs.piecewise f)

Tactic:
· rintro ⟨x, rfl⟩
    exact mem_iUnion_of_mem (hs.index x) ⟨x, hs.mem_index x, rfl⟩

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
x✝ : x ∈ ⋃ i, f i '' s i
t : Set β
i : ι
hi : (fun i ↦ f i '' s i) i = t
ht : x ∈ t
⊢ x ∈ range (hs.piecewise f)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : 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 ∩ t) * f₄ (insert a s ∪ insert a t) + f₃ (insert a (s ∩ t)) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
← add_mul

Goal state after:
case pos
α : 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 ∩ t) + f₃ (insert a (s ∩ t))) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
inst✝ : Infinite V
hc : ¬⊤.chromaticNumber = ⊤
⊢ False

Tactic:
rw [← Ne, chromaticNumber_ne_top_iff_exists] at hc

Goal state after:
V : Type u_4
inst✝ : Infinite V
hc : ∃ n, ⊤.Colorable n
⊢ False
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case calc_2.e_a.e_s.e_a.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
⊢ insert a (s.erase a) = s

Tactic:
rw [insert_erase (erase_ne_self.1 fun hs ↦ ?_)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr
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)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₁.getRight hs₁)))
    (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)

Tactic:
← Sum.inl_getLeft s₂ hs₂,

Goal state after:
case inr
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)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr (s₁.getRight hs₁)))
    (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl (s₂.getLeft hs₂)))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges

Tactic:
rw [← mem_edges_toSubgraph, Subgraph.mem_edgeSet]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i' ∈ {i | i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i ∈ {i | i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ∈ {i | i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ∈ {i | i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 ∈ {i | i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ∈ {i | i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ∈ {i | i ≤ p.length - 1}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i ∈ {i | i ≤ p.length - 1}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ i ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ G.subgraphOfAdj ha ≤ ⊤.induce (s ∪ t)

Tactic:
apply subgraphOfAdj_le_of_adj

Goal state after:
case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n m : ℕ
h : m + 1 < n + 3
⊢ (cycleGraph (n + 3)).Adj ⟨m + 1, h⟩ ⟨m, ⋯⟩

Tactic:
by
      simp [cycleGraph_adj, Fin.ext_iff, Fin.sub_val_of_le]

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

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

Tactic:
let q := (hc v w).some.toPath

Goal state after:
case mp
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v w : V
q : G.Path v w := (Nonempty.some ⋯).toPath
⊢ ∃! p, p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
⊢ w = x

Tactic:
have := mw.2.symm.trans mx.2

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : n + w ≡ n + x [MOD r]
⊢ w = x
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h✝ : IsEmpty α
⊢ G.ediam ≤ 2 * G.radius

Tactic:
radius_eq_top_of_isEmpty

Goal state after:
case inl
α : Type u_1
G : SimpleGraph α
h✝ : IsEmpty α
⊢ G.ediam ≤ 2 * ⊤
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ #(cons s K.parts ⋯) = r + 1 ∨ t = 0

Tactic:
Finset.card_cons,

Goal state after:
case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ #K.parts + 1 = r + 1 ∨ t = 0
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
⊢ Finite (G.ComponentCompl ↑K)

Tactic:
let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
      let p := C.exists_adj_boundary_pair Gpc.out h
      ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩

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

Goal state before:
pp: n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)

pp: n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2

Tactic:
· grw [Nat.mod_le]
    exact Nat.zero_le _

Goal state after:
n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2
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'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ K.vertsᶜ \ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) +
      ∑ v ∈ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤
    ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts)

Tactic:
apply add_le_add

Goal state after:
case h₁
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ K.vertsᶜ \ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤
    ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t)

case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ∑ x ∈ filter K t, ↑(#K.verts)
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ p₁ ∪ p₂ = Set.univ

Tactic:
obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_
  have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
  grind

Goal state after:
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
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ ↑(t'.choose t) ^ r * ↑t + ↑r * ↑t' ≤ (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)

Tactic:
by
            rw [mul_div_assoc, le_mul_iff_one_le_right (by positivity),
              one_le_div (sub_pos.mpr ht_lt_rt'ε), sub_le_sub_iff_right,
              mul_comm (r : ℝ) (t' : ℝ),  mul_assoc, mul_le_iff_le_one_right (by positivity)]
            exact hrε_lt_1.le

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
⊢ ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
⊢ ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case e'_3.e'_5
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ n - k - 1 = #(Gᶜ.neighborFinset v)

Tactic:
simp [h.compl.regular v]

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

Goal state before:
pp: case inr
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) =
    (k • 0 + ℓ • if G.Adj v w then 1 else 0) + μ • if ¬False ∧ ¬G.Adj v w then 1 else 0

Tactic:
by_cases ha : G.Adj v w <;>
      simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one,
        not_true_eq_false, not_false_eq_true, and_false, and_self]

Goal state after:
case pos
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) = ↑ℓ

case neg
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
⊢ ↑(Fintype.card ↑(G.commonNeighbors v w)) = ↑μ
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
convert! ht.isTrail.even_countP_edges_iff x
  rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]
  change Multiset.card _ = _
  congr 1
  convert_to! _ = (ht.isTrail.edgesFinset.filter (x ∈ ·)).val
  rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
by_cases h' : G.edgeSet = ∅

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h' : G.edgeSet = ∅
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

case neg
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
⊢ G.vertexCoverNum ≤ G.edgeSet.encard
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ M, M.IsPerfectMatching

Tactic:
classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self

Goal state after: