awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
h_1 : i < p.support.length
h_2 : j < p.support.length
h_3 : i < j
h_4 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i h_1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j h_2
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
this : ¬p'.Nil
⊢ False
have this₁ : p'.IsSubwalk p
Tactic: have : p'.IsSubwalk p := isSubwalk_drop _ i |>.trans <| p.isSubwalk_take j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
have refine : ∀ (h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle), p.IsPath
Tactic: refine ⟨by grind [isPath_iff_isSubwalk_imp_nil, IsCycle.not_nil], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
⊢ (cons hadj p).IsPath
have hp : p.IsPath
Tactic: have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
⊢ (cons hadj p).IsPath
have refine_1 : ∀ (hup : u ∈ p.support), (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)
Tactic: refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
refine_1 : ∀ (hup : u ∈ p.support), (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)
⊢ (cons hadj p).IsPath
have refine_2 : ∀ (hup : u ∈ p.support), (cons hadj (p.takeUntil u hup)).IsCycle
Tactic: refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)
have refine_1 : u :: (p.takeUntil u hup).support <:+: u :: p.support
Tactic: rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v v_2 : V
hadj : G.Adj u v_2
p : G.Walk v_2 v
ht : (cons hadj p).IsTrail
h : ∀ (v_3 : V) (w : G.Walk v_3 v_3), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsCycle
have refine_2 : ∀ (he : s(u, v_2) ∈ (p.takeUntil u hup).edges), False
Tactic: refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Path v v
⊢ p = Path.nil
have nil : ∀ (h : Walk.IsPath.{u} (V := V) (G := G) (u := v) Walk.nil),
  Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) Walk.nil h = Path.nil
Tactic: obtain ⟨_ | _, h⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Path v v
nil :
  ∀ (h : Walk.IsPath.{u} (V := V) (G := G) (u := v) Walk.nil),
    Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) Walk.nil h = Path.nil
⊢ p = Path.nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 v) (h_1 : (Walk.cons h p).IsPath),
  Subtype.mk (p := fun (p : G.Walk v v) ↦ p.IsPath) (Walk.cons h p) h_1 = Path.nil
