-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {u 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

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

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

Proof state:
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 = c.toSubgraph.spanningCoe

Tactic:
ext w x

Result:
case Adj.h.h.a
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)
w x : V
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.Adj w x

Proof state:
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)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ c.IsCycle

Tactic:
simp [Walk.cons_isCycle_iff, c, hp, hs]

Result:
no goals

Proof state:
case Adj.h.h.a
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)
w x : V
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.Adj w x

Tactic:
simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
  Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]

Result:
case Adj.h.h.a
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)
w x : V
⊢ p.toSubgraph.Adj w x ∨ (w = v ∧ x = u ∨ w = u ∧ x = v) ∧ w ≠ x ↔ s(v, u) = s(w, x) ∨ p.toSubgraph.Adj w x

Proof state:
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
⊢ (completeGraph V).Adj v u

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
case Adj.h.h.a
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)
w x : V
⊢ p.toSubgraph.Adj w x ∨ (w = v ∧ x = u ∨ w = u ∧ x = v) ∧ w ≠ x ↔ s(v, u) = s(w, x) ∨ p.toSubgraph.Adj w x

Tactic:
aesop

Result:
no goals

Proof state:
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)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles

Tactic:
exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs])

Result:
no goals

Proof state:
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

Tactic:
have : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe := by
  ext w x
  simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
    Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]
  aesop

Result:
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)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles