awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
h :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y _x →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
v : V
p_1 : (p : G.Walk v w) ×' p.IsPath
h_1 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v p_1) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
h_2 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y
        (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v
          (PSigma.mk (β := fun (p : G.Walk v w) ↦ p.IsPath) p hp)) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h_3 : (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this_1 : (G \ p.toSubgraph.spanningCoe).Adj w' v
this_2 : Fintype V
this : p.length < Fintype.card V
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
have : ∀ (this : Fintype V), (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have : Fintype V := Fintype.ofFinite V
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
this : Fintype V
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
reachable_sdiff_toSubgraph_spanningCoe_aux hcyc p hp

Premises used: _private.0.SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
this : Fintype V
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
exact reachable_sdiff_toSubgraph_spanningCoe_aux hcyc p hp

Premises used: _private.0.SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
simp : fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe
⊢ fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe

Tactic:
simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
      Set.mem_singleton_iff, or_true, sup_of_le_left]

Premises used: SimpleGraph.singletonSubgraph_le_iff, SimpleGraph.Walk.toSubgraph, Set.mem_singleton_iff, SimpleGraph.subgraphOfAdj_verts, Set.mem_insert_iff, or_true, sup_of_le_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe

Tactic:
(Subgraph.spanningCoe_subgraphOfAdj hadj).symm

Premises used: SimpleGraph.Subgraph.spanningCoe_subgraphOfAdj, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe

Tactic:
exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm

Premises used: SimpleGraph.Subgraph.spanningCoe_subgraphOfAdj, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe

Tactic:
have : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe := by
    simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
      Set.mem_singleton_iff, or_true, sup_of_le_left]
    exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)}

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w

Tactic:
this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk
    (Walk.IsPath.of_adj hadj)).symm

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Adj.toWalk, SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe, Eq.rec, Eq.symm, SimpleGraph.Walk.IsPath.of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w

Tactic:
exact this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk
    (Walk.IsPath.of_adj hadj)).symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
obtain ⟨w, hw⟩ := hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
obtain :
  ∀ (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges),
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

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

Premises used: SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, And.intro, SimpleGraph.IsCycles.reachable_deleteEdges, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
⊢ v ∈ p.support

Tactic:
have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ p.toSubgraph.Adj v w

Tactic:
(Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj

Premises used: Iff.mpr, SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv, Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
refine : (↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1)
⊢ p.toSubgraph.Adj v w

Tactic:
refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj

Premises used: Iff.mpr, SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv, Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
rw : ∀ (hv : v ∈ p.support) (w : V) (hadj : G.Adj v w), (G.neighborSet v).Nonempty
⊢ (G.neighborSet v).Nonempty

Tactic:
rw [Walk.mem_verts_toSubgraph] at hv

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
⊢ (G.neighborSet v).Nonempty

Tactic:
(Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)

Premises used: SimpleGraph.Walk.toSubgraph, Set.Nonempty.mono, Set.nonempty_of_ncard_ne_zero, SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
refine : (p.toSubgraph.neighborSet v).ncard ≠ 0
⊢ (G.neighborSet v).Nonempty

Tactic:
refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)

Premises used: SimpleGraph.Walk.toSubgraph, Set.Nonempty.mono, Set.nonempty_of_ncard_ne_zero, SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
rw : Ne (α := ℕ) 2 0
⊢ (p.toSubgraph.neighborSet v).ncard ≠ 0

Tactic:
rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]

Premises used: SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
⊢ Ne (α := ℕ) 2 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ (G.neighborSet v).Nonempty

Tactic:
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
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
refine : Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
⊢ (↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1)

Tactic:
refine @Classical.ofNonempty _ ?_

Premises used: Classical.ofNonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
rw : Cardinal.mk (↑(G.neighborSet v) : Type u_1) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₁ : (↑(G.neighborSet v).ncard : Cardinal.{u_1}) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₂ :
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet v).ncard : Cardinal.{u_1})
    (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
rw₄ rw₅ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))

Tactic:
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)]

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph, SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two, Set.toFinite, And.left, Cardinal.eq, Set.cast_ncard, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
obtain : ∀ (c' : G.ConnectedComponent) (hc' : p.toSubgraph.verts = c'.supp), p.toSubgraph.verts = c.supp
⊢ p.toSubgraph.verts = c.supp

Tactic:
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)])

Premises used: SimpleGraph.Subgraph.Connected.exists_verts_eq_connectedComponentSupp, SimpleGraph.Walk.toSubgraph_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
rw : c'.supp = c.supp
⊢ p.toSubgraph.verts = c.supp

Tactic:
rw [hc']
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
rw : v ∈ p.support
⊢ v ∈ c'.supp

Tactic:
rw [← hc', Walk.mem_verts_toSubgraph]

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ p.support

Tactic:
hvp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ p.support

Tactic:
exact hvp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ c'.supp

Tactic:
have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
this : v ∈ c'.supp
⊢ c'.supp = c.supp

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
⊢ p.toSubgraph.verts = c.supp

Tactic:
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
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
h₁ : (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
use p.rotate v hvp

Premises used: SimpleGraph.Walk.rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
h₁ : (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp

Tactic:
rw [← this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨hp.1.rotate _, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
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
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₁ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges),
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₂ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₃ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support) (this : p.toSubgraph.verts = c.supp),
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
h₁ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support) (this : p.toSubgraph.verts = c.supp),
    (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
h₂ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support) (this : p.toSubgraph.verts = c.supp),
    (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
classical
  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⟩