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 u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : p.reverse.toSubgraph = p.toSubgraph
⊢ (cons h p).reverse.toSubgraph = (cons h p).toSubgraph
have cons : p.toSubgraph ⊔ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1) = G.subgraphOfAdj h ⊔ p.toSubgraph
Tactic: simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : p.reverse.toSubgraph = p.toSubgraph
⊢ p.toSubgraph ⊔ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1) = G.subgraphOfAdj h ⊔ p.toSubgraph
have cons : G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 ⊔ p.toSubgraph = G.subgraphOfAdj h ⊔ p.toSubgraph
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : p.reverse.toSubgraph = p.toSubgraph
⊢ G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 ⊔ p.toSubgraph = G.subgraphOfAdj h ⊔ p.toSubgraph
have cons : G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 = G.subgraphOfAdj h
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : p.reverse.toSubgraph = p.toSubgraph
⊢ G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 = G.subgraphOfAdj h
have cons : ∀ (x : V), x ∈ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1).verts ↔ x ∈ (G.subgraphOfAdj h).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : p.reverse.toSubgraph = p.toSubgraph
cons : ∀ (x : V), x ∈ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1).verts ↔ x ∈ (G.subgraphOfAdj h).verts
⊢ G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 = G.subgraphOfAdj h
have cons₁ : ∀ (x x_1 : V), (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1).Adj x x_1 ↔ (G.subgraphOfAdj h).Adj x x_1
Tactic: ext
-- 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
⊢ p.reverse.toSubgraph = p.toSubgraph
have nil : ∀ {u : V}, Eq.{u + 1} (α := G.Subgraph) (Walk.toSubgraph (u := u) (reverse nil)) (Walk.toSubgraph (u := u) nil)
Tactic: induction p with
  | nil => simp
  | cons _ _ _ =>
    simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
    rw [sup_comm]
    congr
    ext <;> simp [-Set.bot_eq_empty]
Cleared hypotheses: p
-- 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
nil :
  ∀ {u : V},
    Eq.{u + 1} (α := G.Subgraph) (Walk.toSubgraph (u := u) (reverse Walk.nil)) (Walk.toSubgraph (u := u) Walk.nil)
⊢ p.reverse.toSubgraph = p.toSubgraph
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  p.reverse.toSubgraph = p.toSubgraph → (cons h p).reverse.toSubgraph = (cons h p).toSubgraph
Tactic: induction p with
  | nil => simp
  | cons _ _ _ =>
    simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
    rw [sup_comm]
    congr
    ext <;> simp [-Set.bot_eq_empty]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate u h).toSubgraph = c.toSubgraph
