awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u v_1 v v_2 : V
hadj : G.Adj u v_2
w : G.Walk v_2 v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ cons (v :=
      (RelHom.mk (r := (cons hadj w).toSubgraph.coe.Adj) (s := (induce s G).Adj)
            (fun (x : (↑(cons hadj w).toSubgraph.verts : Type u)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ s) (↑x : V) ⋯)
            ⋯ :
          (a : (↑(cons hadj w).toSubgraph.verts : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ (cons hadj w).toSubgraph.verts)
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ w.toSubgraph.verts) v_2 ⋯) : V) ⋯))
      ⋯
      (Walk.map
        (Hom.comp
          (RelHom.mk (r := (cons hadj w).toSubgraph.coe.Adj) (s := (induce s G).Adj)
            (fun (x : (↑(cons hadj w).toSubgraph.verts : Type u)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ s) (↑x : V) ⋯) ⋯)
          (Subgraph.inclusion ⋯))
        w.mapToSubgraph) =
    Walk.induce s (cons hadj w) hs

Tactic:
congrArg _ <| w.map_mapToSubgraph_eq_induce s (hs · <| List.mem_of_mem_tail ·)

Premises used: congrArg, SimpleGraph.Walk.induce, List.mem_of_mem_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u v_1 v v_2 : V
hadj : G.Adj u v_2
w : G.Walk v_2 v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ cons (v :=
      (RelHom.mk (r := (cons hadj w).toSubgraph.coe.Adj) (s := (induce s G).Adj)
            (fun (x : (↑(cons hadj w).toSubgraph.verts : Type u)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ s) (↑x : V) ⋯)
            ⋯ :
          (a : (↑(cons hadj w).toSubgraph.verts : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ (cons hadj w).toSubgraph.verts)
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ w.toSubgraph.verts) v_2 ⋯) : V) ⋯))
      ⋯
      (Walk.map
        (Hom.comp
          (RelHom.mk (r := (cons hadj w).toSubgraph.coe.Adj) (s := (induce s G).Adj)
            (fun (x : (↑(cons hadj w).toSubgraph.verts : Type u)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ s) (↑x : V) ⋯) ⋯)
          (Subgraph.inclusion ⋯))
        w.mapToSubgraph) =
    Walk.induce s (cons hadj w) hs

Tactic:
exact congrArg _ <| w.map_mapToSubgraph_eq_induce s (hs · <| List.mem_of_mem_tail ·)

Premises used: congrArg, List.mem_of_mem_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ Eq (α :=
    Walk (V := (↑fun (x : V) ↦ List.Mem x w.support : Type u)) (induce (fun (x : V) ↦ List.Mem x w.support) G)
      ((RelHom.mk (r := w.toSubgraph.coe.Adj) (s := Adj (induce (fun (x : V) ↦ List.Mem x w.support) G))
            (fun (v_1 : (↑w.toSubgraph.verts : Type u)) ↦
              Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) (fun (x : V) ↦ List.Mem x w.support) x)
                (↑v_1 : V) ⋯)
            ⋯ :
          (a : (↑w.toSubgraph.verts : Type u)) → (↑fun (x : V) ↦ List.Mem x w.support : Type u))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ w.toSubgraph.verts) u ⋯))
      ((RelHom.mk (r := w.toSubgraph.coe.Adj) (s := Adj (induce (fun (x : V) ↦ List.Mem x w.support) G))
            (fun (v_1 : (↑w.toSubgraph.verts : Type u)) ↦
              Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) (fun (x : V) ↦ List.Mem x w.support) x)
                (↑v_1 : V) ⋯)
            ⋯ :
          (a : (↑w.toSubgraph.verts : Type u)) → (↑fun (x : V) ↦ List.Mem x w.support : Type u))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ w.toSubgraph.verts) v ⋯)))
    (Walk.map
      (RelHom.mk (r := w.toSubgraph.coe.Adj) (s := Adj (induce (fun (x : V) ↦ List.Mem x w.support) G))
        (fun (v_1 : (↑w.toSubgraph.verts : Type u)) ↦
          Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) (fun (x : V) ↦ List.Mem x w.support) x) (↑v_1 : V)
            ⋯)
        ⋯)
      w.mapToSubgraph)
    (Walk.induce (fun (x : V) ↦ List.Mem x w.support) w ⋯)

Tactic:
w.map_mapToSubgraph_eq_induce ..

Premises used: SimpleGraph.Walk.map_mapToSubgraph_eq_induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
simp_rw :
  (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → s(v_1, w_1) ∈ w.edges) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
simp_rw [Subgraph.IsInduced, IsChordless, IsChord, Sym2.forall, Sym2.lift_mk, G.mem_edgeSet,
    mem_verts_toSubgraph, adj_toSubgraph_iff_mem_edges]

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph, Sym2.forall, SimpleGraph.Subgraph.IsInduced, SimpleGraph.Walk.adj_toSubgraph_iff_mem_edges, SimpleGraph.Walk.IsChordless, Sym2.lift_mk, SimpleGraph.mem_edgeSet, SimpleGraph.Walk.IsChord
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → s(v_1, w_1) ∈ w.edges) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)

Tactic:
grind only
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.Adj u p.snd

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

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p : G.Walk u v_1
hp : p.IsPath
hnp : ¬p.Nil
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.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd} v

Tactic:
simp_all only [Subgraph.mem_neighborSet, 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
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p : G.Walk u v_1
hp : p.IsPath
hnp : ¬p.Nil
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

Tactic:
grind [getVert_eq_start_iff]

Premises used: SimpleGraph.Walk.IsPath.getVert_eq_start_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
rw : 0 < p.length
⊢ ¬p.reverse.Nil

Tactic:
rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length, SimpleGraph.Walk.length_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length

Tactic:
Walk.not_nil_iff_lt_length.mp hnp

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length

Tactic:
exact
        Walk.not_nil_iff_lt_length.mp hnp

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.neighborSet v = {p.penultimate}

Tactic:
simpa using IsPath.neighborSet_toSubgraph_startpoint hp.reverse
      (by rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]; exact
        Walk.not_nil_iff_lt_length.mp hnp)

Premises used: SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_startpoint, SimpleGraph.Walk.IsPath.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
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
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
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
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
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
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
h₁ :
  ∀ (v_1 : V),
    v_1 ∈ p.toSubgraph.neighborSet (p.getVert i) ↔
      Membership.mem (γ := Set V) {p.getVert (i - 1), p.getVert (i + 1)} v_1
⊢ 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
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
hl : p.getVert i' = p.getVert i
right_1 : p.getVert (i' + 1) = v
⊢ i' ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
hl : p.getVert i' = p.getVert i
right_1 : p.getVert (i' + 1) = v
⊢ i ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
hl : p.getVert i' = p.getVert i
right_1 : p.getVert (i' + 1) = v
⊢ i' = i

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

Premises used: SimpleGraph.Walk.IsPath.getVert_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
left : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
left : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
left : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 = i

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

Premises used: SimpleGraph.Walk.IsPath.getVert_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
right_1 : p.getVert (i' + 1) = v
hl : i' = 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
v_1 u : V
i : ℕ
p : G.Walk u v_1
hp : p.IsPath
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
left : p.getVert i' = v
hl : 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
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
rw : Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

Tactic:
rw [hp.neighborSet_toSubgraph_internal h h']

Premises used: SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h_1 : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h_1 : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h_1 : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 = i + 1

Tactic:
have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; lia) (by rw [Set.mem_setOf_eq]; lia) h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h_1 : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
this : i - 1 = i + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
have : p.getVert (i - 1) ≠ p.getVert (i + 1) := by
    intro h
    have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; lia) (by rw [Set.mem_setOf_eq]; lia) h
    lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
this : p.getVert (i - 1) ≠ p.getVert (i + 1)
⊢ Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2

Tactic:
simp_all
-- 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'
have : ∀ (i : ℕ) (hi : s(p.getVert i, p.getVert (i + 1)) = s(u, v') ∧ i < p.length), p.snd = v'
⊢ p.snd = v'

Tactic:
have ⟨i, hi⟩ := p.toSubgraph_adj_iff.mp hadj
-- 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 : s(p.getVert i, p.getVert (i + 1)) = s(u, v') ∧ i < p.length
⊢ (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hi

Premises used: Sym2.eq, Prod.swap_prod_mk, Sym2.rel_iff', Prod.mk.injEq
-- 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
inl :
  ∀ (hl1 : p.getVert i = u) (hadj : p.toSubgraph.Adj u (p.getVert (i + 1)))
    (hi :
      (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨
          p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
        i < p.length),
    p.snd = p.getVert (i + 1)
inr : ∀ (hr1 : p.getVert i = v') (hr2 : p.getVert (i + 1) = u), p.snd = v'
⊢ p.snd = v'

Tactic:
rcases hi.1 with ⟨hl1, rfl⟩ | ⟨hr1, hr2⟩

Premises used: And.left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    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 v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
apply : p.getVert i = p.getVert 0
⊢ i = 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
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
rw : p.getVert i = u
rw₁ rw₂ : u = u
⊢ p.getVert i = p.getVert 0

Tactic:
rw [p.getVert_zero, hl1]

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

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

Tactic:
simp [this]
-- 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 ≤ p.length

Tactic:
lia
-- 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
⊢ 0 ≤ p.length

Tactic:
lia