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 : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
pos : ∀ (he : i = 0 ∨ i = p.length), (p.toSubgraph.neighborSet v).ncard = 2
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have neg : ∀ (he : i ≠ 0 ∧ i ≠ p.length), (p.toSubgraph.neighborSet v).ncard = 2
Tactic: by_cases! he : i = 0 ∨ i = p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have huv : u = v
Tactic: have huv : u = v := by aesop
-- 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 u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have pos : Set.ncard (α := V) {p.snd, p.penultimate} = 2
Tactic: rw [← huv, hpc.neighborSet_toSubgraph_endpoint]
-- 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 u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2
have neg : Set.ncard (α := V) {p.getVert (i - 1), p.getVert (i + 1)} = 2
Tactic: rw [← hi.1, hpc.neighborSet_toSubgraph_internal he.1 (by lia)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
have this : w ∈ p.toSubgraph.neighborSet v
Tactic: have : w ∈ p.toSubgraph.neighborSet v := hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ p.toSubgraph.neighborSet v
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
have this₁ : Membership.mem (γ := Set V) {p.snd, p.penultimate} w
Tactic: rw [h.neighborSet_toSubgraph_endpoint] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : Membership.mem (γ := Set V) {p.snd, p.penultimate} w
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
have this₁ : w = p.snd ∨ w = p.penultimate
Tactic: push _ ∈ _ at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w = p.snd ∨ w = p.penultimate
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
have inl : ∀ (hl : w = p.snd), ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
Tactic: obtain hl | hr := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w = p.snd ∨ w = p.penultimate
inl : ∀ (hl : w = p.snd), ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
have inr : ∀ (hr : w = p.penultimate), ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
Tactic: obtain hl | hr := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts
have h₁ : p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts
Tactic: use p.reverse
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts
have hr₁ : w = p.reverse.getVert 1
Tactic: rw [penultimate, ← getVert_reverse] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.toSubgraph.verts = p.toSubgraph.verts
have rw : p.toSubgraph.verts = p.toSubgraph.verts
Tactic: rw [toSubgraph_reverse _]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
have simp : ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: simp only [← Finset.subset_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have h₁ : ∀ (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 sorry).support} ⊆ ∅)
  {v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) (hp : p.length + #s = n),
  ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: induction hp : p.length + #s using Nat.strong_induction_on generalizing s v with | _ n ih
Cleared hypotheses: v, p, s, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
h : {x ∈ s | x ∈ p.support}.Nonempty
hp : p.length + #s = n
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have h₁ : ∃ x ∈ s, x ∈ p.support
Tactic: simp only [Finset.Nonempty, mem_filter] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
h : ∃ x ∈ s, x ∈ p.support
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have h₁ : ∀ (x : V) (hxs : x ∈ s) (hx : x ∈ p.support),
  ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: obtain ⟨x, hxs, hx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have h : ∀ (h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅),
  ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: obtain h | h := Finset.eq_empty_or_nonempty {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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 :
  ∀ (h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).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} ⊆ ∅
have h₁ : ∀ (h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty),
  ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: obtain h | h := Finset.eq_empty_or_nonempty {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have h₁ : {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: use x, hxs, hx, h.le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
have hp₁ : p.length + (#(s.erase x) + 1) = n
Tactic: rw [← card_erase_add_one hxs] at hp
Cleared hypotheses: hp, hxs, hx, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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 + #(s.erase x) < n
have this : (p.takeUntil x hx).length ≤ p.length
Tactic: have := p.length_takeUntil_le hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have this : (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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have 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 sorry).support} ⊆ ∅),
  ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x sorry).support} ⊆ ∅
Tactic: obtain ⟨y, hys, hyp, h⟩ := ih _ this (s.erase x) h rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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} ⊆ ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
have h₁ : {t ∈ s.erase y | t ∈ (p.takeUntil y sorry).support} ⊆ ∅
Tactic: use y, mem_of_mem_erase hys, support_takeUntil_subset_support p hx hyp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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} ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
have h₁ : ∀ (h : {t ∈ s.erase y | t ∈ (p.takeUntil y sorry).support}.erase x ⊆ ∅), x ∉ {t ∈ s.erase y | t ∈ (p.takeUntil y sorry).support}
Tactic: rwa [takeUntil_takeUntil, erase_right_comm, filter_erase, erase_eq_of_notMem] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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 ⊆ ∅
⊢ x ∉ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}
have h₁ : ¬x = y → x ∈ s → x ∉ (p.takeUntil y sorry).support
Tactic: simp only [mem_filter, mem_erase, ne_eq, not_and, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
have 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
Tactic: obtain ⟨x, hxs, hx, h⟩ := p.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty s h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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} = ∅
⊢ ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
have h₁ : ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
Tactic: use x, hxs, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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} = ∅
⊢ ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
have h₁ : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
Tactic: suffices {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x} by simpa [Finset.subset_iff] using this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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} = ∅
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
have h₁ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support}.erase 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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}
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
have h₂ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support}.erase 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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}
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
have h₃ : ∀ (h : {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ insert 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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}
⊢ {t ∈ s | t ∈ (p.takeUntil x hx).support} ⊆ {x}
have h₄ : ∀ (h : {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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ (Walk.cons h p).toSubgraph.Connected
have cons : (G.subgraphOfAdj h ⊓ p.toSubgraph).verts.Nonempty
Tactic: apply Subgraph.connected_sup (subgraphOfAdj_connected h).preconnected ih.preconnected
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts.Nonempty
have cons : w ∈ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts
Tactic: exists w
-- 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.Connected
have nil : ∀ {u : V}, Subgraph.Connected.{u} (V := V) (G := G) (Walk.toSubgraph (u := u) Walk.nil)
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
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}, Subgraph.Connected.{u} (V := V) (G := G) (Walk.toSubgraph (u := u) Walk.nil)
⊢ p.toSubgraph.Connected
have 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
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
have refine_1 : Subgraph.Preconnected (V := V) (G := G) (induce ⊤ {u, v})
Tactic: refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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})
⊢ (induce ⊤ {u, v} ⊔ H ⊔ K).Connected
have refine_2 : (induce ⊤ {u, v} ⊓ H).verts.Nonempty
Tactic: refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_