awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Maximal Subgraph.Connected G' ↔ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'

Tactic:
⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩

Premises used: Exists, _private.0.SimpleGraph.ConnectedComponent.maximal_subgraph_connected_iff.match_2, _private.0.SimpleGraph.ConnectedComponent.maximal_subgraph_connected_iff.match_1, SimpleGraph.ConnectedComponent.toSubgraph, Iff.intro, SimpleGraph.Subgraph.Connected, Maximal, Eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
refine_1 :
  Maximal Subgraph.Connected G' →
    ∀ (hconn : G'.Connected) (h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'),
      ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
refine_2 :
  (∃ (C : G.ConnectedComponent), C.toSubgraph = G') →
    ∀ (C : G.ConnectedComponent) (h : C.toSubgraph = G'), Maximal Subgraph.Connected G'
⊢ Maximal Subgraph.Connected G' ↔ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'

Tactic:
refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
refine_1 : ∀ (v : V) (hv : v ∈ G'.verts), ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
⊢ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'

Tactic:
have ⟨v, hv⟩ := hconn.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
v : V
hv : v ∈ G'.verts
refine_1 : G' ≤ (G.connectedComponentMk v).toSubgraph
⊢ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'

Tactic:
suffices G' ≤ (G.connectedComponentMk v).toSubgraph from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSubgraph _) this) this⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
v : V
hv : v ∈ G'.verts
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph

Tactic:
le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦
      ConnectedComponent.sound <| hconn.coe.preconnected ⟨u, hu⟩ ⟨v, hv⟩ |>.map G'.hom

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Subgraph.le_induce_top_verts, SimpleGraph.Subgraph.hom, Subtype.mk, SimpleGraph.Reachable.map, SimpleGraph.ConnectedComponent.sound, SimpleGraph.Subgraph.induce_mono_right, le_trans, SimpleGraph.Subgraph.Connected.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
v : V
hv : v ∈ G'.verts
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph

Tactic:
exact le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦
      ConnectedComponent.sound <| hconn.coe.preconnected ⟨u, hu⟩ ⟨v, hv⟩ |>.map G'.hom

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Subgraph.le_induce_top_verts, SimpleGraph.Subgraph.hom, Subtype.mk, SimpleGraph.Reachable.map, SimpleGraph.ConnectedComponent.sound, SimpleGraph.Subgraph.induce_mono_right, le_trans, SimpleGraph.Subgraph.Connected.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
C : G.ConnectedComponent
h : C.toSubgraph = G'
⊢ Maximal Subgraph.Connected G'

Tactic:
h ▸ maximal_connected_toSubgraph _

Premises used: Eq.rec, SimpleGraph.ConnectedComponent.maximal_connected_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
C : G.ConnectedComponent
h : C.toSubgraph = G'
⊢ Maximal Subgraph.Connected G'

Tactic:
exact h ▸ maximal_connected_toSubgraph _
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).toSubgraph = G.subgraphOfAdj h

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
⊢ Membership.mem (γ := Set V) (Subgraph.verts (G := G) (Walk.toSubgraph (u := u_1) nil)) w ↔
    Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) w

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w x z : V
h : G.Adj x w
p' : G.Walk w z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w x y z : V
h_1 : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
h : w ∈ p'.support
⊢ w ∈ p'.support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support → w = y ∨ w ∈ p'.support

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w = y ∨ w ∈ p'.support ↔ w ∈ p'.support

Tactic:
have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
this : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
simp [ih, or_assoc, this]

Premises used: or_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Membership.mem (γ := Set V) (Subgraph.verts (G := G) (Walk.toSubgraph (u := u) Walk.nil)) w ↔
      Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p' : G.Walk v w_1) (ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support),
    w ∈ (Walk.cons h p').toSubgraph.verts ↔ w ∈ (Walk.cons h p').support
⊢ w ∈ p.toSubgraph.verts ↔ w ∈ p.support

Tactic:
induction p with
  | nil => simp
  | cons h p' ih =>
    rename_i x y z
    have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
    simp [ih, or_assoc, this]

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, or_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
nil :
  ∀ (hadj : Subgraph.Adj (G := G) (Walk.toSubgraph (u := u) Walk.nil) w x), ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (hadj : (Walk.cons h p).toSubgraph.Adj w x), ¬(Walk.cons h p).Nil
⊢ ¬p.Nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w u x : V
hadj : Subgraph.Adj (G := G) (Walk.toSubgraph (u := u) nil) w x
⊢ ¬Nil.{u} (V := V) (G := G) (v := u) nil

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w u v x v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
hadj : (cons h p).toSubgraph.Adj w x
⊢ ¬(cons h p).Nil

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.toSubgraph.verts

Tactic:
simp [mem_verts_toSubgraph]

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.toSubgraph.verts

Tactic:
simp [mem_verts_toSubgraph]

Premises used: SimpleGraph.Walk.mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph.verts = {w : V | w ∈ p.support}

Tactic:
Set.ext fun _ => p.mem_verts_toSubgraph

Premises used: Set.ext, SimpleGraph.Walk.mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
e : Sym2 V
nil :
  ∀ {u : V},
    Membership.mem (γ := Set (Sym2 V)) (Subgraph.edgeSet (G := G) (Walk.toSubgraph (u := u) Walk.nil)) e ↔
      Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges) → (e ∈ (Walk.cons h p).toSubgraph.edgeSet ↔ e ∈ (Walk.cons h p).edges)
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u_1 : V
⊢ Membership.mem (γ := Set (Sym2 V)) (Subgraph.edgeSet (G := G) (Walk.toSubgraph (u := u_1) nil)) e ↔
    Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges
⊢ e ∈ (cons h p).toSubgraph.edgeSet ↔ e ∈ (cons h p).edges

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph.edgeSet = p.edgeSet

Tactic:
Set.ext fun _ => p.mem_edges_toSubgraph

Premises used: Set.ext, SimpleGraph.Walk.mem_edges_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
nil : ∀ {u : V} (q : G.Walk u w), (append Walk.nil q).toSubgraph = Walk.toSubgraph (u := u) Walk.nil ⊔ q.toSubgraph
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 w), (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph) →
      ∀ (q : G.Walk w_1 w), ((Walk.cons h p).append q).toSubgraph = (Walk.cons h p).toSubgraph ⊔ q.toSubgraph
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
q : G.Walk u_1 w
⊢ (append nil q).toSubgraph = Walk.toSubgraph (u := u_1) nil ⊔ q.toSubgraph

Tactic:
simp [*, sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (q : G.Walk w_1 w), (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph
q : G.Walk w_1 w
⊢ ((cons h p).append q).toSubgraph = (cons h p).toSubgraph ⊔ q.toSubgraph

Tactic:
simp [*, sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := G.Subgraph) (Walk.toSubgraph (u := u_1) (reverse nil)) (Walk.toSubgraph (u := u_1) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 : p.toSubgraph ⊔ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1) = G.subgraphOfAdj h ⊔ p.toSubgraph
⊢ (Walk.cons h p).reverse.toSubgraph = (Walk.cons h p).toSubgraph

Tactic:
simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]

Premises used: SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.toSubgraph_append, SimpleGraph.Walk.reverse_cons, SimpleGraph.subgraphOfAdj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 : G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 ⊔ p.toSubgraph = G.subgraphOfAdj h ⊔ p.toSubgraph
⊢ p.toSubgraph ⊔ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1) = G.subgraphOfAdj h ⊔ p.toSubgraph

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 : G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 = G.subgraphOfAdj h
⊢ G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 ⊔ p.toSubgraph = G.subgraphOfAdj h ⊔ p.toSubgraph

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
cons₁ : ∀ (x x_1 : V), (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1).Adj x x_1 ↔ (G.subgraphOfAdj h).Adj x x_1
⊢ G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1 = G.subgraphOfAdj h

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
x : V
⊢ x ∈ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1).verts ↔ x ∈ (G.subgraphOfAdj h).verts

Tactic:
simp [-Set.bot_eq_empty]

Premises used: Set.bot_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
x x_1 : V
⊢ (G.subgraphOfAdj h ⊔ G.singletonSubgraph u_1).Adj x x_1 ↔ (G.subgraphOfAdj h).Adj x x_1

Tactic:
simp [-Set.bot_eq_empty]

Premises used: Set.bot_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    p.reverse.toSubgraph = p.toSubgraph → (Walk.cons h p).reverse.toSubgraph = (Walk.cons h p).toSubgraph
⊢ p.reverse.toSubgraph = 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]

