awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
w : V
left : x ∈ s
w₁ : x ∈ p.support
h₁ : {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
use x, hxs, hx, h.le

Premises used: Eq.le
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
⊢ p.length + (#(s.erase x) + 1) = n

Tactic:
rw [← card_erase_add_one hxs] at hp

Premises used: Finset.card_erase_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
hp₁ : p.length + (#(s.erase x) + 1) = n
⊢ x ∈ s

Tactic:
rw [← card_erase_add_one hxs] at hp

Premises used: Finset.card_erase_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
hp₁ : p.length + (#(s.erase x) + 1) = n
hxs₁ : x ∈ s
⊢ x ∈ p.support

Tactic:
rw [← card_erase_add_one hxs] at hp

Premises used: Finset.card_erase_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
hp₁ : p.length + (#(s.erase x) + 1) = n
hxs₁ : x ∈ s
hx₁ : x ∈ p.support
⊢ {t ∈ s.erase x | t ∈ (p.takeUntil x hx₁).support}.Nonempty

Tactic:
rw [← card_erase_add_one hxs] at hp

Premises used: Finset.card_erase_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
x : V
hp : p.length + (#(s.erase x) + 1) = n
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
⊢ (p.takeUntil x hx).length ≤ p.length

Tactic:
have := p.length_takeUntil_le hx
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
x : V
hp : p.length + (#(s.erase x) + 1) = n
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length ≤ p.length
⊢ (p.takeUntil x hx).length + #(s.erase x) < n

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
⊢ (p.takeUntil x hx).length + #(s.erase x) < n

Tactic:
have : (p.takeUntil x hx).length + #(s.erase x) < n := by
    rw [← card_erase_add_one hxs] at hp
    have := p.length_takeUntil_le hx
    lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
h₁ :
  ∀ (y : V) (hys : y ∈ s.erase x) (hyp : y ∈ (p.takeUntil x hx).support)
    (h : {t ∈ (s.erase x).erase y | t ∈ ((p.takeUntil x hx).takeUntil y ⋯).support} ⊆ ∅),
    ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
obtain ⟨y, hys, hyp, h⟩ := ih _ this (s.erase x) h rfl

Premises used: Finset.erase, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h_1 : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ (s.erase x).erase y | t ∈ ((p.takeUntil x hx).takeUntil y ⋯).support} ⊆ ∅
h₁ : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
use y, mem_of_mem_erase hys, support_takeUntil_subset_support p hx hyp

Premises used: Finset.mem_of_mem_erase, SimpleGraph.Walk.support_takeUntil_subset_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h_1 : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ (s.erase x).erase y | t ∈ ((p.takeUntil x hx).takeUntil y ⋯).support} ⊆ ∅
h₁ :
  ∀ (h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅),
    x ∉ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅

Tactic:
rwa [takeUntil_takeUntil, erase_right_comm, filter_erase, erase_eq_of_notMem] at h

Premises used: Finset.filter_erase, SimpleGraph.Walk.takeUntil_takeUntil, Finset.erase_right_comm, Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h_1 : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
h₁ : ¬x = y → x ∈ s → x ∉ (p.takeUntil y ⋯).support
⊢ x ∉ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}

Tactic:
simp only [mem_filter, mem_erase, ne_eq, not_and, and_imp]

Premises used: and_imp, ne_eq, Finset.mem_erase, Finset.mem_filter, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h_1 : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
hxy : ¬x = y
⊢ x ∉ (p.takeUntil y ⋯).support

Tactic:
notMem_support_takeUntil_support_takeUntil_subset (Ne.symm hxy) hx hyp

Premises used: SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = m),
      ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
hp : p.length + #s = n
x : V
hxs : x ∈ s
hx : x ∈ p.support
h_1 : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
hxy : ¬x = y
⊢ x ∉ (p.takeUntil y ⋯).support

Tactic:
exact notMem_support_takeUntil_support_takeUntil_subset (Ne.symm hxy) hx hyp

Premises used: SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h : {x ∈ s | x ∈ p.support}.Nonempty
obtain :
  ∀ (x : V) (hxs : x ∈ s) (hx : x ∈ p.support) (h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅),
    ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
obtain ⟨x, hxs, hx, h⟩ := p.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty s h

Premises used: SimpleGraph.Walk.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h_1 : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
h₁ : ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
use x, hxs, hx
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h_1 : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
this : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
⊢ ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
simpa [Finset.subset_iff] using this

Premises used: Finset.subset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h_1 : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
h₁ : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
⊢ ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

Tactic:
suffices {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x} by simpa [Finset.subset_iff] using this
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
s : Finset V
h_1 : {x ∈ s | x ∈ p.support}.Nonempty
x : V
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
h₁ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support}.erase x = ∅), {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
h₂ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support}.erase x ⊆ ∅), {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
h₃ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ insert x ∅), {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
h₄ h₅ h₆ h₇ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}), {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}

Tactic:
rwa [Finset.filter_erase, ← Finset.subset_empty, ← Finset.subset_insert_iff,
    LawfulSingleton.insert_empty_eq] at h

Premises used: Finset.filter_erase, Finset.subset_empty, LawfulSingleton.insert_empty_eq, Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Subgraph.Connected.{u} (V := V) (G := G) (Walk.toSubgraph (u := u_1) Walk.nil)

Tactic:
apply singletonSubgraph_connected