Tactic: obtain ⟨_ | _, h⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u u' v v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).bypass = p.bypass.copy hu hv
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).bypass = p.bypass.copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.bypass.IsPath
⊢ IsPath.{u} (V := V) (G := G) (u := u_1) (v := w)
    (if hs : u_1 ∈ p'.bypass.support then p'.bypass.dropUntil u_1 hs else cons h p'.bypass)
have pos : ∀ (hs : u_1 ∈ p'.bypass.support), (p'.bypass.dropUntil u_1 hs).IsPath
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.bypass.IsPath
pos : ∀ (hs : u_1 ∈ p'.bypass.support), (p'.bypass.dropUntil u_1 hs).IsPath
⊢ IsPath.{u} (V := V) (G := G) (u := u_1) (v := w)
    (if hs : u_1 ∈ p'.bypass.support then p'.bypass.dropUntil u_1 hs else cons h p'.bypass)
have neg : ∀ (hs : u_1 ∉ p'.bypass.support), (cons h p'.bypass).IsPath
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.bypass.IsPath
have nil : ∀ {u : V}, IsPath.{u} (V := V) (G := G) (u := u) (bypass nil)
Tactic: induction p with
  | nil => simp!
  | cons _ p' ih =>
    simp only [bypass]
    split_ifs with hs
    · exact ih.dropUntil hs
    · simp [*, cons_isPath_iff]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, IsPath.{u} (V := V) (G := G) (u := u) (bypass Walk.nil)
⊢ p.bypass.IsPath
have cons : ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w) (ih : p'.bypass.IsPath), (cons h p').bypass.IsPath
Tactic: induction p with
  | nil => simp!
  | cons _ p' ih =>
    simp only [bypass]
    split_ifs with hs
    · exact ih.dropUntil hs
    · simp [*, cons_isPath_iff]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
⊢ length.{u} (V := V) (G := G) (u := u_1) (v := w)
      (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ≤
    (cons h p).length
have pos : ∀ (h_1 : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
pos : ∀ (h_1 : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length
⊢ length.{u} (V := V) (G := G) (u := u_1) (v := w)
      (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ≤
    (cons h p).length
have neg : u_1 ∉ p.bypass.support → (cons h p.bypass).length ≤ (cons h p).length
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∈ p.bypass.support
⊢ (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length
have trans : (p.bypass.dropUntil u_1 h_1).length ≤ p.bypass.length
Tactic: trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∈ p.bypass.support
trans : (p.bypass.dropUntil u_1 h_1).length ≤ p.bypass.length
⊢ (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length
have trans₁ : p.bypass.length ≤ (cons h p).length
Tactic: trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.length ≤ p.length
h_1 : u_1 ∈ p.bypass.support
trans : (p.bypass.dropUntil u_1 h_1).length ≤ p.bypass.length
trans₁ : p.bypass.length ≤ (cons h p).length
⊢ (p.bypass.dropUntil u_1 h_1).length ≤ (cons h p).length
have trans₂ : ℕ
Tactic: trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.bypass.length ≤ p.length
have nil : ∀ {u : V}, length.{u} (V := V) (G := G) (u := u) (bypass nil) ≤ length.{u} (V := V) (G := G) (u := u) (bypass nil)
Tactic: induction p with
  | nil => rfl
  | cons _ _ ih =>
    simp only [bypass]
    split_ifs
    · trans
      · apply length_dropUntil_le
      rw [length_cons]
      lia
    · rw [length_cons, length_cons]
      exact Nat.add_le_add_right ih 1
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    length.{u} (V := V) (G := G) (u := u) (bypass Walk.nil) ≤ length.{u} (V := V) (G := G) (u := u) (bypass Walk.nil)
⊢ p.bypass.length ≤ p.length
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.bypass.length ≤ p.length),
  (cons h p).bypass.length ≤ (cons h p).length
Tactic: induction p with
  | nil => rfl
  | cons _ _ ih =>
    simp only [bypass]
    split_ifs
    · trans
      · apply length_dropUntil_le
      rw [length_cons]
      lia
    · rw [length_cons, length_cons]
      exact Nat.add_le_add_right ih 1
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
⊢ (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h_1 p.bypass) = cons h_1 p
have pos : ∀ (hb : u_1 ∈ p.bypass.support), p.bypass.dropUntil u_1 hb = cons h_1 p
Tactic: split_ifs with hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
pos : ∀ (hb : u_1 ∈ p.bypass.support), p.bypass.dropUntil u_1 hb = cons h_1 p
⊢ (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h_1 p.bypass) = cons h_1 p
have neg : ∀ (hb : u_1 ∉ p.bypass.support), cons h_1 p.bypass = cons h_1 p
Tactic: split_ifs with hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
hb : u_1 ∈ p.bypass.support
⊢ p.bypass.dropUntil u_1 hb = cons h_1 p
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
hb : u_1 ∈ p.bypass.support
⊢ False
have h₁ : p.length + 1 ≤ (p.bypass.dropUntil u_1 sorry).length
Tactic: simp only [hb, Walk.bypass, Walk.length_cons, dif_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∈ p.bypass.support
h : p.length + 1 ≤ (p.bypass.dropUntil u_1 ⋯).length
⊢ False
have pos : p.length.succ ≤ p.length
Tactic: apply Nat.not_succ_le_self p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
h : (cons h_1 p).length ≤ (cons h_1 p).bypass.length
hb : u_1 ∉ p.bypass.support
⊢ cons h_1 p.bypass = cons h_1 p
have h₁ : p.length ≤ p.bypass.length
Tactic: simp only [hb, Walk.bypass, Walk.length_cons, not_false_iff, dif_neg,
        Nat.add_le_add_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p
hb : u_1 ∉ p.bypass.support
h : p.length ≤ p.bypass.length
⊢ cons h_1 p.bypass = cons h_1 p
have neg : cons h_1 p = cons h_1 p
Tactic: rw [ih h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.length ≤ p.bypass.length
⊢ p.bypass = p
have nil : ∀ {u : V} (h : length.{u} (V := V) (G := G) (u := u) nil ≤ length.{u} (V := V) (G := G) (u := u) (bypass nil)),
  Eq.{u + 1} (α := G.Walk u u) (bypass nil) nil
Tactic: induction p with
  | nil => rfl
  | cons h p ih =>
    simp only [Walk.bypass]
    split_ifs with hb
    · exfalso
      simp only [hb, Walk.bypass, Walk.length_cons, dif_pos] at h
      apply Nat.not_succ_le_self p.length
      calc p.length + 1
        _ ≤ (p.bypass.dropUntil _ _).length := h
        _ ≤ p.bypass.length := Walk.length_dropUntil_le p.bypass hb
        _ ≤ p.length := Walk.length_bypass_le _
    · simp only [hb, Walk.bypass, Walk.length_cons, not_false_iff, dif_neg,
        Nat.add_le_add_iff_right] at h
      rw [ih h]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.length ≤ p.bypass.length
nil :
  ∀ {u : V}
    (h : length.{u} (V := V) (G := G) (u := u) Walk.nil ≤ length.{u} (V := V) (G := G) (u := u) (bypass Walk.nil)),
    Eq.{u + 1} (α := G.Walk u u) (bypass Walk.nil) Walk.nil
⊢ p.bypass = p
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ (h : p.length ≤ p.bypass.length), p.bypass = p)
  (h_1 : (cons h p).length ≤ (cons h p).bypass.length), (cons h p).bypass = cons h p
Tactic: induction p with
  | nil => rfl
  | cons h p ih =>
    simp only [Walk.bypass]
    split_ifs with hb
    · exfalso
      simp only [hb, Walk.bypass, Walk.length_cons, dif_pos] at h
      apply Nat.not_succ_le_self p.length
      calc p.length + 1
        _ ≤ (p.bypass.dropUntil _ _).length := h
        _ ≤ p.bypass.length := Walk.length_dropUntil_le p.bypass hb
        _ ≤ p.length := Walk.length_bypass_le _
    · simp only [hb, Walk.bypass, Walk.length_cons, not_false_iff, dif_neg,
        Nat.add_le_add_iff_right] at h
      rw [ih h]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
⊢ support (G := G) (u := u_1) (v := w)
      (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ⊆
    u_1 :: p.support
have pos : ∀ (h : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h).support ⊆ u_1 :: p.support
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
pos : ∀ (h : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h).support ⊆ u_1 :: p.support
⊢ support (G := G) (u := u_1) (v := w)
      (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ⊆
    u_1 :: p.support
have neg : u_1 ∉ p.bypass.support → (cons h p.bypass).support ⊆ u_1 :: p.support
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
h_1 : u_1 ∈ p.bypass.support
⊢ (p.bypass.dropUntil u_1 h_1).support ⊆ u_1 :: p.support
have pos : p.bypass.support ⊆ u_1 :: p.support
Tactic: apply List.Subset.trans (support_dropUntil_subset _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.bypass.support ⊆ p.support
have nil : ∀ {u : V}, Subset.{u} (α := List V) (support (G := G) (u := u) (bypass nil)) (support (G := G) (u := u) nil)
Tactic: induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (support_dropUntil_subset _ _)
      apply List.subset_cons_of_subset
      assumption
    · rw [support_cons]
      apply List.cons_subset_cons
      assumption
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V}, Subset.{u} (α := List V) (support (G := G) (u := u) (bypass Walk.nil)) (support (G := G) (u := u) Walk.nil)
⊢ p.bypass.support ⊆ p.support
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.bypass.support ⊆ p.support),
  (cons h p).bypass.support ⊆ (cons h p).support
Tactic: induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (support_dropUntil_subset _ _)
      apply List.subset_cons_of_subset
      assumption
    · rw [support_cons]
      apply List.cons_subset_cons
      assumption
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
⊢ darts (u := u_1) (v := w) (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ⊆
    { fst := u_1, snd := v_1, adj := h : G.Dart } :: p.darts
have pos : ∀ (h_1 : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h_1).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
pos :
  ∀ (h_1 : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h_1).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
⊢ darts (u := u_1) (v := w) (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ⊆
    { fst := u_1, snd := v_1, adj := h : G.Dart } :: p.darts
have neg : u_1 ∉ p.bypass.support → (cons h p.bypass).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
h_1 : u_1 ∈ p.bypass.support
⊢ (p.bypass.dropUntil u_1 h_1).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
have pos : p.bypass.darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
Tactic: apply List.Subset.trans (darts_dropUntil_subset _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.bypass.darts ⊆ p.darts
have nil : ∀ {u : V}, Subset.{u} (α := List G.Dart) (darts (u := u) (bypass nil)) (darts (u := u) nil)
Tactic: induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (darts_dropUntil_subset _ _)
      apply List.subset_cons_of_subset _ ih
    · rw [darts_cons]
      exact List.cons_subset_cons _ ih
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Subset.{u} (α := List G.Dart) (darts (u := u) (bypass Walk.nil)) (darts (u := u) Walk.nil)
⊢ p.bypass.darts ⊆ p.darts
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.bypass.darts ⊆ p.darts),
  (cons h p).bypass.darts ⊆ (cons h p).darts
Tactic: induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (darts_dropUntil_subset _ _)
      apply List.subset_cons_of_subset _ ih
    · rw [darts_cons]
      exact List.cons_subset_cons _ ih
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
⊢ (cons hvv' w).cycleBypass.edges ⊆ (cons hvv' w).edges
have dsimp : s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges
Tactic: dsimp only [cycleBypass, edges_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
⊢ s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges
have s : w.bypass.edges ⊆ w.edges
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
⊢ (cons hvv' w).cycleBypass.edges ⊆ (cons hvv' w).edges
have dsimp : s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges
Tactic: classical
    dsimp only [cycleBypass, edges_cons]
    gcongr
    exact edges_bypass_subset _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
dsimp : s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges
⊢ (cons hvv' w).cycleBypass.edges ⊆ (cons hvv' w).edges
have s : w.bypass.edges ⊆ w.edges
Tactic: classical
    dsimp only [cycleBypass, edges_cons]
    gcongr
    exact edges_bypass_subset _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).IsCycle
have refine_1 : ∀ (hvv' : s(v, v') ∈ w.bypass.edges), False
Tactic: refine ⟨⟨(bypass_isPath _).isTrail.cons _ fun hvv' ↦ ?_, by simp⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
refine_1 : ∀ (hvv' : s(v, v') ∈ w.bypass.edges), False
⊢ (cons hvv' w.bypass).IsCycle
have refine_2 : (cons hvv' w.bypass).support.tail.Nodup
Tactic: refine ⟨⟨(bypass_isPath _).isTrail.cons _ fun hvv' ↦ ?_, by simp⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv'_1 : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv'_1 w).IsCircuit
hvv' : s(v, v') ∈ w.bypass.edges
⊢ False
have hw₁ : w.IsTrail ∧ s(v, v') ∉ w.edges
Tactic: simp only [isCircuit_def, isTrail_cons, ne_eq, reduceCtorEq, not_false_eq_true,
        and_true] at hw
Cleared hypotheses: hw