awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
hwu₁ : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
⊢ p.snd ≠ w

Tactic:
subst hww'
-- 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'
hwu₁ : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1₁ : p.snd ≠ w
⊢ G.Adj v w

Tactic:
subst hww'
-- 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'
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:
subst hww'
-- 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
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
simp : G.Adj w v ∧ ¬p.toSubgraph.Adj w v
⊢ (G \ p.toSubgraph.spanningCoe).Adj w v

Tactic:
simp only [sdiff_adj, Subgraph.spanningCoe_adj]

Premises used: SimpleGraph.sdiff_adj, SimpleGraph.Subgraph.spanningCoe_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
hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
⊢ G.Adj w v ∧ ¬p.toSubgraph.Adj w v

Tactic:
⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Subgraph.Adj.symm, And.intro
-- 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
hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
⊢ G.Adj w v ∧ ¬p.toSubgraph.Adj w v

Tactic:
exact ⟨hw'2.symm, fun h ↦ hnpvw' h.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
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
⊢ (G \ p.toSubgraph.spanningCoe).Adj w v

Tactic:
have : (G \ p.toSubgraph.spanningCoe).Adj w v := by
      simp only [sdiff_adj, Subgraph.spanningCoe_adj]
      exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩
-- 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
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
this : (G \ p.toSubgraph.spanningCoe).Adj w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
this.reachable

Premises used: SimpleGraph.Adj.reachable
-- 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
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
this : (G \ p.toSubgraph.spanningCoe).Adj w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
exact this.reachable

Premises used: SimpleGraph.Adj.reachable
-- 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'
⊢ G ≤ G

Tactic:
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
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'
hcd : p.toSubgraph.spanningCoe ≤ (Walk.cons ⋯ p).toSubgraph.spanningCoe
⊢ G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe

Tactic:
apply sdiff_le_sdiff (by rfl) ?hcd

Premises used: sdiff_le_sdiff
-- 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'
⊢ p.toSubgraph.spanningCoe ≤ (Walk.cons ⋯ p).toSubgraph.spanningCoe

Tactic:
simp
-- 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'
⊢ G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe

Tactic:
have hle : (G \ (p.cons hw'2.symm).toSubgraph.spanningCoe) ≤ (G \ p.toSubgraph.spanningCoe) := by
    apply sdiff_le_sdiff (by rfl) ?hcd
    simp
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
rw : p.IsPath ∧ w' ∉ p.support
⊢ (Walk.cons ⋯ p).IsPath

Tactic:
rw [Walk.cons_isPath_iff]

Premises used: SimpleGraph.Walk.cons_isPath_iff
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ p.IsPath ∧ w' ∉ p.support

Tactic:
⟨hp, fun hw' ↦ ?_⟩

Premises used: And.intro
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
refine : ∀ (hw' : w' ∈ p.support), False
⊢ p.IsPath ∧ w' ∉ p.support

Tactic:
refine ⟨hp, fun hw' ↦ ?_⟩
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hw' : w' ∈ p.support
⊢ False

Tactic:
hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)

Premises used: SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_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'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hw' : w' ∈ p.support
⊢ False

Tactic:
exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)

Premises used: SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_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'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ (Walk.cons ⋯ p).IsPath

Tactic:
have hp'p : (p.cons hw'2.symm).IsPath := by
    rw [Walk.cons_isPath_iff]
    refine ⟨hp, fun hw' ↦ ?_⟩
    exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
simp : G.Adj w' v ∧ ¬p.toSubgraph.Adj w' v
⊢ (G \ p.toSubgraph.spanningCoe).Adj w' v

Tactic:
simp only [sdiff_adj, Subgraph.spanningCoe_adj]

Premises used: SimpleGraph.sdiff_adj, SimpleGraph.Subgraph.spanningCoe_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'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
⊢ G.Adj w' v ∧ ¬p.toSubgraph.Adj w' v

Tactic:
⟨hw'2.symm, fun h ↦ ?_⟩

