awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles

Tactic:
exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs])
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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

Tactic:
fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)

Premises used: SimpleGraph.neighborSet, Nonempty.some, SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv, Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
refine : ∀ (w : V), Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet v) : Type u_1))
⊢ ∀ (w : V), p.toSubgraph.Adj v w ↔ G.Adj v w

Tactic:
refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)

Premises used: SimpleGraph.neighborSet, Nonempty.some, SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv, Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ v ∈ p.support

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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.neighborSet v).ncard = 2

Tactic:
have := hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
⊢ (p.toSubgraph.neighborSet v).ncard ≠ 0

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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})
rw₄ rw₅ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1} ((↑(G.neighborSet v) : Type u_1) ≃ (↑(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]

Premises used: SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.finite_neighborSet_toSubgraph, Set.Nonempty.mono, Set.toFinite, Set.nonempty_of_ncard_ne_zero, Cardinal.eq, Set.cast_ncard, SimpleGraph.Subgraph.neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v : V
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
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Tactic:
obtain ⟨w, hw⟩ := hM.1 (hM.2 v)

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
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
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

Tactic:
obtain ⟨w', hw'⟩ := hM'.1 (hM'.2 v)

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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'
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}
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2

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]

Premises used: symmDiff_def, Classical.not_not, Set.ncard_eq_two, Set.not_nonempty_iff_eq_empty, SimpleGraph.sup_adj, SimpleGraph.mem_neighborSet, ne_eq, imp_iff_not_or, not_or, SimpleGraph.sdiff_adj, Set.eq_empty_iff_forall_notMem, SimpleGraph.Subgraph.spanningCoe_adj, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
pos :
  ∀ (hww' : w = w'),
    (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
      ∃ (x : V) (y : V),
        ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
neg :
  ∀ (hww' : ¬w = w'),
    (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
      ∃ (x : V) (y : V),
        ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
⊢ (∀ (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'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
hww' : w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
simp_all [← imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
neg :
  ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
h : ¬w = w' ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {w, w'}
⊢ ∃ (x : V) (y : V), ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
use w, w'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun (w : V) ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ ¬w = w' ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {w, w'}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
⊢ p.snd = w'

Tactic:
apply hp.snd_of_toSubgraph_adj

Premises used: SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hw'

Premises used: SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
hw'₁ : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length
⊢ p.IsPath

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hw'

Premises used: SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
hw'₁ : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length
hp₁ : p.IsPath
⊢ G.Adj v w'

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hw'

Premises used: SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length
hp : p.IsPath
hadj : G.Adj v w'
obtain :
  ∀ (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)), p.toSubgraph.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v w'

Tactic:
obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
pos : ∀ (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
neg : ∀ (hn : ¬(n = 0 ∨ n = p.length)), p.toSubgraph.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
by_cases hn : n = 0 ∨ n = p.length

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : n = 0 ∨ n = p.length
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
refine :
  Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))
⊢ (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)

Tactic:
refine @Classical.ofNonempty _ ?_

Premises used: Classical.ofNonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ n < p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
rw :
  Cardinal.mk (↑(G.neighborSet (p.getVert n)) : Type u_1) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₁ :
  (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) =
    Cardinal.mk (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
rw₂ :
  Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
    (↑(p.toSubgraph.neighborSet (p.getVert n)).ncard : Cardinal.{u_1})
rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑(G.neighborSet (p.getVert n)).ncard : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
rw₄ rw₅ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) (↑2 : Cardinal.{u_1})
⊢ Nonempty.{u_1 + 1}
    ((↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1))

Tactic:
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two, Set.toFinite, Cardinal.eq, Set.cast_ncard, Set.nonempty_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
neg :
  ∀ (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
    p.toSubgraph.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
neg : G.Adj (p.getVert n) v
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]

Premises used: SimpleGraph.Subgraph.adj_comm, SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv, Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
⊢ G.Adj (p.getVert n) v

Tactic:
hadj.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)
⊢ G.Adj (p.getVert n) v

Tactic:
exact hadj.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
apply : p.toSubgraph.Adj v w'
apply₁ : ∀ (hw' : ∃ (n : ℕ), p.getVert n = w' ∧ n ≤ p.length) (hp : p.IsPath) (hadj : G.Adj v w'), p.toSubgraph.Adj v w'
apply₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n)),
    p.toSubgraph.Adj v (p.getVert n)
pos :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : n = 0 ∨ n = p.length), p.toSubgraph.Adj v (p.getVert n)
neg neg₁ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : ¬(n = 0 ∨ n = p.length)), p.toSubgraph.Adj v (p.getVert n)
neg₂ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : ¬(n = 0 ∨ n = p.length))
    (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
    p.toSubgraph.Adj v (p.getVert n)
neg₃ :
  ∀ (hp : p.IsPath) (n : ℕ) (hnl : n ≤ p.length) (hw : w ≠ p.getVert n) (hadj : G.Adj v (p.getVert n))
    (hn : ¬(n = 0 ∨ n = p.length))
    (e : (↑(G.neighborSet (p.getVert n)) : Type u_1) ≃ (↑(p.toSubgraph.neighborSet (p.getVert n)) : Type u_1)),
    G.Adj (p.getVert n) v
⊢ p.snd = w'

Tactic:
classical
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj, SimpleGraph.Walk.length, SimpleGraph.Subgraph.adj_comm, rfl, SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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 : ∀ (hvw : ¬v = w), (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
by_cases hvw : v = w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : v = w
pos : ∀ (p : G.Walk v v) (hp : p.IsPath), (G \ p.toSubgraph.spanningCoe).Reachable v v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
subst hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v : V
hcyc : G.IsCycles
p : G.Walk v v
hp : p.IsPath
val : (G \ p.toSubgraph.spanningCoe).Walk v v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable v v

Tactic:
use .nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
⊢ ¬p.Nil

Tactic:
have hpn : ¬p.Nil := Walk.not_nil_of_ne hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
neg :
  ∀ (w' : V) (hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w') (hw'1 : p.snd ≠ w')
    (hw'2 : G.Adj v w'), (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
obtain ⟨w', ⟨hw'1, hw'2⟩, hwu⟩ := hcyc.existsUnique_ne_adj
    (p.toSubgraph_adj_snd hpn).adj_sub

Premises used: SimpleGraph.Walk.toSubgraph_adj_snd, SimpleGraph.Subgraph.Adj.adj_sub, SimpleGraph.IsCycles.existsUnique_ne_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
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'
h : p.toSubgraph.Adj v w'
⊢ False

Tactic:
hw'1 (hp.snd_of_toSubgraph_adj h)

Premises used: SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
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'
h : p.toSubgraph.Adj v w'
⊢ False

Tactic:
exact hw'1 (hp.snd_of_toSubgraph_adj h)

Premises used: SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
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'
⊢ ¬p.toSubgraph.Adj v w'

Tactic:
have hnpvw' : ¬ p.toSubgraph.Adj v w' := by
    intro h
    exact hw'1 (hp.snd_of_toSubgraph_adj h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
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'
pos : ∀ (hww' : w = w'), (G \ p.toSubgraph.spanningCoe).Reachable w v
neg : ∀ (hww' : ¬w = w'), (G \ p.toSubgraph.spanningCoe).Reachable w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
by_cases hww' : w = w'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
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'
⊢ ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w

Tactic:
subst hww'