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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ a ∈ (t ⊔ u) \ v

pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v

Tactic:
· rw [sup_eq_union, mem_sdiff, mem_union]
        exact ⟨Or.inl hat, hav⟩

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Injective supp

Tactic:
refine ConnectedComponent.ind₂ ?_
  simp only [ConnectedComponent.supp, Set.ext_iff, ConnectedComponent.eq, Set.mem_ofPred_eq]
  intro v w h
  rw [reachable_comm, h]

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

Goal state before:
pp: 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 ≤ #𝒜
m : ℕ
⊢ m ∈ range k → m < n

Tactic:
by rw [mem_range]; apply forall_lt_iff_le.2 hkn

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

Goal state before:
pp: case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (extend (⇑f) (⇑C) (const β default) (f w✝))

Tactic:
f.injective.extend_apply

Goal state after:
case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (C w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
s : Set (Sym2 V)
hs₂ : s.encard < ↑2
hs₁ : s.encard ≠ ↑1
⊢ (G.deleteEdges s).Reachable u v

Tactic:
apply G.isEdgeReachable_one.mpr huv.reachable
    exact lt_of_le_of_ne (ENat.lt_natCast_add_one_iff.mp hs₂) hs₁

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
this : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : v' ∈ w.toSubgraph.verts
⊢ v' ∈ G'.verts

Tactic:
mem_verts_toSubgraph,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : v' ∈ w.support
⊢ v' ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄,
      v_1 ∈ w.toSubgraph.verts → ∀ ⦃w_1 : V⦄, w_1 ∈ w.toSubgraph.verts → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)

Tactic:
mem_verts_toSubgraph,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → w.toSubgraph.Adj v_1 w_1) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

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

Tactic:
simp [edist, not_reachable_iff_isEmpty_walk.mp h]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
⊢ ∃ left_1 right, #left_1 = #left ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left_1 ↑right

Tactic:
← card_right

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case inr
α : 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₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    (Or.by_cases x (fun hG ↦ cons ⋯ w'.ofBoxProdLeft) fun hH ↦ ⋯ ▸ w'.ofBoxProdLeft).length +
      (⋯.by_cases (fun hH ↦ cons ⋯ w'.ofBoxProdRight) fun hG ↦ ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
simp only [h₂, add_assoc, Or.by_cases]

Goal state after:
case inr
α : 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₂ : H.Adj b₁ c.2 ∧ a₁ = c.1
⊢ w'.ofBoxProdLeft.length + (w'.ofBoxProdRight.length + 1) =
    (if h : G.Adj c.1 c.1 ∧ b₁ = c.2 then cons ⋯ w'.ofBoxProdLeft else ⋯ ▸ w'.ofBoxProdLeft).length +
      (if h : True ∧ True then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length
Module: Mathlib.Combinatorics.SimpleGraph.Sum

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

Tactic:
obtain ⟨hG⟩ := hG

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hH : H.Connected
hG : G.Preconnected
nonempty✝ : Nonempty V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inl.inr.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inl i ∈ left
j : V
hj : j ∈ ↑right.toRight
⊢ G.Adj i j

Tactic:
rw [mem_coe, mem_toRight] at hj

Goal state after:
case refine_1.inl.inr.refine_3
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inl i ∈ left
j : V
hj : Sum.inr j ∈ right
⊢ G.Adj i j
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ ∃ left_1 right, #left_1 = #left ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left_1 ↑right

Tactic:
← card_right

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ : ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left_1 ↑right_1
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case mp.inl
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩

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

Goal state before:
pp: case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
← add_eq_of_eq_sub' huv.symm,

Goal state after:
case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(↑(v + 1) % 2 = 0 ↔ ↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
← add_eq_of_eq_sub' huv.symm,

Goal state after:
case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑(u + 1) % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case h
r t : ℕ
ht_pos : t > 0
⊢ ∃ (_ : ∀ (i : Fin r), Nonempty (const (Fin r) (Fin t) i)),
    Nonempty (completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t)))

Tactic:
const_apply,

Goal state after:
case h
r t : ℕ
ht_pos : t > 0
⊢ ∃ (_ : ∀ (i : Fin r), Nonempty (Fin t)),
    Nonempty (completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t)))
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ 2 * #(completeEquipartiteGraph r t).edgeFinset = 2 * (r.choose 2 * t ^ 2)

Tactic:
← sum_degrees_eq_twice_card_edges

