-- 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
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length

Tactic:
have := Walk.IsPath.length_lt hp

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

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

Tactic:
aesop

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'
⊢ G ≤ G

Tactic:
rfl

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

Tactic:
exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)

Result:
no goals