Premises used: SimpleGraph.Adj.symm, And.intro
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
refine : ∀ (h : p.toSubgraph.Adj w' v), False
⊢ G.Adj w' v ∧ ¬p.toSubgraph.Adj w' v

Tactic:
refine ⟨hw'2.symm, fun 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'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
h : p.toSubgraph.Adj w' v
⊢ False

Tactic:
hnpvw' h.symm

Premises used: SimpleGraph.Subgraph.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
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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
h : p.toSubgraph.Adj w' v
⊢ False

Tactic:
exact hnpvw' h.symm

Premises used: SimpleGraph.Subgraph.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
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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Adj w' v

Tactic:
have : (G \ p.toSubgraph.spanningCoe).Adj w' v := by
    simp only [sdiff_adj, Subgraph.spanningCoe_adj]
    refine ⟨hw'2.symm, fun h ↦ ?_⟩
    exact hnpvw' h.symm
-- 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'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
val : (G \ p.toSubgraph.spanningCoe).Walk w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
use (((hcyc.reachable_sdiff_toSubgraph_spanningCoe_aux
    (p.cons hw'2.symm) hp'p).some).mapLe hle).append this.toWalk

Premises used: SimpleGraph.Adj.toWalk, SimpleGraph.Adj.symm, Nonempty.some, SimpleGraph.Walk.cons, SimpleGraph.Walk.mapLe, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
h :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y _x →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
v : V
p_1 : (p : G.Walk v w) ×' p.IsPath
h_1 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v p_1) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
h_2 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y
        (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v
          (PSigma.mk (β := fun (p : G.Walk v w) ↦ p.IsPath) p hp)) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h_3 : (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this : (G \ p.toSubgraph.spanningCoe).Adj w' v
have : ∀ (this : Fintype V), Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length

Tactic:
have := Fintype.ofFinite V
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
h :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y _x →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
v : V
p_1 : (p : G.Walk v w) ×' p.IsPath
h_1 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v p_1) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
h_2 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y
        (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v
          (PSigma.mk (β := fun (p : G.Walk v w) ↦ p.IsPath) p hp)) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h_3 : (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this_1 : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
simp_wf : Fintype.card V - p.length < Fintype.card V + 1 - p.length
⊢ Nat.card V + 1 - (Walk.cons ⋯ p).length < Nat.card V + 1 - p.length

Tactic:
simp_wf
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
w : V
hcyc : G.IsCycles
_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath
h :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y _x →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
v : V
p_1 : (p : G.Walk v w) ×' p.IsPath
h_1 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v p_1) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
p : G.Walk v w
hp : p.IsPath
h_2 :
  ∀ (y : (v : V) ×' (p : G.Walk v w) ×' p.IsPath),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦
          PSigma.casesOn (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) (motive :=
            fun (_x : (v : V) ×' (p : G.Walk v w) ×' p.IsPath) ↦ ℕ) x fun (v : V) (p : (p : G.Walk v w) ×' p.IsPath) ↦
            PSigma.casesOn (β := fun (p : G.Walk v w) ↦ p.IsPath) (motive := fun (p : (p : G.Walk v w) ×' p.IsPath) ↦ ℕ)
              p fun (p : G.Walk v w) (hp : p.IsPath) ↦ Nat.card V + 1 - p.length)
        y
        (PSigma.mk (β := fun {v : V} ↦ (p : G.Walk v w) ×' p.IsPath) v
          (PSigma.mk (β := fun (p : G.Walk v w) ↦ p.IsPath) p hp)) →
      (G \ Subgraph.spanningCoe (G := G) (Walk.toSubgraph (u := y.1) (v := w) y.2.1)).Reachable w y.1
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
h_3 : (fun (w' : V) ↦ p.snd ≠ w' ∧ G.Adj v w') w' ∧ ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
left : p.snd ≠ w' ∧ G.Adj v w'
hwu : ∀ (y : V), p.snd ≠ y ∧ G.Adj v y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
this_1 : (G \ p.toSubgraph.spanningCoe).Adj w' v
this : Fintype V
⊢ p.length < Fintype.card V

Tactic:
have := Walk.IsPath.length_lt hp