awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 < (Walk.cons hxy i').length
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))
⊢ (Walk.cons hxy i').toSubgraph.Adj ((Walk.cons hxy i').getVert (n + 1)) ((Walk.cons hxy i').getVert (n + 1 + 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]

Premises used: Sym2.eq, SimpleGraph.Subgraph.sup_adj, SimpleGraph.subgraphOfAdj_adj, SimpleGraph.Walk.toSubgraph, Prod.swap_prod_mk, SimpleGraph.Walk.getVert_cons_succ, Sym2.rel_iff', Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 < (Walk.cons hxy i').length
cons : i'.toSubgraph.Adj (i'.getVert n) (i'.getVert (n + 1))
⊢ (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:
right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
⊢ i'.toSubgraph.Adj (i'.getVert n) (i'.getVert (n + 1))

Tactic:
ih (Nat.succ_lt_succ_iff.mp hi)

Premises used: Nat.succ_lt_succ_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
⊢ i'.toSubgraph.Adj (i'.getVert n) (i'.getVert (n + 1))

Tactic:
exact ih (Nat.succ_lt_succ_iff.mp hi)

Premises used: Nat.succ_lt_succ_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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))
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 < (Walk.cons hxy i').length),
    (Walk.cons hxy i').toSubgraph.Adj ((Walk.cons hxy i').getVert i) ((Walk.cons hxy i').getVert (i + 1))
⊢ w.toSubgraph.Adj (w.getVert i) (w.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)

Premises used: Sym2.eq, SimpleGraph.Subgraph.sup_adj, SimpleGraph.subgraphOfAdj_adj, SimpleGraph.Walk.toSubgraph, Prod.swap_prod_mk, SimpleGraph.Walk.getVert_cons_succ, Sym2.rel_iff', SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj u w.snd

Tactic:
simpa using w.toSubgraph_adj_getVert (not_nil_iff_lt_length.mp h)

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

Tactic:
rw [not_nil_iff_lt_length] at h

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.length - 1 + 1 = w.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.length - 1 < w.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
simpa [show w.length - 1 + 1 = w.length from by lia]
    using w.toSubgraph_adj_getVert (by lia : w.length - 1 < w.length)

Premises used: SimpleGraph.Walk.toSubgraph_adj_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
mpr : (∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length) → w.toSubgraph.Adj u' v'
⊢ w.toSubgraph.Adj u' v' ↔ ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
hadj : w.toSubgraph.Adj u' v'
⊢ 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

Premises used: SimpleGraph.Walk.toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
hadj :
  Subgraph.Adj (G := G)
    (match (motive := (v : V) → G.Walk u v → G.Subgraph) u, nil with
    | .(u), nil => G.singletonSubgraph u
    | v, cons h p => G.subgraphOfAdj h ⊔ p.toSubgraph)
    u' v'
⊢ ∃ (i : ℕ),
    s(getVert (G := G) (u := u) nil i, getVert (G := G) (u := u) nil (i + 1)) = s(u', v') ∧
      i < length.{u} (V := V) (G := G) (u := u) nil

Tactic:
simp only [singletonSubgraph_adj, Pi.bot_apply, Prop.bot_eq_false] at hadj

Premises used: SimpleGraph.singletonSubgraph_adj, Prop.bot_eq_false, Pi.bot_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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'
⊢ (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

Premises used: Sym2.eq, SimpleGraph.Subgraph.sup_adj, SimpleGraph.subgraphOfAdj_adj, 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_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'
h₁ : s((cons h p).getVert 0, (cons h p).getVert (HAdd.hAdd (α := ℕ) 0 1)) = s(u', v') ∧ 0 < (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

Tactic:
use 0
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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'
h₁ : s(u, v_2) = s(u', v') ∧ 0 < (cons h p).length
⊢ s((cons h p).getVert 0, (cons h p).getVert (HAdd.hAdd (α := ℕ) 0 1)) = s(u', v') ∧ 0 < (cons h p).length

Tactic:
simp only [Walk.getVert_zero, zero_add, getVert_cons_succ]

Premises used: SimpleGraph.Walk.getVert_zero, zero_add, SimpleGraph.Walk.getVert_cons_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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'
⊢ 0 < (cons h p).length

Tactic:
simp only [length_cons, Nat.zero_lt_succ]

Premises used: Nat.zero_lt_succ, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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'
h₁ : s(u, v_2) = s(u', v')
⊢ s(u, v_2) = s(u', v') ∧ 0 < (cons h p).length

Tactic:
refine ⟨?_, by simp only [length_cons, Nat.zero_lt_succ]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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')

Tactic:
Sym2.eq_iff.mpr hl

Premises used: Iff.mpr, Sym2.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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')

Tactic:
exact Sym2.eq_iff.mpr hl

Premises used: Iff.mpr, Sym2.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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'
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
⊢ ∃ (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

Premises used: Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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((cons h p).getVert (i + 1), (cons h p).getVert (i + 1 + 1)) = s(u', v') ∧ i + 1 < (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

Tactic:
use i + 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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') ∧ i + 1 < (cons h 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

Tactic:
simp only [getVert_cons_succ]

Premises used: SimpleGraph.Walk.getVert_cons_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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')
h₂ : i + 1 < (cons h p).length
⊢ s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i + 1 < (cons h p).length

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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')

Tactic:
hi.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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')

Tactic:
exact hi.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 + 1 < (cons h p).length

Tactic:
simp only [Walk.length_cons, Nat.add_lt_add_right hi.2 1]

Premises used: And.right, SimpleGraph.Walk.length_cons, OfNat.ofNat, Nat.add_lt_add_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
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
⊢ ∃ (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]

Premises used: SimpleGraph.Walk.getVert_zero, zero_add, SimpleGraph.Walk.getVert_cons_succ, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
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'
⊢ ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length

Tactic:
match w with
    | .nil =>
      simp only [singletonSubgraph_adj, Pi.bot_apply, Prop.bot_eq_false] at hadj
    | .cons h p =>
      simp only [Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
        Prod.swap_prod_mk] at hadj
      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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
mpr : w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))
⊢ w.toSubgraph.Adj u' v'

Tactic:
rw [← Subgraph.mem_edgeSet, ← hi.1, Subgraph.mem_edgeSet]

Premises used: SimpleGraph.Subgraph.mem_edgeSet, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 (w.getVert i) (w.getVert (i + 1))

Tactic:
toSubgraph_adj_getVert _ hi.2

Premises used: And.right, SimpleGraph.Walk.toSubgraph_adj_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 (w.getVert i) (w.getVert (i + 1))

Tactic:
exact toSubgraph_adj_getVert _ hi.2

Premises used: And.right, SimpleGraph.Walk.toSubgraph_adj_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hp : p.toSubgraph.Adj u' v'
⊢ u' ∈ p.support

Tactic:
p.mem_verts_toSubgraph.mp (p.toSubgraph.edge_vert hp)

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Walk.mem_verts_toSubgraph, SimpleGraph.Walk.toSubgraph, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
rw₁ rw₂ : p.toSubgraph.Adj u' v' ↔ p.toSubgraph.Adj u' v'
⊢ p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges

Tactic:
rw [← p.mem_edges_toSubgraph, Subgraph.mem_edgeSet]

Premises used: SimpleGraph.Subgraph.mem_edgeSet, SimpleGraph.Walk.mem_edges_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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

Tactic:
⟨fun hw e he ↦ Subgraph.edgeSet_mono hw <| w.mem_edges_toSubgraph.mpr he, fun hw ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Subgraph.edgeSet_mono, Iff.intro, SimpleGraph.Walk.mem_edges_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
refine : ∀ (hw : w.edgeSet ⊆ G'.edgeSet), w.toSubgraph ≤ G'
⊢ w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet

Tactic:
refine ⟨fun hw e he ↦ Subgraph.edgeSet_mono hw <| w.mem_edges_toSubgraph.mpr he, fun hw ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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'

Tactic:
⟨fun v' hv' ↦ ?_, fun u' v' hadj ↦ hw <| w.mem_edges_toSubgraph.mp (hadj : s(_, _) ∈ _)⟩

Premises used: And.intro, Iff.mp, SimpleGraph.Walk.mem_edges_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
refine : ∀ (v' : V) (hv' : v' ∈ w.toSubgraph.verts), v' ∈ G'.verts
⊢ w.toSubgraph ≤ G'

Tactic:
refine ⟨fun v' hv' ↦ ?_, fun u' v' hadj ↦ hw <| w.mem_edges_toSubgraph.mp (hadj : s(_, _) ∈ _)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
⊢ ∃ e ∈ w.edges, v' ∈ e

Tactic:
rw [mem_verts_toSubgraph, mem_support_iff_exists_mem_edges_of_not_nil hnil] at hv'

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph, SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
have : ∀ (e : Sym2 V) (he : e ∈ w.edges) (hv'e : v' ∈ e), v' ∈ G'.verts
⊢ v' ∈ G'.verts

Tactic:
have ⟨e, he, hv'e⟩ := hv'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
e : Sym2 V
he : e ∈ w.edges
hv'e : v' ∈ e
⊢ v' ∈ G'.verts

Tactic:
G'.mem_verts_of_mem_edge (hw he) hv'e

Premises used: SimpleGraph.Subgraph.mem_verts_of_mem_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
e : Sym2 V
he : e ∈ w.edges
hv'e : v' ∈ e
⊢ v' ∈ G'.verts

Tactic:
exact G'.mem_verts_of_mem_edge (hw he) hv'e

Premises used: SimpleGraph.Subgraph.mem_verts_of_mem_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
right : ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w
⊢ p.bypass.toSubgraph ≤ p.toSubgraph

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst : DecidableEq V
⊢ p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts

Tactic:
simpa using p.support_bypass_subset

Premises used: SimpleGraph.Walk.support_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w

Tactic:
simpa [adj_toSubgraph_iff_mem_edges] using fun _ _ h ↦ p.edges_toPath_subset h

Premises used: SimpleGraph.Walk.adj_toSubgraph_iff_mem_edges, SimpleGraph.Walk.edges_toPath_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
rw : cons ⋯ (Walk.map ((cons h w).toSubgraph.hom.comp (Subgraph.inclusion ⋯)) w.mapToSubgraph) = cons h w
⊢ Walk.map (cons h w).toSubgraph.hom (cons h w).mapToSubgraph = cons h w

Tactic:
rw [mapToSubgraph, Walk.map, map_map]

Premises used: SimpleGraph.Walk.map, SimpleGraph.Walk.map_map, SimpleGraph.Walk.mapToSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
⊢ cons ⋯ (Walk.map ((cons h w).toSubgraph.hom.comp (Subgraph.inclusion ⋯)) w.mapToSubgraph) = cons h w

Tactic:
congrArg₂ _ rfl w.map_mapToSubgraph_hom

Premises used: congrArg₂, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
⊢ cons ⋯ (Walk.map ((cons h w).toSubgraph.hom.comp (Subgraph.inclusion ⋯)) w.mapToSubgraph) = cons h w

Tactic:
exact congrArg₂ _ rfl w.map_mapToSubgraph_hom

Premises used: congrArg₂, rfl
-- 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
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) ⋯)
            ⋯ :
          (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
⊢ 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

Tactic:
rw [mapToSubgraph, map_cons, map_map]

Premises used: SimpleGraph.Walk.map_map, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.mapToSubgraph