-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
h :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y _x →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
v : V
p_1 : (p : G.Walk v w) ×' p.IsPath
h_1 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v p_1) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
h_2 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y
        (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v
          (PSigma.mk (β := fun (p : G.Walk v w) ↦ p.IsPath) p hp)) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h_3 : (fun (w' : V) ↦ 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
have have₁ have₂ : ∀ (this : Fintype V), Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length
have₃ : ∀ (this : Fintype V), Fintype.card V - p.length < Fintype.card V + 1 - p.length
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length
have have₄ : ∀ (this : Fintype V) (this_1 : p.length < Fintype.card V), Fintype.card V - p.length < Fintype.card V + 1 - p.length
Tactic: decreasing_by
  have := Fintype.ofFinite V
  simp_wf
  have := Walk.IsPath.length_lt hp
  lia