-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
private lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux [Fintype V] {v w : V}
    (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) :
    (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
obtain ⟨w', ⟨hw'1, hw'2⟩, hwu⟩ := hcyc.existsUnique_ne_adj
  (p.toSubgraph_adj_snd hpn).adj_sub

Result:
case neg.intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
case neg.intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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:
by_cases hww' : w = w'

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
hww' : w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
hww' : ¬w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
case neg.intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have hnpvw' : ¬ p.toSubgraph.Adj v w' := by
  intro h
  exact hw'1 (hp.snd_of_toSubgraph_adj h)

Result:
case neg.intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
by_cases hvw : v = w

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
hww' : w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
subst hww'

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype 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

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
use (((hcyc.reachable_sdiff_toSubgraph_spanningCoe_aux
  (p.cons hw'2.symm) hp'p).some).mapLe hle).append this.toWalk

Result:
no goals

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

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

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
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'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have hpn : ¬p.Nil := Walk.not_nil_of_ne hvw

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype 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.Adj w v ∧ ¬p.toSubgraph.Adj w v

Tactic:
exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩

Result:
no goals