awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ Ne (α := ℕ∞) 1 ⊤

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
refine : HAdd.hAdd (α := ℕ∞) 1 1 ≤ (Set.univ \ t).encard
⊢ 1 < (Set.univ \ t).encard

Tactic:
refine ENat.add_one_le_iff (by simp) |>.mp ?_

Premises used: ENat.add_one_le_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t ⊆ Set.univ

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
rw : HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V - t.encard
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ (Set.univ \ t).encard

Tactic:
rw [Set.encard_diff (by simp) (Set.finite_of_encard_eq_coe ht₁), Set.encard_univ]

Premises used: Set.encard_univ, Set.finite_of_encard_eq_coe, Set.encard_diff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard ≠ ⊤

Tactic:
simp [ht₁]
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
refine : t.encard + HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V - t.encard

Tactic:
refine ENat.le_sub_of_add_le_left (by simp [ht₁]) ?_

Premises used: ENat.le_sub_of_add_le_left
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ t.encard + HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V

Tactic:
add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_

Premises used: add_le_of_le_tsub_right_of_le, Order.add_one_le_of_lt, ENat.one_lt_card
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
refine : t.encard ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1
⊢ t.encard + HAdd.hAdd (α := ℕ∞) 1 1 ≤ ENat.card V

Tactic:
refine add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_

Premises used: add_le_of_le_tsub_right_of_le, Order.add_one_le_of_lt, ENat.one_lt_card
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
grw : ENat.card V - 1 - (↑1 : ℕ∞) ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1
⊢ t.encard ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1

Tactic:
grw [ht₁, ENat.coe_sub, hn]

Premises used: ENat.coe_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ ENat.card V - 1 - (↑1 : ℕ∞) ≤ ENat.card V - HAdd.hAdd (α := ℕ∞) 1 1

Tactic:
simp [add_assoc, one_add_one_eq_two, le_tsub_add]

Premises used: add_assoc, one_add_one_eq_two, le_tsub_add
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
⊢ 1 < (Set.univ \ t).encard

Tactic:
have : 1 < (Set.univ \ t).encard := by
    refine ENat.add_one_le_iff (by simp) |>.mp ?_
    rw [Set.encard_diff (by simp) (Set.finite_of_encard_eq_coe ht₁), Set.encard_univ]
    refine ENat.le_sub_of_add_le_left (by simp [ht₁]) ?_
    refine add_le_of_le_tsub_right_of_le (Order.add_one_le_of_lt ENat.one_lt_card) ?_
    grw [ht₁, ENat.coe_sub, hn]
    simp [add_assoc, one_add_one_eq_two, le_tsub_add]
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this_1 : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
refine_2 : ∀ (a b : V), a ∈ Set.univ \ t → b ∈ Set.univ \ t → ∀ (hne : a ≠ b), False
⊢ False

Tactic:
obtain ⟨a, b, _, _, hne⟩ := Set.one_lt_encard_iff.mp <| this

Premises used: Iff.mp, Set.one_lt_encard_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this_1 : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
a b : V
left : a ∈ Set.univ \ t
left_1 : b ∈ Set.univ \ t
hne : a ≠ b
⊢ (completeGraph V).Adj a b

Tactic:
simp [hne]
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this_1 : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
a b : V
left : a ∈ Set.univ \ t
left_1 : b ∈ Set.univ \ t
hne : a ≠ b
⊢ a ∈ t ∨ b ∈ t

Tactic:
have := @ht₂ a b (by simp [hne])
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this_1 : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = (↑(n - 1) : ℕ∞)
ht₂ : (completeGraph V).IsVertexCover t
this_2 : 1 < (Set.univ \ t).encard
a b : V
left : a ∈ Set.univ \ t
left_1 : b ∈ Set.univ \ t
hne : a ≠ b
this : a ∈ t ∨ b ∈ t
⊢ False

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
have :
  ∀ (f : G →g H) (hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)),
    G.vertexCoverNum ≤ H.vertexCoverNum
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
have ⟨f, hf⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
obtain :
  ∀ (s : Set W) (hs₁ : s.encard = H.vertexCoverNum) (hs₂ : H.IsVertexCover s), G.vertexCoverNum ≤ H.vertexCoverNum
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists H

Premises used: SimpleGraph.vertexCoverNum_exists
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
⊢ IsAntichain H.Adj sᶜ

Tactic:
have := H.isIndepSet_iff_isAntichain_adj.mp <| isIndepSet_compl_iff_isVertexCover.mpr hs₂
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this : IsAntichain H.Adj sᶜ
⊢ IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)

Tactic:
have : IsAntichain G.Adj (f ⁻¹' sᶜ) := this.preimage hf (fun _ _ hadj ↦ f.map_rel' hadj)
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this_1 : IsAntichain H.Adj sᶜ
this : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
⊢ G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' s)