Premises used: SimpleGraph.Subgraph.singletonSubgraph_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u_1 w w_1 : V
h : G.Adj u_1 w
p : G.Walk w w_1
ih : p.toSubgraph.Connected
cons : (G.subgraphOfAdj h ⊓ p.toSubgraph).verts.Nonempty
⊢ (Walk.cons h p).toSubgraph.Connected

Tactic:
apply Subgraph.connected_sup (subgraphOfAdj_connected h).preconnected ih.preconnected

Premises used: SimpleGraph.Subgraph.Connected.preconnected, SimpleGraph.Subgraph.connected_sup, SimpleGraph.Subgraph.subgraphOfAdj_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u_1 w w_1 : V
h : G.Adj u_1 w
p : G.Walk w w_1
ih : p.toSubgraph.Connected
cons : w ∈ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts
⊢ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts.Nonempty

Tactic:
exists w
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v u_1 w w_1 : V
h : G.Adj u_1 w
p : G.Walk w w_1
ih : p.toSubgraph.Connected
⊢ w ∈ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Subgraph.Connected.{u} (V := V) (G := G) (Walk.toSubgraph (u := u) Walk.nil)
cons :
  ∀ {u w w_1 : V} (h : G.Adj u w) (p : G.Walk w w_1) (ih : p.toSubgraph.Connected), (Walk.cons h p).toSubgraph.Connected
⊢ p.toSubgraph.Connected

Tactic:
induction p with
  | nil => apply singletonSubgraph_connected
  | @cons _ w _ h p ih =>
    apply Subgraph.connected_sup (subgraphOfAdj_connected h).preconnected ih.preconnected
    exists w
    simp

Premises used: SimpleGraph.Subgraph.singletonSubgraph_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Preconnected
tconn : (H.induce t).Preconnected
sintert : (s ⊓ t).Nonempty
⊢ (H.induce s ⊔ H.induce t).verts = (H.induce (s ∪ t)).verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (induce ⊤ {u, v} ⊔ H ⊔ K).Connected

Tactic:
Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_

Premises used: SimpleGraph.Subgraph.Connected.preconnected, SimpleGraph.Subgraph.connected_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
refine_1 : Subgraph.Preconnected (V := V) (G := G) (induce ⊤ {u, v})
refine_2 : (induce ⊤ {u, v} ⊓ H).verts.Nonempty
refine_3 : ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts.Nonempty
⊢ (induce ⊤ {u, v} ⊔ H ⊔ K).Connected

Tactic:
refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_

Premises used: SimpleGraph.Subgraph.Connected.preconnected, SimpleGraph.Subgraph.connected_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ Subgraph.Preconnected (V := V) (G := G) (induce ⊤ {u, v})

Tactic:
(top_induce_pair_connected_of_adj huv).preconnected

Premises used: SimpleGraph.Subgraph.top_induce_pair_connected_of_adj, SimpleGraph.Subgraph.Connected.preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ Subgraph.Preconnected (V := V) (G := G) (induce ⊤ {u, v})

Tactic:
exact (top_induce_pair_connected_of_adj huv).preconnected

Premises used: SimpleGraph.Subgraph.top_induce_pair_connected_of_adj, SimpleGraph.Subgraph.Connected.preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ u ∈ (induce ⊤ {u, v} ⊓ H).verts

Tactic:
simp [uH]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (induce ⊤ {u, v} ⊓ H).verts.Nonempty

Tactic:
exact ⟨u, by simp [uH]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ v ∈ ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts

Tactic:
simp [vK]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts.Nonempty

Tactic:
exact ⟨v, by simp [vK]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
mp : H.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
mpr : (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) → H.Preconnected
⊢ H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ (p : G.Walk u v), p.toSubgraph ≤ H

Tactic:
(hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_

Premises used: SimpleGraph.Reachable.elim, SimpleGraph.Subgraph.Preconnected.coe, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
mp :
  ∀
    (p :
      H.coe.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)),
    ∃ (p : G.Walk u v), p.toSubgraph ≤ H
⊢ ∃ (p : G.Walk u v), p.toSubgraph ≤ H

Tactic:
refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_

Premises used: SimpleGraph.Reachable.elim, SimpleGraph.Subgraph.Preconnected.coe, Subtype.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
mp : (Walk.map H.hom p).toSubgraph ≤ H
⊢ ∃ (p : G.Walk u v), p.toSubgraph ≤ H

Tactic:
exists p.map (Subgraph.hom _)

Premises used: SimpleGraph.Walk.map, SimpleGraph.Subgraph.hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
⊢ (Walk.map H.hom p).toSubgraph ≤ H

Tactic:
simp [coeSubgraph_le]

Premises used: SimpleGraph.Subgraph.coeSubgraph_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
mpr : H.coe.Preconnected
⊢ H.Preconnected

Tactic:
rw [Subgraph.preconnected_iff]

Premises used: SimpleGraph.Subgraph.preconnected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
mpr :
  ∀ (p : G.Walk u v) (h : p.toSubgraph ≤ H),
    H.coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
⊢ H.coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)

Tactic:
obtain ⟨p, h⟩ := hw hu hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
p : G.Walk u v
h : p.toSubgraph ≤ H
⊢ H.coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)

Tactic:
Reachable.map (Subgraph.inclusion h)
      (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)

Premises used: SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe._proof_1, SimpleGraph.Subgraph.inclusion, Subtype.mk, SimpleGraph.Walk.end_mem_verts_toSubgraph, SimpleGraph.Reachable.map, SimpleGraph.Walk.toSubgraph_connected, SimpleGraph.Walk.start_mem_verts_toSubgraph