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
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hMmatch :
  (M.induce
      (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
        (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).IsMatching
⊢ False
have apply : Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
Tactic: apply Nat.not_even_iff_odd.2 c.prop
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hMmatch :
  (M.induce
      (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
        (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).IsMatching
⊢ Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
have haveI : ∀
  (this :
    Fintype
      (↑(M.induce
              (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts :
        Type u_1)),
  Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
Tactic: haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hMmatch :
  (M.induce
      (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
        (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).IsMatching
this :
  Fintype
    (↑(M.induce
            (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
              (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts :
      Type u_1)
⊢ Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
have haveI : ∀ (this : Fintype (↑(↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp : Type u_1)),
  Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
Tactic: haveI := Fintype.ofFinite c.val.supp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hMmatch :
  (M.induce
      (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
        (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).IsMatching
this :
  Fintype
    (↑(M.induce
            (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
              (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts :
      Type u_1)
⊢ Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
have haveI : ∀ (this : Fintype (↑(↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp : Type u_1)),
  Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
Tactic: classical
  haveI := Fintype.ofFinite c.val.supp
  simpa [Finset.card_image_of_injective] using hMmatch.even_card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ False
have apply : (Subgraph.map (Hom.ofLE h) x).IsPerfectMatching
Tactic: apply hmf (x.map (SimpleGraph.Hom.ofLE h))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ (Subgraph.map (Hom.ofLE h) x).IsPerfectMatching
have refine : (Subgraph.map (Hom.ofLE h) x).IsSpanning
Tactic: refine ⟨hc.1.map_ofLE h, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ (Subgraph.map (Hom.ofLE h) x).verts
have simp : v ∈ x.verts
Tactic: simp only [Subgraph.map_verts, Hom.coe_ofLE, id_eq, Set.image_id']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : G.IsMatchingFree
⊢ ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
have simp_rw : ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
Tactic: simp_rw [← @not_forall_not _ Subgraph.IsPerfectMatching]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : G.IsMatchingFree
⊢ ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
have obtain : ∀ (Gmax : SimpleGraph V) (hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax),
  ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
Tactic: obtain ⟨Gmax, hGmax⟩ := Finite.exists_le_maximal h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃ (w' : V), w ≠ w' ∧ G.Adj v w'
have simp_rw : ∀ (hadj : w ∈ G.neighborSet v), ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v
Tactic: simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
⊢ ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v
have this : (G.neighborSet v).ncard = 2
Tactic: have := h ⟨w, hadj⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
⊢ ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v
have obtain : ∀ (w' : V) (hww' : w' ∈ G.neighborSet v ∧ w' ≠ w), ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v
Tactic: obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by lia) w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃! w' : V, w ≠ w' ∧ G.Adj v w'
have obtain : ∀ (w' : V) (hww : w ≠ w') (hww' : G.Adj v w'), ∃! w' : V, w ≠ w' ∧ G.Adj v w'
Tactic: obtain ⟨w', ⟨hww, hww'⟩⟩ := h.other_adj_of_adj hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ ∃! w' : V, w ≠ w' ∧ G.Adj v w'
have h₁ : (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') y → y = w'
Tactic: use w'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') y → y = w'
have h₁ : ∀ (y : V), (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') y → y = w'
Tactic: refine ⟨⟨hww, hww'⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
⊢ (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') y → y = w'
have h₁ : ∀ (hwy : w ≠ y) (hwy' : G.Adj v y), y = w'
Tactic: ⟨hwy, hwy'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
⊢ y = w'
have h₁ : ∀ (x y' : V) (hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}), y = w'
Tactic: obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
⊢ y = w'
have hadj₁ : w ∈ G.neighborSet v
Tactic: simp_rw [← SimpleGraph.mem_neighborSet] at *
Cleared hypotheses: hadj, hww', hwy'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
hadj₁ : w ∈ G.neighborSet v
⊢ y = w'
have hww'₁ : w' ∈ G.neighborSet v
Tactic: simp_rw [← SimpleGraph.mem_neighborSet] at *
Cleared hypotheses: hadj, hww', hwy'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
hadj₁ : w ∈ G.neighborSet v
hww'₁ : w' ∈ G.neighborSet v
⊢ y = w'
have hwy'₁ : y ∈ G.neighborSet v
Tactic: simp_rw [← SimpleGraph.mem_neighborSet] at *
Cleared hypotheses: hadj, hww', hwy'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v : V
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).Nonempty →
    (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = 2
have this : ∀ (w : V) (hw : w ∈ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v),
  (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = 2
Tactic: ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : w ∈ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = 2
have hw₁ : v ∈ c.supp ∧ G.Adj v w
Tactic: rw [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = 2
have rw : (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = (G.neighborSet v).ncard
Tactic: rw [← h ⟨w, hw.2⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = (G.neighborSet v).ncard
have e_s : c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v = G.neighborSet v
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : v ∈ c.supp ∧ G.Adj v w
⊢ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v = G.neighborSet v
have e_s : ∀ (w' : V), w' ∈ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v ↔ w' ∈ G.neighborSet v
Tactic: ext w'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2
have apply : v ∈ p.support
Tactic: apply hpc.ncard_neighborSet_toSubgraph_eq_two
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ v ∈ p.support
have obtain : ∀ (w : V) (hw : w ∈ p.toSubgraph.spanningCoe.neighborSet v), v ∈ p.support
Tactic: obtain ⟨_, hw⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
⊢ p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
have Adj : ∀ (w x : V), (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.Adj w x
Tactic: ext w x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
w x : V
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.Adj w x
have Adj : p.toSubgraph.Adj w x ∨ (w = v ∧ x = u ∨ w = u ∧ x = v) ∧ w ≠ x ↔ s(v, u) = s(w, x) ∨ p.toSubgraph.Adj w x
Tactic: simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
      Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : u ≠ v
hs : s(v, u) ∉ p.edges
c : (completeGraph V).Walk v v := cons ⋯ (Walk.mapLe ⋯ p)
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles
have this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
Tactic: have : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe := by
    ext w x
    simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c,
      Walk.toSubgraph, Subgraph.sup_adj, subgraphOfAdj_adj, adj_toSubgraph_mapLe]
    grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
⊢ ∀ (w : V), p.toSubgraph.Adj v w ↔ G.Adj v w
have refine : ∀ (w : V), Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
Tactic: refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
have this : (p.toSubgraph.neighborSet v).ncard = 2
Tactic: have := hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ 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 (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
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 (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
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 (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
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 (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
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 (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]
-- 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 : V
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2
have obtain : ∀ (w : V) (hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w),
  ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2
Tactic: obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
-- 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
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2
have obtain : ∀ (w' : V) (hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'),
  ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2
Tactic: obtain ⟨w', hw'⟩ := hM'.1 (hM'.2 v)
-- 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'
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2
have simp : (∀ (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: simp only [symmDiff_def, Set.ncard_eq_two, ne_eq, imp_iff_not_or, Set.not_nonempty_iff_eq_empty,
    Set.eq_empty_iff_forall_notMem, SimpleGraph.mem_neighborSet, SimpleGraph.sup_adj, sdiff_adj,
    spanningCoe_adj, not_or, not_and, not_not]
-- 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'
⊢ (∀ (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 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}
Tactic: by_cases hww' : w = w'