-- 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:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
x✝ : (v : V) ×' (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath
a✝⁴ :
  ∀ (y : (v : V) ×' (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath),
    (invImage
            (fun x =>
              PSigma.casesOn x fun v w =>
                PSigma.casesOn w fun w hcyc =>
                  PSigma.casesOn hcyc fun hcyc p => PSigma.casesOn p fun p hp => Fintype.card V + 1 - p.length)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      (G \ y.2.2.2.1.toSubgraph.spanningCoe).Reachable y.2.1 y.1
v : V
w✝ : (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath
a✝³ :
  ∀ (y : (v : V) ×' (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath),
    (invImage
            (fun x =>
              PSigma.casesOn x fun v w =>
                PSigma.casesOn w fun w hcyc =>
                  PSigma.casesOn hcyc fun hcyc p => PSigma.casesOn p fun p hp => Fintype.card V + 1 - p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v, w✝⟩ →
      (G \ y.2.2.2.1.toSubgraph.spanningCoe).Reachable y.2.1 y.1
w : V
hcyc✝ : (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath
a✝² :
  ∀ (y : (v : V) ×' (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath),
    (invImage
            (fun x =>
              PSigma.casesOn x fun v w =>
                PSigma.casesOn w fun w hcyc =>
                  PSigma.casesOn hcyc fun hcyc p => PSigma.casesOn p fun p hp => Fintype.card V + 1 - p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v, ⟨w, hcyc✝⟩⟩ →
      (G \ y.2.2.2.1.toSubgraph.spanningCoe).Reachable y.2.1 y.1
hcyc : G.IsCycles
p✝ : (p : G.Walk v w) ×' p.IsPath
a✝¹ :
  ∀ (y : (v : V) ×' (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath),
    (invImage
            (fun x =>
              PSigma.casesOn x fun v w =>
                PSigma.casesOn w fun w hcyc =>
                  PSigma.casesOn hcyc fun hcyc p => PSigma.casesOn p fun p hp => Fintype.card V + 1 - p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v, ⟨w, ⟨hcyc, p✝⟩⟩⟩ →
      (G \ y.2.2.2.1.toSubgraph.spanningCoe).Reachable y.2.1 y.1
p : G.Walk v w
hp : p.IsPath
a✝ :
  ∀ (y : (v : V) ×' (w : V) ×' (_ : G.IsCycles) ×' (p : G.Walk v w) ×' p.IsPath),
    (invImage
            (fun x =>
              PSigma.casesOn x fun v w =>
                PSigma.casesOn w fun w hcyc =>
                  PSigma.casesOn hcyc fun hcyc p => PSigma.casesOn p fun p hp => Fintype.card V + 1 - p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v, ⟨w, ⟨hcyc, ⟨p, hp⟩⟩⟩⟩ →
      (G \ y.2.2.2.1.toSubgraph.spanningCoe).Reachable y.2.1 y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h✝ : (fun w' => 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✝ : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : p.length < Fintype.card V
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length

Tactic:
omega

Result:
no goals

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
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.Adj w' v ∧ ¬p.toSubgraph.Adj w' v

Tactic:
refine ⟨hw'2.symm, fun h ↦ ?_⟩

Result:
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
h : p.toSubgraph.Adj w' v
⊢ False

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
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 \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe

Tactic:
apply sdiff_le_sdiff (by rfl) ?hcd

Result:
case hcd
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'
⊢ p.toSubgraph.spanningCoe ≤ (Walk.cons ⋯ p).toSubgraph.spanningCoe

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
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'
⊢ ¬p.toSubgraph.Adj v w'

Tactic:
intro h

Result:
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'
h : p.toSubgraph.Adj v w'
⊢ False

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
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
subst hvw

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

Tactic:
refine ⟨hp, fun hw' ↦ ?_⟩

Result:
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
hw' : w' ∈ p.support
⊢ False

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 \ p.toSubgraph.spanningCoe).Adj w v

Tactic:
simp only [sdiff_adj, Subgraph.spanningCoe_adj]

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