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
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
hvp : v ∈ p.support
⊢ p.toSubgraph.verts = c.supp
have obtain : ∀ (c' : G.ConnectedComponent) (hc' : p.toSubgraph.verts = c'.supp), p.toSubgraph.verts = c.supp
Tactic: obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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 : 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
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ p.toSubgraph.verts = c.supp
have rw : c'.supp = c.supp
Tactic: rw [hc']
-- 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
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ c'.supp = c.supp
have this : v ∈ c'.supp
Tactic: have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
-- 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
hvp : v ∈ p.support
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have this : p.toSubgraph.verts = c.supp
Tactic: have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
-- 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
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have h₁ : (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
Tactic: use p.rotate v hvp
-- 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
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
have h₁ : (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts
Tactic: rw [← this]
-- 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: classical
  obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩
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
hn : (G.neighborSet v).Nonempty
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have obtain₁ : ∀ (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
Tactic: classical
  obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩
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
hn : (G.neighborSet v).Nonempty
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₁ :
  ∀ (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
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have obtain₂ : ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
  (hvp : v ∈ p.support), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
Tactic: classical
  obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩
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
hn : (G.neighborSet v).Nonempty
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₁ :
  ∀ (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
obtain₂ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have obtain₃ : ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges) (hvp : v ∈ p.support)
  (this : p.toSubgraph.verts = c.supp), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
Tactic: classical
  obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩
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
hn : (G.neighborSet v).Nonempty
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₁ :
  ∀ (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
obtain₂ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₃ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support) (this : p.toSubgraph.verts = c.supp),
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have h₁ : ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges) (hvp : v ∈ p.support)
  (this : p.toSubgraph.verts = c.supp), (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
Tactic: classical
  obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩
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
hn : (G.neighborSet v).Nonempty
obtain : ∀ (w : V) (hw : w ∈ G.neighborSet v), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₁ :
  ∀ (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
obtain₂ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support), ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
obtain₃ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support) (this : p.toSubgraph.verts = c.supp),
    ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
h₁ :
  ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges)
    (hvp : v ∈ p.support) (this : p.toSubgraph.verts = c.supp),
    (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp
⊢ ∃ (p : G.Walk v v), p.IsCycle ∧ p.toSubgraph.verts = c.supp
have h₂ : ∀ (w : V) (hw : w ∈ G.neighborSet v) (u : V) (p : G.Walk u u) (hp : p.IsCycle ∧ s(v, w) ∈ p.edges) (hvp : v ∈ p.support)
  (this : p.toSubgraph.verts = c.supp),
  (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts
Tactic: classical
  obtain ⟨w, hw⟩ := hn
  obtain ⟨u, p, hp⟩ := SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle.mp
    ⟨hw, h.reachable_deleteEdges hw⟩
  have hvp : v ∈ p.support := SimpleGraph.Walk.fst_mem_support_of_mem_edges _ hp.2
  have : p.toSubgraph.verts = c.supp := by
    obtain ⟨c', hc'⟩ := p.toSubgraph_connected.exists_verts_eq_connectedComponentSupp (by
      intro v hv w hadj
      refine (Subgraph.adj_iff_of_neighborSet_equiv ?_ (Set.toFinite _)).mpr hadj
      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
      refine @Classical.ofNonempty _ ?_
      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)])
    rw [hc']
    have : v ∈ c'.supp := by
      rw [← hc', Walk.mem_verts_toSubgraph]
      exact hvp
    simp_all
  use p.rotate v hvp
  rw [← this]
  exact ⟨hp.1.rotate _, by simp⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
⊢ (G ⊔ edge u x).IsAlternating G'
have pos : ∀ (hadj : G.Adj u x), (G ⊔ edge u x).IsAlternating G'
Tactic: by_cases hadj : G.Adj u x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
pos : ∀ (hadj : G.Adj u x), (G ⊔ edge u x).IsAlternating G'
⊢ (G ⊔ edge u x).IsAlternating G'
have neg : ∀ (hadj : ¬G.Adj u x), (G ⊔ edge u x).IsAlternating G'
Tactic: by_cases hadj : G.Adj u x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvw : (G ⊔ edge u x).Adj v w
hvv' : (G ⊔ edge u x).Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have hvw₁ : G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
Tactic: simp only [sup_adj, edge_adj] at hvw hvv'
Cleared hypotheses: hvw, hvv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvw : (G ⊔ edge u x).Adj v w
hvv' : (G ⊔ edge u x).Adj v w'
hvw₁ : G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have hvv'₁ : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
Tactic: simp only [sup_adj, edge_adj] at hvw hvv'
Cleared hypotheses: hvw, hvv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvw : G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg : ∀ (hl : G.Adj v w), G'.Adj v w ↔ ¬G'.Adj v w'
Tactic: obtain hl | hr := hvw
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvw : G.Adj v w ∨ (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
neg : ∀ (hl : G.Adj v w), G'.Adj v w ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg₁ : ∀ (hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w), G'.Adj v w ↔ ¬G'.Adj v w'
Tactic: obtain hl | hr := hvw
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hl : G.Adj v w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg : ∀ (h1 : G.Adj v w'), G'.Adj v w ↔ ¬G'.Adj v w'
Tactic: obtain h1 | h2 := hvv'
Cleared hypotheses: hvv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hl : G.Adj v w
neg : ∀ (h1 : G.Adj v w'), G'.Adj v w ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg₁ : ∀ (h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'), G'.Adj v w ↔ ¬G'.Adj v w'
Tactic: obtain h1 | h2 := hvv'
Cleared hypotheses: hvv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg : ∀ (h1 : G.Adj v w'), G'.Adj v w ↔ ¬G'.Adj v w'
Tactic: obtain h1 | h2 := hvv'
Cleared hypotheses: hvv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hvv' : G.Adj v w' ∨ (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
neg : ∀ (h1 : G.Adj v w'), G'.Adj v w ↔ ¬G'.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg₁ : ∀ (h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'), G'.Adj v w ↔ ¬G'.Adj v w'
Tactic: obtain h1 | h2 := hvv'
Cleared hypotheses: hvv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg : G'.Adj v w ↔ ¬G'.Adj u x
Tactic: rw [G'.adj_congr_of_sym2 (by grind : s(v, w') = s(u, x))]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj u x
have neg : G'.Adj v w
Tactic: simp only [hnadj, not_false_eq_true, iff_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w
have neg : ∀ (hnadj : ¬G'.Adj v w') (hu' : ∀ (u' : V), u' ≠ v → G.Adj w' u' → G'.Adj w' u')
  (hx' : ∀ (x' : V), x' ≠ w' → G.Adj x' v → G'.Adj x' v) (hadj : ¬G.Adj v w')
  (h2 : (v = v ∧ w' = w' ∨ v = w' ∧ w' = v) ∧ v ≠ w'), G'.Adj v w
Tactic: rcases h2.1 with ⟨rfl, rfl⟩ | ⟨h2r1, h2r2⟩
Cleared hypotheses: u, x, hnadj, hu', hx', hadj, h2