awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg neg₁ : ∀ (hvw : ¬v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₂ : ∀ (hvw : ¬v = w) (hpn : ¬p.Nil), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg₃ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (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
neg₄ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (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') (hnpvw' : ¬p.toSubgraph.Adj v w'),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
pos₁ :
  ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (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') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : w = w'),
    (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
have neg₅ : ∀ (hvw : ¬v = w) (hpn : ¬p.Nil) (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') (hnpvw' : ¬p.toSubgraph.Adj v w') (hww' : ¬w = w'),
  (G \ p.toSubgraph.spanningCoe).Reachable w v
Tactic: classical
  -- Consider the case when p is nil
  by_cases hvw : v = w
  · subst hvw
    use .nil
  have hpn : ¬p.Nil := Walk.not_nil_of_ne hvw
  obtain ⟨w', ⟨hw'1, hw'2⟩, hwu⟩ := hcyc.existsUnique_ne_adj
    (p.toSubgraph_adj_snd hpn).adj_sub
  -- The edge (v, w) can't be in p, because then it would be the second node
  have hnpvw' : ¬ p.toSubgraph.Adj v w' := by
    intro h
    exact hw'1 (hp.snd_of_toSubgraph_adj h)
  -- If w = w', then the reachability can be proved with just one edge
  by_cases hww' : w = w'
  · subst hww'
    have : (G \ p.toSubgraph.spanningCoe).Adj w v := by
      simp only [sdiff_adj, Subgraph.spanningCoe_adj]
      exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩
    exact this.reachable
  -- Construct the walk needed recursively by extending p
  have hle : (G \ (p.cons hw'2.symm).toSubgraph.spanningCoe) ≤ (G \ p.toSubgraph.spanningCoe) := by
    apply sdiff_le_sdiff (by rfl) ?hcd
    simp
  have hp'p : (p.cons hw'2.symm).IsPath := by
    rw [Walk.cons_isPath_iff]
    refine ⟨hp, fun hw' ↦ ?_⟩
    exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)
  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
  use (((hcyc.reachable_sdiff_toSubgraph_spanningCoe_aux
    (p.cons hw'2.symm) hp'p).some).mapLe hle).append this.toWalk
-- 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
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length
have have : ∀ (this : Fintype V), Nat.card V + 1 - (Walk.cons sorry p).length < Nat.card V + 1 - p.length
Tactic: have := Fintype.ofFinite V
-- 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_1 : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length
have simp_wf : Fintype.card V - p.length < Fintype.card V + 1 - p.length
Tactic: simp_wf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
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_1 : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
⊢ Fintype.card V - p.length < Fintype.card V + 1 - p.length
have this₁ : p.length < Fintype.card V
Tactic: have := Walk.IsPath.length_lt hp
-- 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 have : ∀ (this : Fintype V), (G \ p.toSubgraph.spanningCoe).Reachable w v
Tactic: have : Fintype V := Fintype.ofFinite V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
have simp : fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe
Tactic: simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
      Set.mem_singleton_iff, or_true, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inst : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ (G.deleteEdges {s(v, w)}).Reachable v w
have this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
Tactic: have : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe := by
    simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
      Set.mem_singleton_iff, or_true, sup_of_le_left]
    exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
hn : (G.neighborSet v).Nonempty
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
Tactic: obtain ⟨w, hw⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have obtain : ∀ (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges),
  ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
Tactic: obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have hvp : v ∈ p.support
Tactic: have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ p.toSubgraph.Adj v w
have refine : (↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1)
Tactic: refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ (G.neighborSet v).Nonempty
have rw : ∀ (hv : v ∈ p.support) (w : V) (hadj : G.Adj v w), (G.neighborSet v).Nonempty
Tactic: rw [Walk.mem_verts_toSubgraph] at hv
Cleared hypotheses: hv, w, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
⊢ (G.neighborSet v).Nonempty
have refine : (p.toSubgraph.neighborSet v).ncard ≠ 0
Tactic: refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.support
w : V
hadj : G.Adj v w
⊢ (p.toSubgraph.neighborSet v).ncard ≠ 0
have rw : Ne (α := ℕ) 2 0
Tactic: rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
⊢ (↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1)
have this : (G.neighborSet v).Nonempty
Tactic: have : (G.neighborSet v).Nonempty := by
        rw [Walk.mem_verts_toSubgraph] at hv
        refine (Set.nonempty_of_ncard_ne_zero ?_).mono (p.toSubgraph.neighborSet_subset v)
        rw [hp.1.ncard_neighborSet_toSubgraph_eq_two hv]
        lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ (↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1)
have refine : Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : 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
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
have rw : Cardinal.mk (↑(G.neighborSet v) : Type u_1) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
rw : Cardinal.mk (↑(G.neighborSet v) : Type u_1) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
have rw₁ : (↑(G.neighborSet v).ncard : Cardinal.{u_1}) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
rw : Cardinal.mk (↑(G.neighborSet v) : Type u_1) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₁ : (↑(G.neighborSet v).ncard : Cardinal.{u_1}) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
have rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet v).ncard : Cardinal.{u_1})
  (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
rw : Cardinal.mk (↑(G.neighborSet v) : Type u_1) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₁ : (↑(G.neighborSet v).ncard : Cardinal.{u_1}) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₂ :
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet v).ncard : Cardinal.{u_1})
    (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
have rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v_1 : V
inst : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv_1 : v_1 ∈ c.supp
w_1 : V
hw : w_1 ∈ G.neighborSet v_1
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v_1, w_1) ∈ p.edges
hvp : v_1 ∈ p.support
v : V
hv : v ∈ p.toSubgraph.verts
w : V
hadj : G.Adj v w
this : (G.neighborSet v).Nonempty
rw : Cardinal.mk (↑(G.neighborSet v) : Type u_1) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₁ : (↑(G.neighborSet v).ncard : Cardinal.{u_1}) = Cardinal.mk (↑(p.toSubgraph.neighborSet v) : Type u_1)
rw₂ :
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet v).ncard : Cardinal.{u_1})
    (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑(p.toSubgraph.neighborSet v).ncard : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : 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 _),
        h this, hp.1.ncard_neighborSet_toSubgraph_eq_two (p.mem_verts_toSubgraph.mp hv)]