-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp [Finite V]
    {c : G.ConnectedComponent} (h : G.IsCycles) (hv : v ∈ c.supp)
    (hn : (G.neighborSet v).Nonempty) :
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp

Proof state:
case intro.intro.intro
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, p.IsCycle ∧ 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]
      omega
    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

Result:
case intro.intro.intro
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, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Proof state:
case intro.intro.intro
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, p.IsCycle ∧ p.toSubgraph.verts = c.supp

Tactic:
use p.rotate hvp

Result:
case h
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 hvp).IsCycle ∧ (p.rotate hvp).toSubgraph.verts = c.supp

Proof state:
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
⊢ ∀ v ∈ p.toSubgraph.verts, ∀ (w : V), G.Adj v w → p.toSubgraph.Adj v w

Tactic:
intro v hv w hadj

Result:
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
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ p.toSubgraph.Adj v w

Proof state:
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:
rw [← hc', Walk.mem_verts_toSubgraph]

Result:
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

Proof state:
case h
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 hvp).IsCycle ∧ (p.rotate hvp).toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨hp.1.rotate _, by simp_all⟩

Result:
no goals

Proof state:
case intro
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
⊢ c'.supp = c.supp

Tactic:
have : v ∈ c'.supp := by
  rw [← hc', Walk.mem_verts_toSubgraph]
  exact hvp

Result:
case intro
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

Proof state:
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
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ ↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v)

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]
  omega

Result:
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
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ ↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v)

Proof state:
case intro
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
⊢ p.toSubgraph.verts = c.supp

Tactic:
rw [hc']

Result:
case intro
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
⊢ c'.supp = c.supp

Proof state:
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:
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]
    omega
  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)])

Result:
case intro
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
⊢ p.toSubgraph.verts = c.supp