mathlib-initiative/mathlib-tactics huggingface dataset:
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:
first | contradiction | rfl

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:
first | contradiction | rfl

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i : V
⊢ A.compl i i = 0

Tactic:
by simp [compl]

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
⊢ ∀ (a₁ : V) (ha₁ : a₁ ∈ {default}ᶜ) (a₂ : V) (ha₂ : a₂ ∈ {default}ᶜ),
    ((f a₁).firstDart ⋯).edge = ((f a₂).firstDart ⋯).edge → a₁ = a₂

Tactic:
intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))
    rw [dart_edge_eq_iff] at h
    obtain (h | h) := h
    · exact (congrArg (·.fst) h)
    · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
      have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
      · rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail

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), G.Adj x y → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
intro x

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 : V
⊢ ∀ (y : V), G.Adj x y → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
⊢ C.labelGraph k ≤ G

Tactic:
intro x

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x : V
⊢ ∀ ⦃w : V⦄, (C.labelGraph k).Adj x w → G.Adj x w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u

Tactic:
have l2 : (G.replaceVertex s t).degree u = G.degree u - 1 := by
    rw [degree, degree, ← card_singleton t, ← card_sdiff_of_subset (by simp [h.symm])]
    congr 1; ext v
    simp_rw [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]
    split_ifs <;> simp_all [adj_comm]

Goal state after:
case right
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
classical
  use (G.replaceVertex s t).replaceVertex s u, inferInstance,
    (cf.replaceVertex s t).replaceVertex s u
  have nst : s ≠ t := fun a ↦ hsu (a ▸ h)
  have ntu : t ≠ u := G.ne_of_adj h
  have := (G.adj_replaceVertex_iff_of_ne s nst ntu.symm).not.mpr hsu
  rw [card_edgeFinset_replaceVertex_of_not_adj _ this,
    card_edgeFinset_replaceVertex_of_not_adj _ hst, dst, Nat.add_sub_cancel]
  have l1 : (G.replaceVertex s t).degree s = G.degree s := by
    unfold degree; congr 1; ext v
    simp_rw [mem_neighborFinset]
    by_cases eq : v = t
    · simpa only [eq, not_adj_replaceVertex_same, false_iff]
    · rw [G.adj_replaceVertex_iff_of_ne s nst eq]
  have l2 : (G.replaceVertex s t).degree u = G.degree u - 1 := by
    rw [degree, degree, ← card_singleton t, ← card_sdiff_of_subset (by simp [h.symm])]
    congr 1; ext v
    simp_rw [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]
    split_ifs <;> simp_all [adj_comm]
  have l3 : 0 < G.degree u := by rw [G.degree_pos_iff_exists_adj u]; use t, h.symm
  lia

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
h : ¬G.IsCompleteMultipartite
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂

Tactic:
apply mt IsTrans.mk at h
  push Not at h
  obtain ⟨_, _, _, h1, h2, h3⟩ := h
  rw [adj_comm] at h1
  exact ⟨_, _, _, h3, h1, h2⟩

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

Goal state before:
pp: case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 ≤ ↑(⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).2

Tactic:
rw [Nat.le_div_iff_mul_le v.1.pos]

Goal state after:
case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 * r ≤ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
x✝¹ x✝ : V
hne : x✝¹ ≠ x✝
he : G.IsEdgeReachable 2 x✝¹ x✝
w : G.Walk x✝¹ x✝¹
hw : w.IsCycle
⊢ False

Tactic:
exact h w hw

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

Goal state before:
pp: n r c : ℕ
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
rcases r.eq_zero_or_pos with rfl | hr

Goal state after:
case inl
n c : ℕ
⊢ (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = 0 - 1

case inr
n r c : ℕ
hr : r > 0
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
| ∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

Tactic:
2,

Goal state after:
n r : ℕ
| fun x ↦ ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v

Tactic:
have h : 1 ≤ G.eccent u := Order.one_le_iff_ne_zero.mpr (eccent_ne_zero u)

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
h : 1 ≤ G.eccent u
⊢ G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩
  rw [eq_top_iff_forall_eccent_eq_one]
  intro u
  apply le_antisymm (h ▸ eccent_le_ediam)
  rw [Order.one_le_iff_pos, pos_iff_ne_zero]
  exact eccent_ne_zero u

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

Goal state before:
pp: n r : ℕ
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
rcases r.eq_zero_or_pos with rfl | hr

Goal state after:
case inl
n : ℕ
⊢ #(turanGraph n 0).edgeFinset = (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

case inr
n r : ℕ
hr : r > 0
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r)

