awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
w v' : V
hv'_1 : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv'_1 ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv'_1) : V)
          w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj
              (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv'_1) : V)
              w)
          y →
        y = w
hwnu : w ∉ u
hv' : v' ∉ u
⊢ v' ∉ u

Tactic:
trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ (M.induce
      (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
        (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).IsMatching

Tactic:
have hMmatch : (M.induce c.val.supp).IsMatching := by
    intro v hv
    obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
    obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv
    use w
    have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
    refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
    apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
    simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and,
      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
      and_true] at hv' ⊢
    trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
apply : Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
⊢ False

Tactic:
apply Nat.not_even_iff_odd.2 c.prop

Premises used: Iff.mpr, Nat.not_even_iff_odd, Subtype.prop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
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
⊢ Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard

Tactic:
haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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)
haveI :
  ∀ (this : Fintype (↑(↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp : Type u_1)),
    Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
⊢ Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard

Tactic:
haveI := Fintype.ofFinite c.val.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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_1 :
  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)
this : Fintype (↑(↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp : Type u_1)
⊢ Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard

Tactic:
simpa [Finset.card_image_of_injective] using hMmatch.even_card

Premises used: Finset.card_image_of_injective, SimpleGraph.Subgraph.IsMatching.even_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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)
haveI haveI₁ haveI₂ :
  ∀ (this : Fintype (↑(↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp : Type u_1)),
    Even (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp.ncard
⊢ 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

Premises used: Finset.card_image_of_injective, SimpleGraph.Subgraph.IsMatching.even_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
by_contra! : ∀ (hc : x.IsPerfectMatching), False
⊢ ¬x.IsPerfectMatching

Tactic:
by_contra! hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
apply : (Subgraph.map (Hom.ofLE h) x).IsPerfectMatching
⊢ False

Tactic:
apply hmf (x.map (SimpleGraph.Hom.ofLE h))

Premises used: SimpleGraph.Subgraph.map, SimpleGraph.Hom.ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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

Tactic:
⟨hc.1.map_ofLE h, ?_⟩

Premises used: SimpleGraph.Subgraph.IsMatching.map_ofLE, And.left, And.intro, SimpleGraph.Subgraph.IsPerfectMatching
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
refine : (Subgraph.map (Hom.ofLE h) x).IsSpanning
⊢ (Subgraph.map (Hom.ofLE h) x).IsPerfectMatching

Tactic:
refine ⟨hc.1.map_ofLE h, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
simp : v ∈ x.verts
⊢ v ∈ (Subgraph.map (Hom.ofLE h) x).verts

Tactic:
simp only [Subgraph.map_verts, Hom.coe_ofLE, id_eq, Set.image_id']

Premises used: Set.image_id', SimpleGraph.Subgraph.map_verts, SimpleGraph.Hom.coe_ofLE, id_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ x.verts

Tactic:
hc.2 v

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ x.verts

Tactic:
exact hc.2 v

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : G.IsMatchingFree
simp_rw :
  ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
⊢ ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching

Tactic:
simp_rw [← @not_forall_not _ Subgraph.IsPerfectMatching]

Premises used: not_forall_not
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : G.IsMatchingFree
obtain :
  ∀ (Gmax : SimpleGraph V) (hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax),
    ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
⊢ ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Tactic:
obtain ⟨Gmax, hGmax⟩ := Finite.exists_le_maximal h

Premises used: Finite.exists_le_maximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : G.IsMatchingFree
Gmax : SimpleGraph V
hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax
⊢ ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Tactic:
⟨Gmax, ⟨hGmax.1, ⟨hGmax.2.prop, fun _ h' ↦ hGmax.2.not_prop_of_gt h'⟩⟩⟩

Premises used: Maximal.prop, Maximal.not_prop_of_gt, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : G.IsMatchingFree
Gmax : SimpleGraph V
hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax
⊢ ∃ (Gmax : SimpleGraph V), G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Tactic:
exact ⟨Gmax, ⟨hGmax.1, ⟨hGmax.2.prop, fun _ h' ↦ hGmax.2.not_prop_of_gt h'⟩⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
simp_rw : ∀ (hadj : w ∈ G.neighborSet v), ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v
⊢ ∃ (w' : V), w ≠ w' ∧ G.Adj v w'

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢

Premises used: SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
⊢ (G.neighborSet v).ncard = 2

Tactic:
have := h ⟨w, hadj⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ 1 < (G.neighborSet v).ncard

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
obtain : ∀ (w' : V) (hww' : w' ∈ G.neighborSet v ∧ w' ≠ w), ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v
⊢ ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by lia) w

Premises used: Set.exists_ne_of_one_lt_ncard
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
hww' : w' ∈ G.neighborSet v ∧ w' ≠ w
⊢ ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
⟨w', ⟨hww'.2.symm, hww'.1⟩⟩

Premises used: Ne.symm, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
hww' : w' ∈ G.neighborSet v ∧ w' ≠ w
⊢ ∃ (w' : V), w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
obtain : ∀ (w' : V) (hww : w ≠ w') (hww' : G.Adj v w'), ∃! w' : V, w ≠ w' ∧ G.Adj v w'
⊢ ∃! w' : V, w ≠ w' ∧ G.Adj v w'

Tactic:
obtain ⟨w', ⟨hww, hww'⟩⟩ := h.other_adj_of_adj hadj

Premises used: SimpleGraph.IsCycles.other_adj_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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'
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'
⊢ ∃! w' : V, w ≠ w' ∧ G.Adj v w'

Tactic:
use w'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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'

Tactic:
⟨⟨hww, hww'⟩, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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'
h₁ : ∀ (y : V), (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') y → y = 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'

Tactic:
refine ⟨⟨hww, hww'⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
h₁ : ∀ (hwy : w ≠ y) (hwy' : G.Adj v y), y = w'
⊢ (fun (w' : V) ↦ w ≠ w' ∧ G.Adj v w') y → y = w'

Tactic:
⟨hwy, hwy'⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
h₁ : ∀ (x y' : V) (hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}), y = w'
⊢ y = w'

Tactic:
obtain ⟨x, y', hxy'⟩ := Set.ncard_eq_two.mp (h ⟨w, hadj⟩)

Premises used: Set.ncard_eq_two, Exists.intro, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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'}
⊢ w ∈ G.neighborSet v

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at *

Premises used: SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ w' ∈ G.neighborSet v

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at *

Premises used: SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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 ∈ G.neighborSet v

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at *

Premises used: SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
w' : V
hww : w ≠ w'
y : V
hwy : w ≠ y
x y' : V
hxy' : x ≠ y' ∧ G.neighborSet v = {x, y'}
hadj : w ∈ G.neighborSet v
hww' : w' ∈ G.neighborSet v
hwy' : y ∈ G.neighborSet v
⊢ y = w'

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v : V
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
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).Nonempty →
    (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = 2

Tactic:
⟨w, hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ v ∈ c.supp ∧ G.Adj v w

Tactic:
rw [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph] at hw

Premises used: SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph, SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
rw : (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = (G.neighborSet v).ncard
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = 2

Tactic:
rw [← h ⟨w, hw.2⟩]

Premises used: And.right, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
e_s : c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v = G.neighborSet v
⊢ (c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v).ncard = (G.neighborSet v).ncard

Tactic:
congr 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
e_s : ∀ (w' : V), w' ∈ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v ↔ w' ∈ G.neighborSet v
⊢ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v = G.neighborSet v

Tactic:
ext w'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
w' : V
⊢ w' ∈ c.toSimpleGraph.spanningCoe (s := (↑c : Set V)).neighborSet v ↔ w' ∈ G.neighborSet v

Tactic:
simp only [mem_neighborSet, c.adj_spanningCoe_toSimpleGraph, hw, true_and]

Premises used: SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph, SimpleGraph.mem_neighborSet, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
apply : v ∈ p.support
⊢ (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2

Tactic:
apply hpc.ncard_neighborSet_toSubgraph_eq_two

Premises used: SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
obtain : ∀ (w : V) (hw : w ∈ p.toSubgraph.spanningCoe.neighborSet v), v ∈ p.support
⊢ v ∈ p.support

Tactic:
obtain ⟨_, hw⟩ := hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v w : V
hw : w ∈ p.toSubgraph.spanningCoe.neighborSet v
⊢ v ∈ p.support

Tactic:
p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Walk.mem_verts_toSubgraph, SimpleGraph.Walk.toSubgraph, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v w : V
hw : w ∈ p.toSubgraph.spanningCoe.neighborSet v
⊢ v ∈ p.support

Tactic:
exact p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Walk.mem_verts_toSubgraph, SimpleGraph.Walk.toSubgraph, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ (completeGraph V).Adj v u

Tactic:
simp [h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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)
Adj : ∀ (w x : V), (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.Adj w x
⊢ p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe

Tactic:
ext w x
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
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
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).Adj w x ↔ c.toSubgraph.spanningCoe.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]

Premises used: SimpleGraph.Subgraph.sup_adj, SimpleGraph.subgraphOfAdj_adj, SimpleGraph.Walk.adj_toSubgraph_mapLe, SimpleGraph.Walk.toSubgraph, SimpleGraph.sup_adj, SimpleGraph.edge_adj, SimpleGraph.completeGraph_eq_top, SimpleGraph.Subgraph.spanningCoe_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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.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:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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

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
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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)
this : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe
⊢ c.IsCycle

Tactic:
simp [Walk.cons_isCycle_iff, c, hp, hs]

Premises used: SimpleGraph.Walk.cons_isCycle_iff