Tactic:
have : G.IsVertexCover (f ⁻¹' s) :=
    isIndepSet_compl_iff_isVertexCover.mp <| G.isIndepSet_iff_isAntichain_adj.mpr this
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this_1 : IsAntichain H.Adj sᶜ
this_2 : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
this : G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' s)
grw : Set.encard.{u_1} (α := V) ((⇑f : (a : V) → W) ⁻¹' s) ≤ s.encard
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
grw [this.vertexCoverNum_le, ← hs₁]

Premises used: SimpleGraph.IsVertexCover.vertexCoverNum_le
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this_1 : IsAntichain H.Adj sᶜ
this_2 : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
this : G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' s)
⊢ ∀ ⦃x : V⦄,
    Membership.mem (γ := Set V) ((⇑f : (a : V) → W) ⁻¹' s) x →
      Membership.mem (α := W) s (({ toFun := (⇑f : (a : V) → W), inj' := hf : V ↪ W } : (a : V) → W) x : W)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this_1 : IsAntichain H.Adj sᶜ
this_2 : IsAntichain G.Adj ((⇑f : (a : V) → W) ⁻¹' sᶜ)
this : G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' s)
⊢ Set.encard.{u_1} (α := V) ((⇑f : (a : V) → W) ⁻¹' s) ≤ s.encard

Tactic:
exact Function.Embedding.encard_le <| Function.Embedding.mk f hf |>.subtypeMap (by simp)

Premises used: Function.Embedding.encard_le, Function.Embedding.mk, Function.Embedding.subtypeMap, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
IsContained.vertexCoverNum_le_vertexCoverNum ⟨f, hf⟩

Premises used: SimpleGraph.Copy.mk, Nonempty.intro, SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
⊢ G.vertexCoverNum ≤ G'.vertexCoverNum

Tactic:
(IsContained.of_le h).vertexCoverNum_le_vertexCoverNum

Premises used: SimpleGraph.IsContained.of_le, SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ≃g H
⊢ G.vertexCoverNum = H.vertexCoverNum

Tactic:
le_antisymm f.isContained.vertexCoverNum_le_vertexCoverNum
    f.symm.isContained.vertexCoverNum_le_vertexCoverNum

Premises used: SimpleGraph.Iso.isContained, le_antisymm, SimpleGraph.Iso.symm, SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ length.{u} (V := V) (G := G) (u := u) nil = 0

Tactic:
rfl

Premises used: SimpleGraph.Walk.length, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).length = p.length + 1

Tactic:
rfl

Premises used: SimpleGraph.Walk.length, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ (∃ (p : G.Walk u v), p.length = 0) ↔ u = v

Tactic:
⟨fun ⟨_, h⟩ ↦ (eq_of_length_eq_zero h), (· ▸ ⟨nil, rfl⟩)⟩

Premises used: SimpleGraph.Walk.eq_of_length_eq_zero, Eq.rec, _private.0.SimpleGraph.Walk.exists_length_eq_zero_iff.match_1, SimpleGraph.Walk.nil, Iff.intro, Exists.intro, Eq, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ support (G := G) (u := u) nil = [u]

Tactic:
rfl

Premises used: SimpleGraph.Walk.support, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).support = u :: p.support

Tactic:
rfl

Premises used: SimpleGraph.Walk.support, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : Ne.{u + 1} (α := List V) (support (G := G) (u := u) Walk.nil) []
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).support ≠ []
⊢ p.support ≠ []

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Ne.{u + 1} (α := List V) (support (G := G) (u := u) nil) []

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).support ≠ []

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G_1 : SimpleGraph V
u v w : V
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support ≠ []

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
nil : List.head (support (G := G) (u := a) Walk.nil) ⋯ = a
cons : ∀ {v : V} (h : G.Adj a v) (p : G.Walk v b), (Walk.cons h p).support.head ⋯ = a
⊢ p.support.head ⋯ = a

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
a : V
⊢ List.head (support (G := G) (u := a) nil) ⋯ = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
a b v : V
h : G.Adj a v
p : G.Walk v b
⊢ (cons h p).support.head ⋯ = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
nil : ∀ {u : V}, List.getLast (support (G := G) (u := u) Walk.nil) ⋯ = u
cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), p.support.getLast ⋯ = w → (Walk.cons h p).support.getLast ⋯ = w
⊢ p.support.getLast ⋯ = b

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
a b u : V
⊢ List.getLast (support (G := G) (u := u) nil) ⋯ = u

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
a b u v w : V
h : G.Adj u v
p : G.Walk v w
p_ih : p.support.getLast ⋯ = w
⊢ (cons h p).support.getLast ⋯ = w

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : u :: List.tail (support (G := G) (u := u) Walk.nil) = support (G := G) (u := u) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), u :: (Walk.cons h p).support.tail = (Walk.cons h p).support
⊢ u :: p.support.tail = p.support

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ u :: List.tail (support (G := G) (u := u) nil) = support (G := G) (u := u) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ u :: (cons h p).support.tail = (cons h p).support

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : support (G := G) (u := u) Walk.nil = u :: List.tail (support (G := G) (u := u) Walk.nil)
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).support = u :: (Walk.cons h p).support.tail
⊢ p.support = u :: p.support.tail

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ support (G := G) (u := u) nil = u :: List.tail (support (G := G) (u := u) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).support = u :: (cons h p).support.tail

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) u
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), u ∈ (Walk.cons h p).support
⊢ u ∈ p.support

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Membership.mem (γ := List V) (support (G := G) (u := u) nil) u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ u ∈ (cons h p).support

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) u
cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), w ∈ p.support → w ∈ (Walk.cons h p).support
⊢ v ∈ p.support

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u_1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : w ∈ p.support
⊢ w ∈ (cons h p).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Membership.mem (γ := Set V) {w : V | w ∈ p.support} u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil :
  Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w ↔
    w = u ∨ Membership.mem (γ := List V) (List.tail (support (G := G) (u := u) Walk.nil)) w
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
    w ∈ (Walk.cons h p).support ↔ w = u ∨ w ∈ (Walk.cons h p).support.tail
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u w : V
⊢ Membership.mem (γ := List V) (support (G := G) (u := u) nil) w ↔
    w = u ∨ Membership.mem (γ := List V) (List.tail (support (G := G) (u := u) nil)) w

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ w ∈ (cons h p).support ↔ w = u ∨ w ∈ (cons h p).support.tail

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ Membership.mem (γ := List V) (support (G := G) (u := v) nil) u ↔ u = v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
obtain : ∀ (w : V) (w_1 : G.Adj u w) (w_2 : G.Walk w v), v ∈ (cons w_1 w_2).support.tail
⊢ v ∈ p.support.tail

