awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
pos :
  ∀ (hww' : w = w'),
    (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
      ∃ (x : V) (y : V),
        ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
have neg : ∀ (hww' : ¬w = w'),
  (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
Tactic: by_cases hww' : w = w'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
have neg : ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
Tactic: right
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
have h : ¬w = w' ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {w, w'}
Tactic: use w, w'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.snd = w'
have apply : p.toSubgraph.Adj v w'
Tactic: apply hp.snd_of_toSubgraph_adj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'
have hw'₁ : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length
Tactic: rw [Walk.mem_support_iff_exists_getVert] at hw'
Cleared hypotheses: hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'
have obtain : ∀ (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)), p.toSubgraph.Adj v (p.getVert n)
Tactic: obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
Cleared hypotheses: w', hw, hw', hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v (p.getVert n)
have pos : ∀ (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
Tactic: by_cases hn : n = 0 ∨ n = p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
pos : ∀ (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v (p.getVert n)
have neg : ∀ (hn : ¬(n = 0 ∨ n = p.length)), p.toSubgraph.Adj v (p.getVert n)
Tactic: by_cases hn : n = 0 ∨ n = p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
have refine : Nonempty.{u_1 + 1}
  ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
Tactic: refine @Classical.ofNonempty _ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
have rw : Cardinal.mk (↑(G.neighborSet (p.getVert n)) : Type u_1) =
  Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
rw :
  Cardinal.mk (↑(G.neighborSet (p.getVert n)) : Type u_1) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
⊢ Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
have rw₁ : (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) =
  Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
rw :
  Cardinal.mk (↑(G.neighborSet (p.getVert n)) : Type u_1) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₁ :
  (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
⊢ Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
have rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
  (↑(p.toSubgraph.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
rw :
  Cardinal.mk (↑(G.neighborSet (p.getVert n)) : Type u_1) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₁ :
  (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₂ :
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
    (↑(p.toSubgraph.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
have rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
rw :
  Cardinal.mk (↑(G.neighborSet (p.getVert n)) : Type u_1) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₁ :
  (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₂ :
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
    (↑(p.toSubgraph.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
have rw₄ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ p.toSubgraph.Adj v (p.getVert n)
have neg : ∀ (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
  p.toSubgraph.Adj v (p.getVert n)
Tactic: have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
⊢ p.toSubgraph.Adj v (p.getVert n)
have neg : G.Adj (p.getVert n) v
Tactic: rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.snd = w'
have apply : p.toSubgraph.Adj v w'
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
⊢ p.snd = w'
have apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
Cleared hypotheses: hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
⊢ p.snd = w'
have apply₂ : ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)),
  p.toSubgraph.Adj v (p.getVert n)
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
Cleared hypotheses: w', hw, hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
apply₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)),
    p.toSubgraph.Adj v (p.getVert n)
⊢ p.snd = w'
have pos : ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
  (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
Cleared hypotheses: w', hw, hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
apply₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)),
    p.toSubgraph.Adj v (p.getVert n)
pos :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
⊢ p.snd = w'
have neg : ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
  (hn : ¬(n = 0 ∨ n = p.length)), p.toSubgraph.Adj v (p.getVert n)
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
Cleared hypotheses: w', hw, hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
apply₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)),
    p.toSubgraph.Adj v (p.getVert n)
pos :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
neg neg₁ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : ¬(n = 0 ∨ n = p.length)), p.toSubgraph.Adj v (p.getVert n)
⊢ p.snd = w'
have neg₂ : ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
  (hn : ¬(n = 0 ∨ n = p.length))
  (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
  p.toSubgraph.Adj v (p.getVert n)
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
Cleared hypotheses: w', hw, hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
apply₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)),
    p.toSubgraph.Adj v (p.getVert n)
pos :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
neg neg₁ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : ¬(n = 0 ∨ n = p.length)), p.toSubgraph.Adj v (p.getVert n)
neg₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : ¬(n = 0 ∨ n = p.length))
    (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
    p.toSubgraph.Adj v (p.getVert n)
⊢ p.snd = w'
have neg₃ : ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
  (hn : ¬(n = 0 ∨ n = p.length))
  (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
  G.Adj (p.getVert n) v
Tactic: classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm
Cleared hypotheses: w', hw, hw', hp, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
have pos : ∀ (hvw : v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
pos : ∀ (hvw : v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
have neg : ∀ (hvw : ¬v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
Tactic: by_cases hvw : v = w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite 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
have pos : ∀ (p : G.Walk v v) (hp : p.IsPath), (G \ p.toSubgraph.spanningCoe).Reachable v v
Tactic: subst hvw
Cleared hypotheses: w, p, hp, hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v : V
hcyc : G.IsCycles
p : G.Walk v v
hp : p.IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable v v
have val : (G \ p.toSubgraph.spanningCoe).Walk v v
Tactic: use .nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite 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
have hpn : ¬p.Nil
Tactic: have hpn : ¬p.Nil := Walk.not_nil_of_ne hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite 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
have neg : ∀ (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ 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: obtain ⟨w', ⟨hw'1, hw'2⟩, hwu⟩ := hcyc.existsUnique_ne_adj
    (p.toSubgraph_adj_snd hpn).adj_sub