Tactic:
rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]

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

Goal state before:
pp: case h₁
n r : ℕ
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)

Tactic:
rcases r.eq_zero_or_pos with rfl | hr

Goal state after:
case h₁.inl
n : ℕ
⊢ (n % 0 - 1) * 0 ≤ (0 - 1) * (n % 0)

case h₁.inr
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
rcases r.eq_zero_or_pos with rfl | hr

Goal state after:
case inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
cf : G.CliqueFree (0 + 1)
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
| (H.turanDensity + ε) * ↑(n.choose 2) ≤ ↑(extremalNumber n H)

Tactic:
2,

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
| ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
| zarankiewicz m n s t ≤ extremalNumber (m + n) (completeBipartiteGraph α β)

Tactic:
2,

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
| extremalNumber (m + n) (completeBipartiteGraph α β)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
| 2 * extremalNumber n (completeBipartiteGraph α β)

Tactic:
2,

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
| extremalNumber n (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
by
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he
  exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard

Tactic:
simp [hnfin.ncard]

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

Goal state before:
pp: case inr
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
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
| inr hmM' =>

Goal state after:
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
⊢ ∃ h, Bijective h ∧ ∀ (a : ↑p₁), G.Adj ↑a ↑(h a)

Tactic:
obtain ⟨f, hf₁, 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]
  have (x : V) (h : x ∈ p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) (h : x ∈ p₂) : f x ∉ p₂ := h₁.disjoint |>.notMem_of_mem_left <|
    isBipartiteWith_neighborSet_subset h₁.symm h <| Set.mem_toFinset.mp <| hf₂ x
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
p : G.Walk a a
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
⊢ ∀ (x : α), List.count (f x) (Walk.map f p).tail.support = 1

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
p : G.Walk a a
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
x : α
⊢ List.count (f x) (Walk.map f p).tail.support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
hG : G.IsHamiltonian
v : α
⊢ ∃ p, p.IsHamiltonianCycle

Tactic:
by
  obtain ⟨u, p, hp⟩ := hG Fintype.one_lt_card.ne'; exact ⟨p.rotate v <| hp.mem_support _, by simpa⟩

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ (↑c).supp
hw : (fun w ↦ M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w ↦ M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ (fun w ↦ (M.induce (Subtype.val '' (↑c).supp)).Adj (↑⟨v', hv'⟩) w) w ∧
    ∀ (y : V), (fun w ↦ (M.induce (Subtype.val '' (↑c).supp)).Adj (↑⟨v', hv'⟩) w) y → y = w

Tactic:
refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ (↑c).supp
hw : (fun w ↦ M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w ↦ M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ w ∈ Subtype.val '' (↑c).supp
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| (∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
    ∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0

Tactic:
2,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ∑ x_1, ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0

Tactic:
2,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| fun x_1 ↦ ∑ x_2, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i : V
| ∑ x_2, if G.Adj i x_2 then x i * x i - x i * x x_2 else 0

Tactic:
2,

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i : V
| fun x_2 ↦ if G.Adj i x_2 then x i * x i - x i * x x_2 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
⊢ G.IsMatchingFree

Tactic:
intro x

Goal state after:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
⊢ ¬x.IsPerfectMatching
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles

Tactic:
let c := (p.mapLe (OrderTop.le_top G)).cons (by simp [h.symm] : (completeGraph V).Adj v u)

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hw'

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : ∃ n, p.getVert n = w' ∧ n ≤ p.length
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

Tactic:
intro x

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
⊢ x ∈ ⊤ → x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: V : Type u_1
r : V
⊢ (starGraph r).IsAcyclic

Tactic:
refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ ?_
  rw [starGraph_adj] at hadj
  wlog! h : v = r
  · rw [Sym2.eq_swap]
    exact this r w v ⟨hadj.1.symm, hadj.2.symm⟩ (hadj.2.resolve_left h)
  · subst h
    apply not_reachable_of_neighborSet_right_eq_empty hadj.1
    ext x
    aesop

Goal state after: