awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
apply : p.getVert (i + 1) = p.getVert 0
⊢ i + 1 = 0

Tactic:
apply hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by rw [Set.mem_setOf]; lia)

Premises used: SimpleGraph.Walk.IsPath.getVert_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 rw : p.getVert (i + 1) = u
rw₁ rw₂ : u = u
⊢ p.getVert (i + 1) = p.getVert 0

Tactic:
rw [p.getVert_zero, hr2]

Premises used: SimpleGraph.Walk.getVert_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ i + 1 = 0

Tactic:
have : i + 1 = 0 := by
      apply hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by rw [Set.mem_setOf]; lia)
      rw [p.getVert_zero, hr2]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
this : i + 1 = 0
⊢ p.snd = v'

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.Adj u p.snd

Tactic:
have hadj1 := p.toSubgraph_adj_snd hpc.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
h : ∀ (v : V), v ∈ p.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd, p.penultimate} v
⊢ p.toSubgraph.neighborSet u = {p.snd, p.penultimate}

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
v : V
h :
  ∀
    (hadj1 :
      ∃ (i : ℕ),
        (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length),
    (∃ (i : ℕ), (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔
      v = p.snd ∨ v = p.penultimate
⊢ v ∈ p.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd, p.penultimate} v

Tactic:
simp_all only [Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Premises used: Sym2.eq, SimpleGraph.Walk.toSubgraph_adj_iff, Prod.swap_prod_mk, SimpleGraph.Subgraph.mem_neighborSet, Sym2.rel_iff', Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 :
  ∃ (i : ℕ), (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
⊢ (∃ (i : ℕ), (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔
    v = p.snd ∨ v = p.penultimate

Tactic:
grind [getVert_endpoint_iff, add_tsub_cancel_right]

Premises used: SimpleGraph.Walk.IsCycle.getVert_endpoint_iff, add_tsub_cancel_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ i - 1 + 1 = i

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ i - 1 < p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))

Tactic:
have hadj1 := ((show i - 1 + 1 = i from by lia) ▸
    p.toSubgraph_adj_getVert (by lia : (i - 1) < p.length)).symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
h₁ :
  ∀ (v : V),
    v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ Membership.mem (γ := Set V) {p.getVert (i - 1), p.getVert (i + 1)} v
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
v : V
h₁ :
  ∀ (h : ¬i = 0) (h' : i < p.length)
    (hadj1 :
      ∃ (i_1 : ℕ),
        (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
            p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
          i_1 < p.length),
    (∃ (i_1 : ℕ),
        (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨
            p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
          i_1 < p.length) ↔
      v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
⊢ v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ Membership.mem (γ := Set V) {p.getVert (i - 1), p.getVert (i + 1)} v

Tactic:
simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
    Prod.swap_prod_mk]

Premises used: Sym2.eq, SimpleGraph.Walk.toSubgraph_adj_iff, Prod.swap_prod_mk, ne_eq, SimpleGraph.Subgraph.mem_neighborSet, Sym2.rel_iff', Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1) →
    ∃ (i_1 : ℕ),
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
h₁ :
  (∃ (i_1 : ℕ),
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
⊢ (∃ (i_1 : ℕ),
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) ↔
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
refine ⟨?_, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ≤ p.length - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i ≤ p.length - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' = i

Tactic:
apply hpc.getVert_injOn' (by rw [Set.mem_setOf_eq]; lia)
      (by rw [Set.mem_setOf_eq]; lia) at hl1

Premises used: SimpleGraph.Walk.IsCycle.getVert_injOn'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hl2 : p.getVert (i' + 1) = v
hl1 : i' = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i' + 1 ∧ i' + 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i ∧ i ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 = i

Tactic:
apply hpc.getVert_injOn (by rw [Set.mem_setOf_eq]; lia)
      (by rw [Set.mem_setOf_eq]; lia) at hr2

Premises used: SimpleGraph.Walk.IsCycle.getVert_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ (i_1 : ℕ),
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right : i' < p.length
hr1 : p.getVert i' = v
hr2 : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : v ∈ p.support
⊢ ∃ (n : ℕ), p.getVert n = v ∧ n ≤ p.length

Tactic:
simp only [SimpleGraph.Walk.mem_support_iff_exists_getVert] at h ⊢

Premises used: SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : ∃ (n : ℕ), p.getVert n = v ∧ n ≤ p.length
obtain : ∀ (i : ℕ) (hi : p.getVert i = v ∧ i ≤ p.length), (p.toSubgraph.neighborSet v).ncard = 2
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
pos : ∀ (he : i = 0 ∨ i = p.length), (p.toSubgraph.neighborSet v).ncard = 2
neg : ∀ (he : i ≠ 0 ∧ i ≠ p.length), (p.toSubgraph.neighborSet v).ncard = 2
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
by_cases! he : i = 0 ∨ i = p.length

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ u = v

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ u = v

Tactic:
have huv : u = v := by aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
pos : Set.ncard (α := V) {p.snd, p.penultimate} = 2
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
rw [← huv, hpc.neighborSet_toSubgraph_endpoint]

Premises used: SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ Set.ncard (α := V) {p.snd, p.penultimate} = 2

Tactic:
Set.ncard_pair hpc.snd_ne_penultimate

Premises used: SimpleGraph.Walk.IsCycle.snd_ne_penultimate, Set.ncard_pair
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ Set.ncard (α := V) {p.snd, p.penultimate} = 2

Tactic:
exact Set.ncard_pair hpc.snd_ne_penultimate

Premises used: SimpleGraph.Walk.IsCycle.snd_ne_penultimate, Set.ncard_pair
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ i < p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
neg : Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
rw [← hi.1, hpc.neighborSet_toSubgraph_internal he.1 (by lia)]

Premises used: And.left, SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_internal
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ i ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2

Tactic:
exact Set.ncard_pair (hpc.getVert_sub_one_ne_getVert_add_one (by lia))

Premises used: Set.ncard_pair, SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
⊢ w ∈ p.toSubgraph.neighborSet v

Tactic:
have : w ∈ p.toSubgraph.neighborSet v := hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ p.toSubgraph.neighborSet v
⊢ Membership.mem (γ := Set V) {p.snd, p.penultimate} w

Tactic:
rw [h.neighborSet_toSubgraph_endpoint] at this

Premises used: SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : Membership.mem (γ := Set V) {p.snd, p.penultimate} w
⊢ w = p.snd ∨ w = p.penultimate

Tactic:
push _ ∈ _ at this
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w = p.snd ∨ w = p.penultimate
inl : ∀ (hl : w = p.snd), ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
inr :
  ∀ (hr : w = p.penultimate), ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
obtain hl | hr := this
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hl : w = p.snd
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
⟨p, ⟨h, hl.symm, rfl⟩⟩

Premises used: And.intro, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hl : w = p.snd
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨p, ⟨h, hl.symm, rfl⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
h₁ : p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
use p.reverse

Premises used: SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ w = p.reverse.getVert 1

Tactic:
rw [penultimate, ← getVert_reverse] at hr

Premises used: SimpleGraph.Walk.getVert_reverse, SimpleGraph.Walk.penultimate
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
rw rw₁ : p.toSubgraph.verts = p.toSubgraph.verts
⊢ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
rw [toSubgraph_reverse _]

Premises used: SimpleGraph.Walk.toSubgraph_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨h.reverse, hr.symm, by rw [toSubgraph_reverse _]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
simp : ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅

Tactic:
simp only [← Finset.subset_empty]

Premises used: Finset.subset_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
h₁ :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
          ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅)
    {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = n),
    ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
induction hp : p.length + #s using Nat.strong_induction_on generalizing s v with | _ n ih

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
hp : p.length + #s = n
⊢ ∃ x ∈ s, x ∈ p.support

Tactic:
simp only [Finset.Nonempty, mem_filter] at h

Premises used: Finset.Nonempty, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
h : ∃ x ∈ s, x ∈ p.support
h₁ :
  ∀ (x : V) (hxs : x ∈ s) (hx : x ∈ p.support),
    ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
obtain ⟨x, hxs, hx⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h :
  ∀ (h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅),
    ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
h₁ :
  ∀ (h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty),
    ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
obtain h | h := Finset.eq_empty_or_nonempty {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}

Premises used: SimpleGraph.Walk.support, Membership.mem, SimpleGraph.Walk.takeUntil, Finset.erase, Finset.filter, Finset.eq_empty_or_nonempty