awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
⊢ w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet
have refine : ∀ (hw : w.edgeSet ⊆ G'.edgeSet), w.toSubgraph ≤ G'
Tactic: refine ⟨fun hw e he ↦ Subgraph.edgeSet_mono hw <| w.mem_edges_toSubgraph.mpr he, fun hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
⊢ w.toSubgraph ≤ G'
have refine : ∀ (v' : V) (hv' : v' ∈ w.toSubgraph.verts), v' ∈ G'.verts
Tactic: refine ⟨fun v' hv' ↦ ?_, fun u' v' hadj ↦ hw <| w.mem_edges_toSubgraph.mp (hadj : s(_, _) ∈ _)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : v' ∈ w.toSubgraph.verts
⊢ v' ∈ G'.verts
have hv'₁ : ∃ e ∈ w.edges, v' ∈ e
Tactic: rw [mem_verts_toSubgraph, mem_support_iff_exists_mem_edges_of_not_nil hnil] at hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
⊢ v' ∈ G'.verts
have have : ∀ (e : Sym2 V) (he : e ∈ w.edges) (hv'e : v' ∈ e), v' ∈ G'.verts
Tactic: have ⟨e, he, hv'e⟩ := hv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst : DecidableEq V
⊢ p.bypass.toSubgraph ≤ p.toSubgraph
have left : p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst : DecidableEq V
left : p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts
⊢ p.bypass.toSubgraph ≤ p.toSubgraph
have right : ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 v v_2 : V
h : G.Adj u v_2
w : G.Walk v_2 v
⊢ Walk.map (cons h w).toSubgraph.hom (cons h w).mapToSubgraph = cons h w
have rw : cons sorry (Walk.map ((cons h w).toSubgraph.hom.comp (Subgraph.inclusion sorry)) w.mapToSubgraph) = cons h w
Tactic: rw [mapToSubgraph, Walk.map, map_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ Walk.map
      (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) ⋯) ⋯)
      (cons hadj w).mapToSubgraph =
    Walk.induce s (cons hadj w) hs
have rw : 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) sorry) sorry :
        (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 sorry) : V) sorry))
    sorry
    (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) sorry) sorry)
        (Subgraph.inclusion sorry))
      w.mapToSubgraph) =
  Walk.induce s (cons hadj w) hs
Tactic: rw [mapToSubgraph, map_cons, map_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless
have 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)
Tactic: simp_rw [Subgraph.IsInduced, IsChordless, IsChord, Sym2.forall, Sym2.lift_mk, G.mem_edgeSet,
    mem_verts_toSubgraph, adj_toSubgraph_iff_mem_edges]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.neighborSet u = {p.snd}
have hadj1 : p.toSubgraph.Adj u p.snd
Tactic: have hadj1 := p.toSubgraph_adj_snd hnp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ p.toSubgraph.neighborSet u = {p.snd}
have h : ∀ (v_1 : V), v_1 ∈ p.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd} v_1
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ v ∈ p.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd} v
have 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
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]
Cleared hypotheses: hadj1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ ¬p.reverse.Nil
have rw : 0 < p.length
Tactic: rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
have hadj1 : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
have 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
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ Membership.mem (γ := Set V) {p.getVert (i - 1), p.getVert (i + 1)} v
have 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)
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]
Cleared hypotheses: h, h', hadj1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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_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)
have 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)
Tactic: refine ⟨?_, by aesop⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
have hl₁ : i' = i
Tactic: apply hp.getVert_injOn (by rw [Set.mem_setOf_eq]; lia)
      (by rw [Set.mem_setOf_eq]; lia) at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
have hl₁ : i' + 1 = i
Tactic: apply hp.getVert_injOn (by rw [Set.mem_setOf_eq]; lia)
      (by rw [Set.mem_setOf_eq]; lia) at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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.neighborSet (p.getVert i)).ncard = 2
have rw : Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2
Tactic: rw [hp.neighborSet_toSubgraph_internal h h']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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)
⊢ False
have this : i - 1 = i + 1
Tactic: have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; lia) (by rw [Set.mem_setOf_eq]; lia) h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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'
⊢ p.snd = v'
have have : ∀ (i : ℕ) (hi : s(p.getVert i, p.getVert (i + 1)) = s(u, v') ∧ i < p.length), p.snd = v'
Tactic: have ⟨i, hi⟩ := p.toSubgraph_adj_iff.mp hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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.snd = v'
have hi₁ : (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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ p.snd = v'
have 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)
Tactic: rcases hi.1 with ⟨hl1, rfl⟩ | ⟨hr1, hr2⟩
Cleared hypotheses: v', hadj, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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)
⊢ p.snd = v'
have inr : ∀ (hr1 : p.getVert i = v') (hr2 : p.getVert (i + 1) = u), p.snd = v'
Tactic: rcases hi.1 with ⟨hl1, rfl⟩ | ⟨hr1, hr2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
have apply : p.getVert i = p.getVert 0
Tactic: apply hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by rw [Set.mem_setOf]; lia)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ p.getVert i = p.getVert 0
have rw₁ : u = u
Tactic: rw [p.getVert_zero, hl1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ p.snd = p.getVert (i + 1)
have this : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
have apply : p.getVert (i + 1) = p.getVert 0
Tactic: apply hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by rw [Set.mem_setOf]; lia)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ p.getVert (i + 1) = p.getVert 0
have rw₁ : u = u
Tactic: rw [p.getVert_zero, hr2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ p.snd = v'
have this : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.neighborSet u = {p.snd, p.penultimate}
have hadj1 : p.toSubgraph.Adj u p.snd
Tactic: have hadj1 := p.toSubgraph_adj_snd hpc.not_nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
⊢ p.toSubgraph.neighborSet u = {p.snd, p.penultimate}
have h : ∀ (v : V), v ∈ p.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd, p.penultimate} v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ v ∈ p.toSubgraph.neighborSet u ↔ Membership.mem (γ := Set V) {p.snd, p.penultimate} v
have 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
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]
Cleared hypotheses: hadj1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
have hadj1 : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
have h₁ : ∀ (v : V),
  v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ Membership.mem (γ := Set V) {p.getVert (i - 1), p.getVert (i + 1)} v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ Membership.mem (γ := Set V) {p.getVert (i - 1), p.getVert (i + 1)} v
have 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)
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]
Cleared hypotheses: h, h', hadj1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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_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)
have 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)
Tactic: refine ⟨?_, by aesop⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
have hl1₁ : i' = i
Tactic: apply hpc.getVert_injOn' (by rw [Set.mem_setOf_eq]; lia)
      (by rw [Set.mem_setOf_eq]; lia) at hl1
Cleared hypotheses: hl1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
have hr2₁ : i' + 1 = i
Tactic: apply hpc.getVert_injOn (by rw [Set.mem_setOf_eq]; lia)
      (by rw [Set.mem_setOf_eq]; lia) at hr2
Cleared hypotheses: hr2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : v ∈ p.support
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have h₁ : ∃ (n : ℕ), p.getVert n = v ∧ n ≤ p.length
Tactic: simp only [SimpleGraph.Walk.mem_support_iff_exists_getVert] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have obtain : ∀ (i : ℕ) (hi : p.getVert i = v ∧ i ≤ p.length), (p.toSubgraph.neighborSet v).ncard = 2
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have pos : ∀ (he : i = 0 ∨ i = p.length), (p.toSubgraph.neighborSet v).ncard = 2
Tactic: by_cases! he : i = 0 ∨ i = p.length