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

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
refine ⟨j, ‹_›, hcard, ?_⟩

Goal state after:
case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    ↑(#(𝒜 # (Fintype.card α - (k + 1)) ∪ ∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) /
      ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))

Tactic:
card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜),

Goal state after:
case succ
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
k✝ : ℕ
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
k : ℕ
ih :
  k ≤ Fintype.card α →
    ∑ r ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
      ↑(#(falling (Fintype.card α - k) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - k))
hk : k + 1 ≤ Fintype.card α
⊢ ∑ x ∈ range (k + 1), ↑(#(𝒜 # (Fintype.card α - x))) / ↑((Fintype.card α).choose (Fintype.card α - x)) +
      ↑(#(𝒜 # (Fintype.card α - (k + 1)))) / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) ≤
    ↑(#(𝒜 # (Fintype.card α - (k + 1))) + #(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜))) /
      ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
huv : u ≠ u
⊢ (G.neighborSet u).Nonempty

Tactic:
contradiction

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
hw : v ≠ v
⊢ v ∈ G.support

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
_i _j : κ
hxi : x ∈ ⋃ i ∈ g ⁻¹' {_i}, s i
hxj : x ∈ ⋃ i ∈ g ⁻¹' {_j}, s i
⊢ _i = _j

Tactic:
obtain ⟨a, ⟨c, hc⟩, ha⟩ := hxi

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
_i _j : κ
hxj : x ∈ ⋃ i ∈ g ⁻¹' {_j}, s i
a : Set α
ha : x ∈ a
c : ι
hc : (fun i ↦ ⋃ (_ : i ∈ g ⁻¹' {_i}), s i) c = a
⊢ _i = _j
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ False

Tactic:
refine reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate v hvc) (hc.isTrail.rotate hvc)
      ?_ (Walk.start_mem_support _)

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ s(w, v) ∈ (c.rotate v hvc).edges
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 ∈ 𝒜
⊢ (0 + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [zero_add, collapse_eq hat, mul_add]
    split_ifs
    · refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_
      rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
        (insert_inter_of_notMem ‹_›) (insert_inter_distrib _ _ _).symm,
        insert_inter_of_notMem ‹_›, ← insert_inter_distrib, insert_union, insert_union_distrib,
        ← add_mul]
      gcongr
      · exact add_nonneg (h₃ _) (h₃ _)
      · exact le_collapse_of_insert_mem ‹_› h₄
          (insert_union_distrib _ _ _).symm <| union_mem_sups ‹_› ‹_›
    · rw [mul_zero, add_zero]
      refine (h ‹_› ‹_›).trans <| mul_le_mul (le_collapse_of_mem ‹_› h₃
        (insert_inter_of_notMem ‹_›) <| inter_mem_infs ‹_› ‹_›) (le_collapse_of_insert_mem ‹_› h₄
        (insert_union _ _ _) <| union_mem_sups ‹_› ‹_›) (h₄ _) <| collapse_nonneg h₃ _
    · rw [mul_zero, zero_add]
      exact (h ‹_› ‹_›).trans <| mul_le_mul (le_collapse_of_insert_mem ‹_› h₃
        (insert_inter_distrib _ _ _).symm <| inter_mem_infs ‹_› ‹_›) (le_collapse_of_insert_mem ‹_›
        h₄ (insert_union_distrib _ _ _).symm <| union_mem_sups ‹_› ‹_›) (h₄ _) <|
        collapse_nonneg h₃ _
    · simp_rw [mul_zero, add_zero]
      exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber

Tactic:
obtain ⟨_, _, h⟩ := ne_bot_iff_exists_adj.mp h
    exact two_le_chromaticNumber_of_adj h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.Preconnected

Tactic:
rw [H.connected_iff] at h

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts.Nonempty

Tactic:
rw [H.connected_iff] at h

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty
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)
⊢ (_root_.completeBipartiteGraph α β).Copy G

Tactic:
let f : α ⊕ β ↪ V := by
    refine ⟨Sum.elim (Subtype.val ∘ fα) (Subtype.val ∘ fβ), fun s₁ s₂ ↦ ?_⟩
    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:
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' := ⋯ }
⊢ (_root_.completeBipartiteGraph α β).Copy G
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : ¬G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
exact edist_eq_top_of_not_reachable hr ▸ le_top

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
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
have hadj1 := ((show i - 1 + 1 = i by lia) ▸
    p.toSubgraph_adj_getVert (by lia : (i - 1) < p.length)).symm
  ext v
  simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
    Prod.swap_prod_mk]
  refine ⟨?_, by aesop⟩
  rintro ⟨i', ⟨hl, _⟩ | ⟨_, hl⟩⟩ <;>
    apply hp.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hl <;> aesop

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

Goal state before:
pp: 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
this : i + 1 = 0
⊢ p.snd = v'

Tactic:
contradiction

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
x✝ : ↑(G ⊕g H).edgeSet
e : Sym2 (V ⊕ W)
he : e ∈ (G ⊕g H).edgeSet
u : V
v : W
h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)
⊢ ↑G.edgeSet ⊕ ↑H.edgeSet

Tactic:
contradiction

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

Goal state before:
pp: U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
x✝ : ↑(G ⊕g H).edgeSet
e : Sym2 (V ⊕ W)
he : e ∈ (G ⊕g H).edgeSet
u : W
v : V
h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)
⊢ ↑G.edgeSet ⊕ ↑H.edgeSet

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).degree x = G.degree x.1 + H.degree x.2

Tactic:
rw [degree, degree, degree, neighborFinset_boxProd, Finset.card_disjUnion]
  simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]

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

Goal state before:
pp: case mk.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u v : V
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩

Tactic:
contradiction

Goal state after:
case mk.inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u v : V
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inl v), h⟩
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case mk.inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u : V
v : W
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inr v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inr v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inl u, Sum.inr v), h⟩

Tactic:
contradiction

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

Goal state before:
pp: case mk.inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u : W
v : V
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inl v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inl v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inl v), h⟩

Tactic:
contradiction

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

Goal state before:
pp: case mk.inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u v : W
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩

Tactic:
contradiction

Goal state after:
case mk.inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
val✝ : Sym2 (V ⊕ W)
u v : W
h : Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v) ∈ (G ⊕g H).edgeSet
⊢ (fun x ↦
        match x with
        | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
        | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
      ((fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun x x_1 x_2 ↦
                match x, x_1, x_2 with
                | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
                | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
                | Sum.inl u, Sum.inr v, h => False.elim ⋯
                | Sum.inr u, Sum.inl v, h => False.elim ⋯)
              ⋯)
        ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩) =
    ⟨Quot.mk (Sym2.Rel (V ⊕ W)) (Sum.inr u, Sum.inr v), h⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce p.toSubgraph.verts G).Connected

Tactic:
exact p.toSubgraph_connected.induce_verts

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 G

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set M
G : SimpleGraph M
⊢ (fun x ↦ mulCayley x) S ≤ G ↔ S ⊆ (fun x ↦ {g | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a}) G
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
⊢ p.IsPath ↔ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) p.edges

Tactic:
refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) p.edges
⊢ p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A ⊙ A = A

Tactic:
ext i j; have := hA.zero_or_one i j; aesop

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ m < ↑(extremalNumber (Fintype.card V) H) ↔ ∃ G x, H.Free G ∧ m < ↑(#G.edgeFinset)

Tactic:
simp_rw [← Nat.floor_lt h]
  exact lt_extremalNumber_iff H ⌊m⌋₊

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (Fintype.card V - 1) H

Tactic:
by
  rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({v} : Set V), ← card_compl_set]
  apply card_edgeFinset_le_extremalNumber
  contrapose h
  exact h.trans ⟨Copy.induce G {v}ᶜ⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ (f x).takeUntil y hy = cons h nil

Tactic:
refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
hy : y ∈ (f x).support
⊢ (cons h nil).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

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

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

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

Goal state before:
pp: n : ℕ
⊢ ∀ {v w : Fin n}, (pathGraph n).Adj v w → decide (↑v % 2 = 0) ≠ decide (↑w % 2 = 0)

Tactic:
intro u v
    rw [pathGraph_adj]
    rintro (h | h) <;> simp [← h, not_iff, Nat.succ_mod_two_eq_zero_iff]

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

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

Tactic:
apply h.isAcyclic.eq_penultimate_of_adj_end hp hadj

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