Goal state after:
r t : ℕ
⊢ ∑ v, (completeEquipartiteGraph r t).degree v = 2 * (r.choose 2 * t ^ 2)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
rw [Nat.card_eq_fintype_card]

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

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

Tactic:
by_cases hdiam : G.ediam = ⊤

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : G.ediam = ⊤
⊢ G.ediam ≤ 2 * G.radius

case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
⊢ G.ediam ≤ 2 * G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ hom ⋯ C = C

Tactic:
change C.map _ = C

Goal state after:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C = C
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
⊢ y = w

Tactic:
cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ (fun w ↦ (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) ↑(f ⟨v, hl⟩) ∧
    ∀ (y : V), (fun w ↦ (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) y → y = ↑(f ⟨v, hl⟩)

Tactic:
simp only [hl, exists_const, true_or, exists_true_left, true_and]

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∀ (y : V), (↑(f ⟨v, ⋯⟩) = y ∨ ∃ (h : y ∈ s), ↑(f ⟨y, h⟩) = v) → y = ↑(f ⟨v, hl⟩)
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
⊢ e ∈ G.edgeSet → ∑ a, incMatrix R G a e = 2

Tactic:
refine e.ind ?_
  intro a b h
  rw [mem_edgeSet] at h
  rw [← Nat.cast_two, ← card_pair h.ne]
  simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h]
  congr 2
  ext e
  simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n ↔ G.Colorable n

Tactic:
constructor
  · rintro ⟨P, hf, hc⟩
    have : Fintype P.parts := hf.fintype
    rw [Set.Finite.card_toFinset hf] at hc
    apply P.colorable.mono hc
  · rintro ⟨C⟩
    refine ⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩
    generalize_proofs h
    change Set.Finite (Coloring.colorClasses C) at h
    have : Fintype C.colorClasses := C.colorClasses_finite.fintype
    rw [h.card_toFinset]
    exact C.card_colorClasses_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
hn : (G.neighborSet v).Nonempty
⊢ ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      have : (G.neighborSet v).Nonempty := by
        rw [Walk.mem_verts_toSubgraph] at hv
        refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)
        rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]
        lia
      refine @Classical.ofNonempty _ ?_
      rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(insert x ((s ∩ t).erase a)) = k + 1

Tactic:
erase_eq_of_notMem <| notMem_mono inter_subset_right hat,

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(insert x (s ∩ t)) = k + 1
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
⊢ IsLowerSet ↑(μ.cells ∩ ν.cells)

Tactic:
by
        rw [Finset.coe_inter]
        exact μ.isLowerSet.inter ν.isLowerSet

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ pt₁.index = pt₁.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₁.groupElts

Tactic:
simp only [and_self, true_and]

Goal state after:
case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ ∃ g, ⟦g⟧ = pt₁.groupElts
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.row i ↔ c ∈ μ ∧ c.1 = i

Tactic:
simp [row]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ.row i ↔ (i, j) ∈ μ

Tactic:
simp [row]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
j : ℕ
⊢ μ.col j = Finset.range (μ.colLen j) ×ˢ {j}

Tactic:
by
  ext ⟨a, b⟩
  simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_col_iff,
    mem_iff_lt_colLen, and_comm, and_congr_right_iff]
  rintro rfl
  rfl

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₂ : Option α
⊢ (Option.casesOn (none, o₂).1 (none, o₂).2 fun b ↦ ((none, o₂), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, o₂).1 (none, o₂).2

Tactic:
cases o₂

Goal state after:
case none.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
⊢ (Option.casesOn (none, none).1 (none, none).2 fun b ↦ ((none, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, none).1 (none, none).2

case none.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (none, some val✝).1 (none, some val✝).2 fun b ↦ ((none, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, some val✝).1 (none, some val✝).2
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₂ : Option α
val✝ : α
⊢ (Option.casesOn (some val✝, o₂).1 (some val✝, o₂).2 fun b ↦ ((some val✝, o₂), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, o₂).1 (some val✝, o₂).2

Tactic:
cases o₂

Goal state after:
case some.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (some val✝, none).1 (some val✝, none).2 fun b ↦ ((some val✝, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, none).1 (some val✝, none).2

case some.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝¹ val✝ : α
⊢ (Option.casesOn (some val✝¹, some val✝).1 (some val✝¹, some val✝).2 fun b ↦ ((some val✝¹, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝¹, some val✝).1 (some val✝¹, some val✝).2
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Nat.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
Fintype.card_eq_nat_card,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc : ¬Nat.card ↑Gmax.universalVerts < Nat.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
⊢ False