have rw : ((c.dropUntil u h).append (c.takeUntil u h)).toSubgraph = c.toSubgraph
Tactic: rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
rw : ((c.dropUntil u h).append (c.takeUntil u h)).toSubgraph = c.toSubgraph
⊢ (c.rotate u h).toSubgraph = c.toSubgraph
have rw₁ : (c.dropUntil u h).toSubgraph ⊔ (c.takeUntil u h).toSubgraph = c.toSubgraph
Tactic: rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
rw : ((c.dropUntil u h).append (c.takeUntil u h)).toSubgraph = c.toSubgraph
rw₁ : (c.dropUntil u h).toSubgraph ⊔ (c.takeUntil u h).toSubgraph = c.toSubgraph
⊢ (c.rotate u h).toSubgraph = c.toSubgraph
have rw₂ : (c.takeUntil u h).toSubgraph ⊔ (c.dropUntil u h).toSubgraph = c.toSubgraph
Tactic: rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
rw : ((c.dropUntil u h).append (c.takeUntil u h)).toSubgraph = c.toSubgraph
rw₁ : (c.dropUntil u h).toSubgraph ⊔ (c.takeUntil u h).toSubgraph = c.toSubgraph
rw₂ : (c.takeUntil u h).toSubgraph ⊔ (c.dropUntil u h).toSubgraph = c.toSubgraph
⊢ (c.rotate u h).toSubgraph = c.toSubgraph
have rw₃ : ((c.takeUntil u h).append (c.dropUntil u h)).toSubgraph = c.toSubgraph
Tactic: rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
rw : ((c.dropUntil u h).append (c.takeUntil u h)).toSubgraph = c.toSubgraph
rw₁ : (c.dropUntil u h).toSubgraph ⊔ (c.takeUntil u h).toSubgraph = c.toSubgraph
rw₂ : (c.takeUntil u h).toSubgraph ⊔ (c.dropUntil u h).toSubgraph = c.toSubgraph
rw₃ : ((c.takeUntil u h).append (c.dropUntil u h)).toSubgraph = c.toSubgraph
⊢ (c.rotate u h).toSubgraph = c.toSubgraph
have rw₄ : c.toSubgraph = c.toSubgraph
Tactic: rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
p : G.Walk u v
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph
have nil : ∀ {u : V}, Walk.toSubgraph (u := (f : (a : V) → V') u) (Walk.map f nil) = Subgraph.map f (Walk.toSubgraph (u := u) nil)
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
p : G.Walk u v
nil :
  ∀ {u : V},
    Walk.toSubgraph (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) =
      Subgraph.map f (Walk.toSubgraph (u := u) Walk.nil)
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph →
    (Walk.map f (cons h p)).toSubgraph = Subgraph.map f (cons h p).toSubgraph
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : (p.toSubgraph.neighborSet w).Finite
⊢ ((cons ha p).toSubgraph.neighborSet w).Finite
have cons : ((G.subgraphOfAdj ha).neighborSet w ∪ p.toSubgraph.neighborSet w).Finite
Tactic: rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : (p.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w ∪ p.toSubgraph.neighborSet w).Finite
have cons : ((G.subgraphOfAdj ha).neighborSet w).Finite
Tactic: refine Set.Finite.union ?_ ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
ha : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : (p.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w).Finite
have cons : Set.Finite (α := V) {u_1, v_1}
Tactic: refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (p.toSubgraph.neighborSet w).Finite
have nil : ∀ {u : V}, (Subgraph.neighborSet (G := G) (Walk.toSubgraph (u := u) nil) w).Finite
Tactic: induction p with
  | nil =>
    rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
    apply Set.toFinite
  | cons ha _ ih =>
    rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
    refine Set.Finite.union ?_ ih
    refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
    apply Set.toFinite
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil : ∀ {u : V}, (Subgraph.neighborSet (G := G) (Walk.toSubgraph (u := u) Walk.nil) w).Finite
⊢ (p.toSubgraph.neighborSet w).Finite
have cons : ∀ {u v w_1 : V} (ha : G.Adj u v) (p : G.Walk v w_1) (ih : (p.toSubgraph.neighborSet w).Finite),
  ((cons ha p).toSubgraph.neighborSet w).Finite
Tactic: induction p with
  | nil =>
    rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
    apply Set.toFinite
  | cons ha _ ih =>
    rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
    refine Set.Finite.union ?_ ih
    refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
    apply Set.toFinite
Cleared hypotheses: p
-- 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
⊢ p.toSubgraph ≤ Subgraph.induce ⊤ {v_1 : V | v_1 ∈ p.support}
have h : {v_1 : V | v_1 ∈ p.support} = p.toSubgraph.verts
Tactic: convert! Subgraph.le_induce_top_verts
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hxy : G.Adj u_1 v_1
i' : G.Walk v_1 w
ih : ∀ {i : ℕ} (hi : i < i'.length), i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
i : ℕ
hi : i < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert i) ((cons hxy i').getVert (i + 1))
have cons : ∀ (hi : 0 < (cons hxy i').length),
  (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (HAdd.hAdd (α := ℕ) 0 1))
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hxy : G.Adj u_1 v_1
i' : G.Walk v_1 w
ih : ∀ {i : ℕ} (hi : i < i'.length), i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
i : ℕ
hi : i < (Walk.cons hxy i').length
cons :
  ∀ (hi : 0 < (Walk.cons hxy i').length),
    (Walk.cons hxy i').toSubgraph.Adj ((Walk.cons hxy i').getVert 0)
      ((Walk.cons hxy i').getVert (HAdd.hAdd (α := ℕ) 0 1))
⊢ (Walk.cons hxy i').toSubgraph.Adj ((Walk.cons hxy i').getVert i) ((Walk.cons hxy i').getVert (i + 1))
have cons₁ : ∀ (n : ℕ) (hi : n + 1 < (Walk.cons hxy i').length),
  (Walk.cons hxy i').toSubgraph.Adj ((Walk.cons hxy i').getVert (n + 1)) ((Walk.cons hxy i').getVert (n + 1 + 1))
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hxy : G.Adj u_1 v_1
i' : G.Walk v_1 w
ih : ∀ {i : ℕ} (hi : i < i'.length), i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n : ℕ
hi : n + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n + 1)) ((cons hxy i').getVert (n + 1 + 1))
have cons : (u_1 = i'.getVert n ∧ v_1 = i'.getVert (n + 1) ∨ u_1 = i'.getVert (n + 1) ∧ v_1 = i'.getVert n) ∨
  i'.toSubgraph.Adj (i'.getVert n) (i'.getVert (n + 1))
Tactic: simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hxy : G.Adj u_1 v_1
i' : G.Walk v_1 w
ih : ∀ {i : ℕ} (hi : i < i'.length), i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n : ℕ
hi : n + 1 < (cons hxy i').length
⊢ (u_1 = i'.getVert n ∧ v_1 = i'.getVert (n + 1) ∨ u_1 = i'.getVert (n + 1) ∧ v_1 = i'.getVert n) ∨
    i'.toSubgraph.Adj (i'.getVert n) (i'.getVert (n + 1))
have cons : i'.toSubgraph.Adj (i'.getVert n) (i'.getVert (n + 1))
Tactic: right
-- 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
i : ℕ
hi : i < w.length
⊢ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))
have nil : ∀ {u : V} {i : ℕ} (hi : i < length.{u} (V := V) (G := G) (u := u) nil),
  Subgraph.Adj.{u} (V := V) (G := G) (Walk.toSubgraph (u := u) nil) (getVert (G := G) (u := u) nil i)
    (getVert (G := G) (u := u) nil (i + 1))
Tactic: induction w generalizing i with
  | nil => cases hi
  | cons hxy i' ih =>
    cases i
    · simp
    · simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
      right
      exact ih (Nat.succ_lt_succ_iff.mp hi)
Cleared hypotheses: w, i, hi
-- 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
i : ℕ
hi : i < w.length
nil :
  ∀ {u : V} {i : ℕ} (hi : i < length.{u} (V := V) (G := G) (u := u) Walk.nil),
    Subgraph.Adj.{u} (V := V) (G := G) (Walk.toSubgraph (u := u) Walk.nil) (getVert (G := G) (u := u) Walk.nil i)
      (getVert (G := G) (u := u) Walk.nil (i + 1))
⊢ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))
have cons : ∀ {u v w : V} (hxy : G.Adj u v) (i' : G.Walk v w)
  (ih : ∀ {i : ℕ} (hi : i < i'.length), i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))) {i : ℕ}
  (hi : i < (cons hxy i').length),
  (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert i) ((cons hxy i').getVert (i + 1))
Tactic: induction w generalizing i with
  | nil => cases hi
  | cons hxy i' ih =>
    cases i
    · simp
    · simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
      right
      exact ih (Nat.succ_lt_succ_iff.mp hi)
Cleared hypotheses: w, i, hi
-- 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
h : ¬w.Nil
⊢ w.toSubgraph.Adj w.penultimate v
have h₁ : 0 < w.length
Tactic: rw [not_nil_iff_lt_length] 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 u' v' : V
w : G.Walk u v
⊢ w.toSubgraph.Adj u' v' ↔ ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
have mp : w.toSubgraph.Adj u' v' → ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
mp : w.toSubgraph.Adj u' v' → ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
⊢ w.toSubgraph.Adj u' v' ↔ ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
have mpr : (∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length) → w.toSubgraph.Adj u' v'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
hadj : w.toSubgraph.Adj u' v'
⊢ ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
have hadj₁ : Subgraph.Adj (G := G)
  (match (motive := (v : V) → G.Walk u v → G.Subgraph) v, w with
  | .(u), nil => G.singletonSubgraph u
  | v, cons h p => G.subgraphOfAdj h ⊔ p.toSubgraph)
  u' v'
Tactic: unfold Walk.toSubgraph at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hadj :
  Subgraph.Adj (G := G)
    (match (motive := (v : V) → G.Walk u v → G.Subgraph) v, cons h p with
    | .(u), nil => G.singletonSubgraph u
    | v, cons h p => G.subgraphOfAdj h ⊔ p.toSubgraph)
    u' v'
⊢ ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
have hadj₁ : (u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u') ∨ p.toSubgraph.Adj u' v'
Tactic: simp only [Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
        Prod.swap_prod_mk] at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hl : u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u'
⊢ ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
have h₁ : s((cons h p).getVert 0, (cons h p).getVert (HAdd.hAdd (α := ℕ) 0 1)) = s(u', v') ∧ 0 < (cons h p).length
Tactic: use 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hl : u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u'
⊢ s((cons h p).getVert 0, (cons h p).getVert (HAdd.hAdd (α := ℕ) 0 1)) = s(u', v') ∧ 0 < (cons h p).length
have h₁ : s(u, v_2) = s(u', v') ∧ 0 < (cons h p).length
Tactic: simp only [Walk.getVert_zero, zero_add, getVert_cons_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hl : u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u'
⊢ s(u, v_2) = s(u', v') ∧ 0 < (cons h p).length
have h₁ : s(u, v_2) = s(u', v')
Tactic: refine ⟨?_, by simp only [length_cons, Nat.zero_lt_succ]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hr : p.toSubgraph.Adj u' v'
⊢ ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
have inr : ∀ (i : ℕ) (hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length),
  ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
Tactic: obtain ⟨i, hi⟩ := (toSubgraph_adj_iff _).mp hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
have h₁ : s((cons h p).getVert (i + 1), (cons h p).getVert (i + 1 + 1)) = s(u', v') ∧ i + 1 < (cons h p).length
Tactic: use i + 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s((cons h p).getVert (i + 1), (cons h p).getVert (i + 1 + 1)) = s(u', v') ∧ i + 1 < (cons h p).length
have h₁ : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i + 1 < (cons h p).length
Tactic: simp only [getVert_cons_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i + 1 < (cons h p).length
have h₁ : s(p.getVert i, p.getVert (i + 1)) = s(u', v')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
h₁ : s(p.getVert i, p.getVert (i + 1)) = s(u', v')
⊢ s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i + 1 < (cons h p).length
have h₂ : i + 1 < (cons h p).length
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hadj : (u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u') ∨ p.toSubgraph.Adj u' v'
⊢ ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
have inl : ∀ (hl : u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u'),
  ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
Tactic: cases hadj with
      | inl hl =>
        use 0
        simp only [Walk.getVert_zero, zero_add, getVert_cons_succ]
        refine ⟨?_, by simp only [length_cons, Nat.zero_lt_succ]⟩
        exact Sym2.eq_iff.mpr hl
      | inr hr =>
        obtain ⟨i, hi⟩ := (toSubgraph_adj_iff _).mp hr
        use i + 1
        simp only [getVert_cons_succ]
        constructor
        · exact hi.1
        · simp only [Walk.length_cons, Nat.add_lt_add_right hi.2 1]
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v_1 u' v' : V
w : G.Walk u v_1
v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
hadj : (u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u') ∨ p.toSubgraph.Adj u' v'
inl :
  ∀ (hl : u = u' ∧ v_2 = v' ∨ u = v' ∧ v_2 = u'),
    ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
⊢ ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
have inr : ∀ (hr : p.toSubgraph.Adj u' v'),
  ∃ (i : ℕ), s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length
Tactic: cases hadj with
      | inl hl =>
        use 0
        simp only [Walk.getVert_zero, zero_add, getVert_cons_succ]
        refine ⟨?_, by simp only [length_cons, Nat.zero_lt_succ]⟩
        exact Sym2.eq_iff.mpr hl
      | inr hr =>
        obtain ⟨i, hi⟩ := (toSubgraph_adj_iff _).mp hr
        use i + 1
        simp only [getVert_cons_succ]
        constructor
        · exact hi.1
        · simp only [Walk.length_cons, Nat.add_lt_add_right hi.2 1]
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
i : ℕ
hi : s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
⊢ w.toSubgraph.Adj u' v'
have mpr : w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))
Tactic: rw [← Subgraph.mem_edgeSet, ← hi.1, Subgraph.mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges
have rw : p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.toSubgraph.edgeSet
Tactic: rw [← p.mem_edges_toSubgraph, Subgraph.mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
rw : p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.toSubgraph.edgeSet
⊢ p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges
have rw₁ : p.toSubgraph.Adj u' v' ↔ p.toSubgraph.Adj u' v'
Tactic: rw [← p.mem_edges_toSubgraph, Subgraph.mem_edgeSet]