Tactic:
obtain ⟨_, _, _, rfl⟩ := exists_eq_cons_of_ne h p

Premises used: SimpleGraph.Walk.exists_eq_cons_of_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
w : V
w_1 : G.Adj u w
w_2 : G.Walk w v
⊢ v ∈ (cons w_1 w_2).support.tail

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hadj : G.Adj u v
⊢ p.support ⊆ (cons hadj p).support

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  (↑(support (G := G) (u := u) Walk.nil) : Multiset V) =
    HAdd.hAdd (α := Multiset V) {u} (↑(List.tail (support (G := G) (u := u) Walk.nil)) : Multiset V)
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
    (↑(Walk.cons h p).support : Multiset V) = {u} + (↑(Walk.cons h p).support.tail : Multiset V)
⊢ (↑p.support : Multiset V) = {u} + (↑p.support.tail : Multiset V)

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ (↑(support (G := G) (u := u) nil) : Multiset V) =
    HAdd.hAdd (α := Multiset V) {u} (↑(List.tail (support (G := G) (u := u) nil)) : Multiset V)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (↑(cons h p).support : Multiset V) = {u} + (↑(cons h p).support.tail : Multiset V)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w u : V
d : G.Dart
h : d.toProd.2 = u
⊢ List.IsChain G.DartAdj (d :: darts (u := u) nil)

Tactic:
.singleton _

Premises used: List.IsChain.singleton, SimpleGraph.Walk.darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w u : V
d : G.Dart
h : d.toProd.2 = u
⊢ List.IsChain G.DartAdj (d :: darts (u := u) nil)

Tactic:
exact .singleton _
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w u v_1 w_1 : V
h' : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ {d : G.Dart} (h : d.toProd.2 = v_1), List.IsChain G.DartAdj (d :: p.darts)
d : G.Dart
h : d.toProd.2 = u
⊢ List.IsChain G.DartAdj (d :: (cons h' p).darts)

Tactic:
.cons_cons h (ih rfl)

Premises used: List.IsChain.cons_cons, SimpleGraph.Walk.darts, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v w u v_1 w_1 : V
h' : G.Adj u v_1
p : G.Walk v_1 w_1
ih : ∀ {d : G.Dart} (h : d.toProd.2 = v_1), List.IsChain G.DartAdj (d :: p.darts)
d : G.Dart
h : d.toProd.2 = u
⊢ List.IsChain G.DartAdj (d :: (cons h' p).darts)

Tactic:
exact .cons_cons h (ih rfl)
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
d : G.Dart
v w : V
h : d.toProd.2 = v
p : G.Walk v w
nil : ∀ {u : V} {d : G.Dart} (h : d.toProd.2 = u), List.IsChain G.DartAdj (d :: darts (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h' : G.Adj u v) (p : G.Walk v w)
    (ih : ∀ {d : G.Dart} (h : d.toProd.2 = v), List.IsChain G.DartAdj (d :: p.darts)) {d : G.Dart} (h : d.toProd.2 = u),
    List.IsChain G.DartAdj (d :: (Walk.cons h' p).darts)
⊢ List.IsChain G.DartAdj (d :: p.darts)

Tactic:
induction p generalizing d with
  | nil => exact .singleton _
  | cons h' p ih => exact .cons_cons h (ih rfl)

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil