mathlib-initiative/mathlib-tactics huggingface dataset:
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)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hadj : (_root_.completeBipartiteGraph α β).Adj s₁ s₂
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)

Tactic:
rcases hadj with ⟨hs₁, hs₂⟩ | ⟨hs₁, hs₂⟩

Goal state after:
case inl
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₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)

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 (f.toFun s₁) (f.toFun s₂)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Tactic:
set s' : Finset L := s.preimage (↑) Subtype.coe_injective.injOn

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' : Finset ↥L := s.preimage Subtype.val ⋯
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected

Tactic:
← Subgraph.copy_eq H' H.verts hv H'.Adj rfl

Goal state after:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝¹ v v✝ : V
hadj : G.Adj u v✝
w : G.Walk v✝ v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ Walk.map { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (cons hadj w).mapToSubgraph = Walk.induce s (cons hadj w) hs

Tactic:
rw [mapToSubgraph, map_cons, map_map]
    exact congrArg _ <| w.map_mapToSubgraph_eq_induce s (hs · <| List.mem_of_mem_tail ·)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
⊢ 4 * G.edgeSet.encard ≤ ENat.card V ^ 2

Tactic:
by
  refine finite_or_infinite V |>.elim (fun hv ↦ ?_) (fun _ ↦ by simp)
  have ⟨s, t, h⟩ := h.exists_isBipartiteWith
  grw [h.encard_edgeSet_le]
  have := Set.encard_union_eq h.disjoint ▸ Set.encard_le_card
  rw [ENat.card_eq_coe_natCard, ← s.toFinite.cast_ncard_eq, ← t.toFinite.cast_ncard_eq] at this ⊢
  norm_cast at this ⊢
  grind [Nat.pow_le_pow_left this 2, four_mul_le_sq_add s.ncard t.ncard]

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

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

Tactic:
rintro b₁ b₂
  obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
  exact ⟨w.ofBoxProdRight⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
⊢ (G □ H).Connected

Tactic:
have := hG.nonempty
  have := hH.nonempty
  exact ⟨hG.preconnected.boxProd hH.preconnected⟩

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.neighborFinset x.1 ×ˢ {x.2}).card + ({x.1} ×ˢ H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card

Tactic:
Finset.card_product,

Goal state after:
α : 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.neighborFinset x.1).card * {x.2}.card + {x.1}.card * (H.neighborFinset x.2).card =
    (G.neighborFinset x.1).card + (H.neighborFinset x.2).card
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Tactic:
classical
  constructor
  · intro ⟨w⟩
    exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩
  · intro ⟨⟨w₁⟩, ⟨w₂⟩⟩
    exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

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

Goal state before:
pp: case refine_1.refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph (n - 3 + 3)).Copy G
this : n = n - 3 + 3
⊢ (Walk.map h.toHom (cycleGraph.cycle (n - 3))).IsCycle

pp: case refine_1.refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph (n - 3 + 3)).Copy G
this : n = n - 3 + 3
⊢ (Walk.map h.toHom (cycleGraph.cycle (n - 3))).length = n

Tactic:
· exact (isCycle_map_iff_of_injective h.injective).mpr cycleGraph.isCycle_cycle

Goal state after:
case refine_1.refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph (n - 3 + 3)).Copy G
this : n = n - 3 + 3
⊢ (Walk.map h.toHom (cycleGraph.cycle (n - 3))).length = n
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : Group M
⊢ mulCayley {1}ᶜ = ⊤

Tactic:
simp [Set.compl_eq_univ_sdiff]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ u ≠ v → (u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0})

Tactic:
intro (h : u ≠ v)

Goal state after:
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₁ H₁ = extremalNumber n₂ H₂

Tactic:
rw [h, le_antisymm_iff]

Goal state after:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
⊢ G.IsAcyclic

Tactic:
isAcyclic_iff_forall_adj_isBridge

Goal state after:
V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
⊢ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝² : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this✝¹ : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left✝ : { fst := u', snd := v', adj := huv } ∈ p.darts
hu : { fst := u', snd := v', adj := huv }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv }.toProd.2 ∉ s
this✝ : ¬F.Reachable v' u'
this : F ⊔ edge v' u' ≤ F
⊢ False

Tactic:
by grind [Adj.reachable, sup_le_iff, le_iff_adj]

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
⊢ ¬Odd v ↔ Even v

Tactic:
simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

Goal state after:
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
⊢ ¬Even u ↔ Odd u

Tactic:
simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
⊢ G.IsAcyclic

Tactic:
isAcyclic_iff_forall_adj_isBridge

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
⊢ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ ∀ x_1 ∈ (↑(pwu.append pux).toPath).support, x_1 ∈ {v}ᶜ

Tactic:
intro z hz

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ z ∈ {v}ᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard

Tactic:
have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
      {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty := by
    refine Set.nonempty_of_ncard_ne_zero fun h' ↦ Nat.not_odd_zero ?_
    rw [← h']
    exact (c.odd_oddComponents_ncard_subset_supp _ h).2 hc
  let f : G'.oddComponents → G.oddComponents :=
    fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.1⟩
  refine Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_
  simp only [Subtype.mk.injEq, f] at fcc'
  exact Subtype.val_injective (ConnectedComponent.eq_of_common_vertex
    ((fcc' ▸ (aux c.1 c.2).choose_spec.2) (ConnectedComponent.nonempty_supp _).some_mem)
      ((aux c'.1 c'.2).choose_spec.2 (ConnectedComponent.nonempty_supp _).some_mem))

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

Goal state before:
pp: case inj'.inl
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : i₁ = i₂ → j₁ ≠ j₂
heq : i₁ = i₂
⊢ ↑((fₜ (fᵣ i₂)) j₁) ≠ ↑((fₜ (fᵣ i₂)) j₂)

Tactic:
← Subtype.ext_iff.ne

Goal state after:
case inj'.inl
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : i₁ = i₂ → j₁ ≠ j₂
heq : i₁ = i₂
⊢ (fₜ (fᵣ i₂)) j₁ ≠ (fₜ (fᵣ i₂)) j₂
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≠ 0 ↔ Nontrivial α

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≠ 0 ↔ ¬Subsingleton α
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
⊢ G.ediam = ⊤

Tactic:
obtain ⟨_, hw⟩ := h Classical.ofNonempty

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
h : G.radius = 0
⊢ Nonempty α

Tactic:
contrapose! h
    simp [radius]

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

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ : Finset V
h₁ : x✝³ ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
x✝² : Finset V
h₂ : x✝² ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
coe_map,

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
h₁ : x✝³ ∈ ⇑{ toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } '' ↑univ
h₂ : x✝² ∈ ⇑{ toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } '' ↑univ
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁' : x✝¹ ∈ ↑(map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ)
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂' : x✝ ∈ ↑(map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ)
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
coe_map,

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
h₁' : x✝¹ ∈ ⇑{ toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } '' ↑univ
h₂' : x✝ ∈ ⇑{ toFun := fun j ↦ f (w✝, j), inj' := ⋯ } '' ↑univ
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁' : x✝¹ ∈ ↑(map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ)
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂' : x✝ ∈ ↑(map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ)
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
h₁' : ∃ y, f (w✝¹, y) = x✝¹
h₂' : ∃ y, f (w✝, y) = x✝
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.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
⊢ Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)

Tactic:
· refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
      · intro hs_mem
        obtain ⟨v, hv⟩ : s.Nonempty := by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht
        exact G.irrefl <| hadj s hs_mem hv hv
      · rw [Finset.card_cons, K.card_parts.resolve_right ht]
        exact .inl rfl
      · simp_rw [mem_cons, forall_eq_or_imp]
        exact ⟨hs, fun p ↦ K.card_mem_parts⟩
      · rw [coe_cons]
        have : Std.Symm G.IsCompleteBetween := by simp [symm_def, isCompleteBetween_comm]
        exact K.isCompleteBetween.insert_of_symm fun p hp _ ↦ hadj p hp |>.symm

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')

Tactic:
haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype

Goal state after:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this : Fintype ↑(↑(Opposite.unop G')).verts
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ List.count a p.tail.support + 1 = 2

Tactic:
hp.isHamiltonian_tail

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
⊢ 1 + 1 = 2
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ List.count b p.tail.support = 1

Tactic:
hp.isHamiltonian_tail

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a a
hp : p.IsHamiltonianCycle
h : a ≠ b
⊢ 1 = 1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have : (G \ p.toSubgraph.spanningCoe).Adj w v := by
      simp only [sdiff_adj, Subgraph.spanningCoe_adj]
      exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
this : (G \ p.toSubgraph.spanningCoe).Adj w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: case inr
V : Type u_1
r v w : V
hadj : v ≠ w ∧ (v = r ∨ w = r)
this : ∀ {V : Type u_1} (r v w : V), v ≠ w ∧ (v = r ∨ w = r) → v = r → (starGraph r).IsBridge s(v, w)
h : v ≠ r
⊢ (starGraph r).IsBridge s(v, w)

pp: V✝ V : Type u_1
r v w : V
hadj : v ≠ w ∧ (v = r ∨ w = r)
h : v = r
⊢ (starGraph r).IsBridge s(v, w)

Tactic:
· rw [Sym2.eq_swap]
    exact this r w v ⟨hadj.1.symm, hadj.2.symm⟩ (hadj.2.resolve_left h)

Goal state after:
V✝ V : Type u_1
r v w : V
hadj : v ≠ w ∧ (v = r ∨ w = r)
h : v = r
⊢ (starGraph r).IsBridge s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ 2 * k

Tactic:
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
    simp [h.regular.degree_eq, two_mul]

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

Goal state before:
pp: case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x v✝ w✝ : V
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
huv : G.Adj x v✝
ht : p.IsTrail ∧ s(x, v✝) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬x = w✝ → ¬x = x ∧ ¬x = w✝

pp: case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
· rw [Nat.even_add_one, ih]
        simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
        rintro rfl rfl
        exact G.loopless.irrefl _ huv

Goal state after:
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