Premises used: SimpleGraph.Walk.toSubgraph, Set.bot_eq_empty, SimpleGraph.Walk.cons, sup_comm, SimpleGraph.Walk.toSubgraph_append, SimpleGraph.Walk.nil, SimpleGraph.Walk.reverse_cons, SimpleGraph.subgraphOfAdj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
rw₄ rw₅ : c.toSubgraph = c.toSubgraph
⊢ (c.rotate u h).toSubgraph = c.toSubgraph

Tactic:
rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.rotate, sup_comm, SimpleGraph.Walk.toSubgraph_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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)
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 (Walk.cons h p)).toSubgraph = Subgraph.map f (Walk.cons h p).toSubgraph
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u_1 : V
⊢ Walk.toSubgraph (u := (f : (a : V) → V') u_1) (Walk.map f nil) = Subgraph.map f (Walk.toSubgraph (u := u_1) nil)

Tactic:
simp [*, Subgraph.map_sup]

Premises used: SimpleGraph.Subgraph.map_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : (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:
simp [*, Subgraph.map_sup]

Premises used: SimpleGraph.Subgraph.map_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ (mapLe h p).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
⊢ Set.Finite.{u} (α := V) ∅

Tactic:
apply Set.toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 : ((G.subgraphOfAdj ha).neighborSet w ∪ p.toSubgraph.neighborSet w).Finite
⊢ ((Walk.cons ha p).toSubgraph.neighborSet w).Finite

Tactic:
rw [Walk.toSubgraph, Subgraph.neighborSet_sup]

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

Tactic:
Set.Finite.union ?_ ih

Premises used: Set.Finite.union
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 : ((G.subgraphOfAdj ha).neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w ∪ p.toSubgraph.neighborSet w).Finite

Tactic:
refine Set.Finite.union ?_ ih

Premises used: Set.Finite.union
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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

Tactic:
Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)

Premises used: SimpleGraph.neighborSet_subgraphOfAdj_subset, Set.Finite.subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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 : Set.Finite (α := V) {u_1, v_1}
⊢ ((G.subgraphOfAdj ha).neighborSet w).Finite

Tactic:
refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)

Premises used: SimpleGraph.neighborSet_subgraphOfAdj_subset, Set.Finite.subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
⊢ Set.Finite (α := V) {u_1, v_1}

Tactic:
apply Set.toFinite

Premises used: Set.toFinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
cons :
  ∀ {u v w_1 : V} (ha : G.Adj u v) (p : G.Walk v w_1) (ih : (p.toSubgraph.neighborSet w).Finite),
    ((Walk.cons ha p).toSubgraph.neighborSet w).Finite
⊢ (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

Premises used: SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.cons, Set.toFinite, SimpleGraph.Walk.nil, SimpleGraph.Subgraph.neighborSet_sup, SimpleGraph.neighborSet_singletonSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph ≤ Subgraph.induce ⊤ p.toSubgraph.verts

Tactic:
Subgraph.le_induce_top_verts

Premises used: SimpleGraph.Subgraph.le_induce_top_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : {v_1 : V | v_1 ∈ p.support} = p.toSubgraph.verts
⊢ p.toSubgraph ≤ Subgraph.induce ⊤ {v_1 : V | v_1 ∈ p.support}

Tactic:
convert! Subgraph.le_induce_top_verts

Premises used: SimpleGraph.Subgraph.le_induce_top_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ {v_1 : V | v_1 ∈ p.support} = p.toSubgraph.verts

Tactic:
p.verts_toSubgraph.symm

Premises used: SimpleGraph.Walk.verts_toSubgraph, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ {v_1 : V | v_1 ∈ p.support} = p.toSubgraph.verts

Tactic:
exact p.verts_toSubgraph.symm

Premises used: SimpleGraph.Walk.verts_toSubgraph, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
i : ℕ
hi : i < length.{u} (V := V) (G := G) (u := u_1) nil
⊢ Subgraph.Adj.{u} (V := V) (G := G) (Walk.toSubgraph (u := u_1) nil) (getVert (G := G) (u := u_1) nil i)
    (getVert (G := G) (u := u_1) nil (i + 1))

Tactic:
cases hi
-- 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))
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))
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))
⊢ (Walk.cons hxy i').toSubgraph.Adj ((Walk.cons hxy i').getVert i) ((Walk.cons hxy i').getVert (i + 1))

Tactic:
cases i
-- 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))
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:
simp